Class Central is learner-supported. When you buy through links on our site, we may earn an affiliate commission.

Reverse Engineering 3201: Symbolic Analysis

OpenSecurityTraining2 via Independent

Overview

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.

Syllabus

  1. Introduction
  2. SAT and Constraints
  3. angr and Symbolic execution
  4. The binary bomb
  5. Congratulations

Taught by

Thaís Moreira Hamasaki

Reviews

Start your review of Reverse Engineering 3201: Symbolic Analysis

Never Stop Learning.

Get personalized course recommendations, track subjects and courses with reminders, and more.