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.
