Practical Symbolic Execution for VR and RE
Virtual 32 CPE Hours Training ★ February 2024
WEEK 1 ★ FEB 10-17 // DETAILED SCHEDULE READY
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 techniques to their problems. 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 use symbolic execution to answer reverse engineering problems, to bypass obfuscations, and to detect many different classes of vulnerabilities. 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 modern 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 working with a variety of low-level binaries and firmware.
Key Learning Objectives
- Understanding of core Symbolic Execution concepts
- Exposure to modern Symbolic Execution toolsets
- Ability to craft custom analysis tooling using Symbolic Execution tooling
- Build intuition on when Symbolic Execution is useful, and when it isn't
This course will benefit anyone who works with analyzing software or firmware. The techniques taught in this class will help reverse engineers to better answer questions and deobfuscate binaries. The course will also help vulnerability researchers to better create tooling to detect vulnerabilities and aid in exploitation.
Symbolic Execution Concepts
- Symbolic Execution Base Concepts
- Expressions as ASTs
- Common uses of Symbolic Execution
- Common Symbolic Execution Weaknesses
- Popular Symbolic Execution Tooling
- Introduction to a few useful Symbolic Execution Frameworks
- Triton Introduction and Demos
- Triton DSE Introduction and Demos
- MAAT Introduction and Demos
- Framework Comparisons
- Taint Analysis
- Using Concrete Traces
- Symbolic Hooks
- Crash Triaging
- Crash Root-Cause Analysis
- Test Case Generation
- Different Exploration Strategies
- Exploration Heuristics
- Overflows and Write-What-Where Detection
- ToCToU Race Condition Detection
- Scope Vulnerability Detection
- Patches and Variants Discussion
- Anti-Static Obfuscation defeat strategies
- Anti-Dynamic Obfuscation defeat strategies
- Working knowledge of Python scripting
- Understanding of X86_64 Binary Reversing
- Familiarity with Memory Corruption Vulnerabilities
A cloud instance will be provided to the students. They must have an internet connection to SSH into their cloud machine.
No software is required, though an interactive disassembler will be useful. Students are welcome to use whatever disassembler they are comfortable with. Binary Ninja's free Cloud platform would be sufficient for the class.
Jordan Whitehead is a Principal Research Consultant at Atredis Partners. He has experience finding and exploiting vulnerabilities in a variety of low-level systems, and has previously helped develop and instruct advanced kernel exploitation and reverse engineering courses.