Intro to Binary Analysis with Z3 and angr
By Sam Brown on 8 November, 2018
If you’ve ever wanted to play with angr but found the barrier to entry too high? Or have you seen people do what may as well be straight up magic using tools like Z3? This workshop will kick start your journey to understanding!
Sample code and labs are included which cover real world challenges that you can immediately apply to your work, hobby, or CTFs. By the end of the workshop you should have an appreciation for what an SMT solver is, problems it can be used to solve, and how to start using Z3 and angr to automate tasks.
Originally delivered by Sam Brown at Steelcon and hack.lu 2018, this was a three hour workshop introducing attendees to using Z3 and angr for SMT solving. The workshop provided an introduction to SMT solvers, the Z3 SMT solver and its python library and the angr binary analysis framework.
Throughout the workshop exercises were provided which aimed to demonstrate potential applications of the technology to assist security researchers carrying out reverse engineering and vulnerability research.
The accompanying code and exercises can be found on Github.