Abstract
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
Contents
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