»Intro to Binary Analysis with Z3 and Angr«
2018-10-17, 13:30–17:30, Vianden - Wiltz

This workshop aims to provide some basic knowledge and exposure to the Z3 SMT solver and Angr binary analysis platform. By the end of the workshop attendees should have an appreciation for what an SMT solver is, problems it can be applied too and usage of Z3 and Angr to begin automating tasks which they can be applied to.

SMT solvers have been at the core of some seriously cool research projects, paticularly in Reverse Engineering and Exploit Development. However the field has a high barrier to entry, often requiring a strong background in Computer Science that a lot of practitioners have never experienced. This workshop aims to provide some basic knowledge and exposure to the Z3 SMT solver and Angr binary analysis platform.

If you've ever wanted to play with Angr but found the barrier to entry too high or seen people do what may aswell be straight up magic using tools like Z3 then hoepfully this workshop will kick start your journey to understanding! Sample code and labs will be included which cover real world and subsets of real world challenges. By the end of the workshop attendees should have an appreciation for what an SMT solver is, problems it can be applied too and usage of Z3 and Angr to begin automating tasks which they can be applied to.

At the end of the workshop a 'king of the hill' style CTF challenge will be opened up.

Contents:

  • What the Hell is an SMT Solver?
  • Z3-python
  • Lab - Cheating at Logic Challenges
  • Lab – Encoding CPU Instructions
  • Z3 in the Real World
  • Angr!
  • Lab – Using Angr in Anger
  • Wrap-up
  • CTF/King of the Hill

Length:

3 hours

Requirements:

Laptop with VirtualBox installed, 30GB of disk space and atleast 4GB of RAM to dedicate to it. A Debian VM with all required tools installed and configured along with exercise files and sample code will be provided.

Pre-requisites:

  • Working knowledge of python scripting
  • Some exposure to assembly language
Speaker