Intro to Binary Analysis with Z3 and angr

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 binary analysis. The workshop provided an introduction to SMT solvers, the Z3 SMT solver and its python library and the angr binary analysis framework.

Through out the workshop exercises were provided which aimed to demonstrate potential applications of the technology to assist security researchers in carrying out reverse engineering and vulnerability research.

The slides provide a rough guide for the content and what order to try the exercises in.

Examples and Exercises

Z3

Name	Type	Description
N Queens	Example	'How can N queens be placed on an NxN chessboard so that no two of them attack each other?' Uses Z3 to generate solutions for an N * N chessboard
Hackvent 15	Example	Solution and walk through for solving a Hackvent 15 CTF challenge with Z3
Sudoku	Exercise	Try to solve Sudoku using Z3
RNG	Exercise	Optional exercises - using Z3 to find non-cryptographically secure random number generators seed value
x86	50/50	Half examples, half DIY - implement simiplified versions of x86 instructions using Z3
Opaque Predicates	Exercise	Use the instructions implemented previously to identify Opaque Predicates in small sequences of assembly instructions
Equivalence Checking