Practical Symbolic Execution for VR and RE


Jordan Whitehead


The “Practical Symbolic Execution for VR and RE” course is a detailed dive into symbolic execution for Reverse Engineers and Vulnerability Researchers. This course provides a diverse set of demonstrations and labs that will help students learn how to effectively apply symbolic execution to their work. A practical approach to symbolic execution will give students hands-on experience solving real world problems through the development of custom analysis tooling.

Students can expect to create custom analysis tooling using symbolic execution. The labs cover a variety of practical situations that will help students explore applications of symbolic execution. These real-world problems will also help them to understand symbolic execution's strengths and limitations. In the labs students will programmatically root-cause crashes, detect various forms of memory corruption, generate unique test cases, and more. The techniques taught are applicable to a variety of low-level binaries and firmware.

Key learning objectives

  • Understanding of core Symbolic Execution concepts
  • Exposure to modern Symbolic Execution tool-sets
  • Ability to craft custom analysis tooling using Symbolic Execution tooling
  • Build intuition on when Symbolic Execution is useful, and when it isn't


Day 1:

Symbolic Execution Concepts:

  • Lifting
  • Expressions as ASTs
  • Solving
  • Common uses of Symbolic Execution
  • Popular Symbolic Execution Tooling

Framework Introductions:

  • Introduction to Frameworks
  • Triton Introduction and Demos
  • MAAT Introduction and Demos
  • Framework Comparisons

Day 2:

Analysis Introduction:

  • Taint Analysis
  • Using Concrete Traces
  • Symbolic Hooks
  • Crash Triaging
  • Crash Root-Cause Analysis

Day 3:

Path Exploration:

  • Test Case Generation
  • Different Exploration Strategies
  • Exploration Heuristics

Day 4:

Vulnerability Detection:

  • Overflows and Write-What-Where Detection
  • ToCToU Race Condidtion Detection
  • Scope Vulnerability Detection
  • Patches and Variants Discussion

Knowledge Prerequisites

  • Working knowledge of Python Scripting
  • Familiarity with Reverse Engineering x86-64 binaries

Hardware Requirements

Students should have access to a machine with which to SSH into a provided test machine