Practical Symbolic Execution and SATisfiability Module Theories (SMT) 101

Practical Symbolic Execution and SATisfiability Module Theories (SMT) 101

May 19, 2018 • By rui

Finding bugs is hard, reverse engineering is hard. Constraint solvers are the heart of many program analysis techniques, and can aid Fuzzing, and software verification.

This post contains a few hands-on experiments with Z3, a high performance theorem prover developed at Microsoft Research by Leonardo de Moura and Nikolaj Bjorner. With KLEE, a Symbolic Execution Engine built on top of the LLVM compiler infrastructure developed by Cristian Cadar, Daniel Dunbar, and Dawson Engler. And, angr, a binary analysis framework developed by the Computer Security Lab at UC Santa Barbara and their associated CTF team, Shellphish.[…]

http://deniable.org/reversing/symbolic-execution

 

Symbiotic: tool for finding bugs in computer programs based on instrumentation, program slicing and KLEE

Symbiotic is a tool for analysis of computer programs. It can check all common safety properties like assertion violations, invalid pointer dereference, double free, memory leaks, etc. Symbiotic uses three well-know techniques: instrumentation, program slicing, and symbolic execution. We use LLVM as program representation.

https://github.com/staticafi/symbiotic

http://staticafi.github.io/symbiotic/

KLEE 1.4.0 released

Cristian Cadar announced the 1.4.0 release of KLEE.

KLEE 1.4.0 is now available at
https://github.com/klee/klee/releases/tag/v1.4.0

Lots of new changes, in particular a new CMake build system, support for  some missing features for LLVM 3.4 (and partial support for 3.5 and  3.6), better support for MacOS, support for release documentation (as in  http://klee.github.io/releases/docs/v1.4.0/) and many other  optimizations, features and bug fixes.[…]

Full announcement:
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
https://klee.github.io/

https://github.com/klee/klee

 

FiE

I just noticed FIE, from Usenix Security 2013!

FIE on Firmware: Finding Vulnerabilities in Embedded Systems Using Symbolic Execution
Drew Davidson, Benjamin Moench, Somesh Jha, Thomas Ristenpart

Embedded systems increasingly use software-driven low-power microprocessors for security-critical settings, surfacing a need for tools that can audit the security of the software (often called firmware) running on such devices. Despite the fact that firmware programs are often written in C, existing source-code analysis tools do not work well for this setting because of the specific architectural features of low-power platforms. We therefore design and implement a new tool, called FIE, that builds off the KLEE symbolic execution engine in order to provide an extensible platform for detecting bugs in firmware programs for the popular MSP430 family of microcontrollers. FIE incorporates new techniques for symbolic execution that enable it to verify security properties of the simple firmwares often found in practice. We demonstrate FIE’s utility by applying it to a corpus of 99 open-source firmware programs that altogether use 13 different models of the MSP430. We are able to verify memory safety for the majority of programs in this corpus and elsewhere discover 21 bugs.

http://pages.cs.wisc.edu/~davidson/fie/

pages.cs.wisc.edu/~davidson/fie/fie.tgz
http://pages.cs.wisc.edu/~davidson/fie/directions.html

https://www.usenix.org/conference/usenixsecurity13/technical-sessions/paper/davidson

https://www.usenix.org/conference/usenixsecurity13/fie-firmware-finding-vulnerabilities-embedded-systems-using-symbolic

 

 

EBC

EBC, The EFI Byte Code, is a UEFI feature that supports Intel (Itanium, x86, and x64) instructions in a single bytecode. The Intel C Compiler can target EBC, and UEFI drivers can use EBC instead of native drivers, to save space (1 binary, instead of 3).

The other week I gave a firmware security tools talk at BlackLodgeResearch.org, and Vincent Zimmer of Intel showed up. I had a slide complaining that EBC is only supported by Intel C Compiler, a commercial-only product, and that the UEFI Forum should fund a ‘summer-of-code’-style effort to get EBC into GCC or LLVM CLang. After the talk, Vincent mentioned that ICC had to do a bit of unexpected work to generate EBC, and would blog about it. Well, he did blog about it, a few days ago, just catching up to it, and describe the problem.
http://vzimmer.blogspot.com/2015/08/efi-byte-code.html

If you know of someone on the LLVM CLang or GCC project, please try to add a request for EBC support.

Not only would it be nice to have LLVM CLang work with EBC to have an alternative to ICC, and for LLBVM’s Klee fuzzer (to fuzz UEFI via OVMF), but ALSO because the Capstone Framework RE tool uses LLVM’s intermediate form and would then get EBC support!!
http://www.capstone-engine.org/

Today, radare2, another RE tool, already has EBC support.
https://firmwaresecurity.com/2015/07/26/tool-mini-review-radare2/

If technically possible, it might be nice if ARM added AArch32 and AArch64 support, and EBC support in their compiler, so that EBC could actually target all UEFI platforms with a single blob. ARM/Linaro already has something that appears to overlap in some ways:
http://people.linaro.org/~christoffer.dall/arm-vm-spec-v1.0.txt

Also, there’s a C#/IL to EBC translation project on Github. If you get it to work, let me know!
https://github.com/nnliaohua/CIL2EBC-ToolChain