This talk is intended for people that are interested in automatic binary analysis and want to get started with it. Getting into automated binary analysis seems daunting at first due the lack of clear starting points and the complexity of the underlying techniques. Also there are various frameworks which all seem similar but have some subtle differences on closer inspection. The whitepaper and talks are often hard to find and understand, or are simply outdated and don’t represent the current state of the project anymore.

We will start with short introduction to the Z3 theoreom prover, specifically its constraint solver that is used in some form by most frameworks and how to manually use it for simple crackme-like tasks to show some of it’s more capabilities that are useful for reverse engineering.

Then we will generally look at the concept of symbolic execution and how it can be combined with constraint solvers for modelling the possible states of a program.

After a quick overview of the popular analysis frameworks(angr, Triton, miasm and others) and some of their differences we will walk through some example challenges with angr.
The focus here will be not on showing that they can be solved with 20 lines of Python that contain the string “”angr”” a lot but on how specifically angr is used to for various kinds of typical reverse engineering tasks. ”

Florian Magin is a security researcher at ERNW Research GmbH. His main interests are reverse engineering and automated security analysis of binary applications. In his free time he is active in the local CCC Erfa and one of the people organizing the CTF team “WizardsOfDos”



[Slides (PDF)] [Recording (MP4)] [Recording (OGV)]

Comments are closed.