Binary Constraint Solving for Automatic Exploit Generation
This talk will show how to perform a control flow attack against a complex, stand-alone application. Specifically, how to use mcsema, LLVM, and satisfiability solvers to discover a targeted execution path using side channel analysis. I show how to traverse this path to collect path constraints and solve for user input which would give us the desired output. This process can then be applied to any targeted behavior in a program, from finding known vulnerability characteristics to simply supplying the correct input to a ‘crackme’ binary. Practical uses of program analysis will be presented and explained including instrumentation, symbolic execution, and concolic execution, both in theory and in practice, and tools for each type of analysis.
The talk will conclude with a demonstration that uses the tools described to solve an obfuscated ‘crackme’ challenge, and a ‘competition’ between a pintool solver and a pysymemu solver that compares which can extract the flag from the same binary first.
- Slides: Automated Exploit Generation
- Sophia D'Antoine