SMT Solver Workshop
This is a one day Workshop on using SMT solvers for reverse engineering I gave at the Honeynet Project Annual Workshop in 2016. It contains the full slides, as well as the tasks and solutions. It teaches the basics of how program behavior is encoded in SMT formulas (more precisely, quantifier free theory of bitvectors - no theory of arrays / separation logic content in a one day workshop, sorry) and how one can use these formulas to get answers to questions about low level program behavior. In particular, it addresses transformations such as SSA and how to deal with control flow such as if statements and loops. Then more practical examples are provided: obtain collisions and preimages for weak hash functions and use existing bounded model checkers to find bugs in C code.
- Task 1: Setup SMT solver and use bitvectors to solve constraints with overflows.
- Task 2: Check that an expression that was obfuscated using mixed boolean arithmetic is equivalent to the simpler original expression.
- Task 3: Perform a Static Single Assignment transformation to turn programs with variables into SMT formulas.
- Task 4: Transform if-statements and branches into formulas.
- Task 5: Perform loop unrolling for fixed length loops.
- Task 6: Perform loop unrolling for loops with an unknown number of iterations.
- Task 7: Use an SMT solver to obtain an input that has a CRC-32 of 0 using a very limited character set.
- Task 8: Use a bounded model checker to avoid doing all the manual work.
- Task 9: Find security issues in a small C library using a bounded model checker.
