What learning paths is this class used in?
Exploits, and Reverse Engineering
Reverse Engineering 3201: Symbolic Analysis
OpenSecurityTraining2
About This Course
Symbolic execution is a way to analyze a program and determine which inputs (or input groups) cause which specific part of a program to execute. To do so, symbolic execution uses symbolic values instead of regular input values. This allows to construct a result that can be expressed as an equation (or a system of equations) of these symbolic values, and can be solved mathematically. This is where the SMT (satisfiability modulo theories) enters in play, and using all the different constraints, is able to say if there is a solution to our equation, and if so, which one.
Symbolic execution is a powerful tool for code verification, bug hunting, and reverse engineering. In this class, we will dive into the concepts of constraint programming and SMT solvers and how binary analysis tools integrate these concepts into their frameworks.
This class is designed to be hands-on, and we will be using several Python frameworks against CTF challenges: a binary analysis framework called angr and a SMT solver called z3. These two tools are well known to CTF players as they are often used to save time when working on reverse engineering challenges, this is also the path we will follow.
Learning Objectives
- Understand the underlying concepts of symbolic execution, its strength and weaknesses
- Overview of binary analysis tools and SMT solvers
- Learn to use features of angr and z3 and apply that knowledge to CTF challenges
Requirements
You must be comfortable with Python3 programming.
If you need to learn Python, we recommend LearnPython.org
Frequently Asked Questions
“Constraint programming represents one of the closest approaches computer science has yet made to the Holy Grail of programming: the user states the problem, the computer solves it.”
Eugene C. Freuder, Constraints, April 1997
Course Staff
Thaís Moreira Hamasaki
Thaís Moreira Hamasaki works as an Offensive Security Researcher at Intel in the prestigious STORM (STrategic Offensive Research and Mitigations) team, with the main objective of discovering and mitigating next generation security threats.
Thaís started her career working on data and malware analysis in the anti-virus industry, where she developed her knowledge of threat protection systems. She became interested very early by symbolic execution, which was not only one of the topics of her very first talk "Using SMT solvers to deobfuscate malware binaries" (for which she won the "best rookie speaker" award from BSides London), but also included in her thesis "Malware Detection and Analysis with Constraint Programming". She loves to explore new topics and gain a deep understanding of them. Her latest research topics include various domains such as hardware-based cryptography, Intel® Trust Domain Extensions, System-Management Mode and Intel® graphics.
Thaís is an active and recognized member of the infosec community: she leads the groups for Reverse Engineering and x86 assembly at the chaosdorf (a CCC-hackerspace based in Düsseldorf), participates in program committees of international conferences and is a board member of blackhoodie (a reverse engineering bootcamp for women). She has given several talks and workshops at international conferences such as Hack.lu, Virus Bulletin, NorthSec, H2HC, Hacktivity, and so on.
In her free time, you can find Thaís writing bad code to solve CTFs, cooking, or climbing somewhere offline.