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
