Skip to content
Code and exercises for a workshop on z3 and angr
Branch: master
Clone or download
Sam Brown
Latest commit b95e33c Nov 30, 2018
Type Name Latest commit message Commit time
Failed to load latest commit information.
angr angr downcase-age Nov 12, 2018
z3 learn to spell Sudoku Sam... Nov 5, 2018
.gitignore Initial commit Oct 23, 2018 angr downcase-age Nov 12, 2018
mwri_hacklu_2018_samdb_z3_final.pdf update slides, calling convention correction Nov 30, 2018

Intro to Binary Analysis with Z3 and angr

Originally delivered by Sam Brown at Steelcon and 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


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 Example Use the instructions implemented previously to identify equivalent sequences of instructions


Name Type Description
opaque_predicates Example Using angr to identify opaque predicates with much less work :)
IOCTLs Example Identify Windows driver IOCTL codes using angr
Hello World 50/50 Exercise and walkthrough on using angr to generate valid arguments for a simple 'License Key Validator'
Bomb Lab Exercise DIY exercise using angr to solve a 'Bomb lab'


All code is in Python3 and you should only need to install the angr binary analysis framework.

mkvirtualenv --python=$(which python3) angr && python -m pip install angr
workon angr 
You can’t perform that action at this time.