Practical symbolic execution for VR and RE

Jordan Whitehead

BOOK NOW

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 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.

INTENDED AUDIENCE

💡
This course will benefit anyone who works with analyzing software or firmware. The techniques taught will help reverse engineers to better answer questions and deobfuscate binaries.

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

COURSE DETAILS

AGENDA

SYMBOLIC EXECUTION CONCEPTS

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

FRAMEWORK INTRODUCTIONS

  • Introduction to a few useful Symbolic Execution Frameworks
  • Triton Introduction and Demos
  • Triton DSE Introduction and Demos
  • MAAT Introduction and Demos
  • Framework Comparisons

ANALYSIS INTRODUCTION

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

PATH EXPLORATION

  • Test Case Generation
  • Different Exploration Strategies
  • Exploration Heuristics

VULNERABILITY DETECTION

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

DEOBFUSCATION

  • Anti-Static Obfuscation defeat strategies
  • Anti-Dynamic Obfuscation defeat strategies

KNOWLEDGE PREQUISITES

  • Working knowledge of Python scripting
  • Understanding of X86_64 Binary Reversing
  • Familiarity with Memory Corruption Vulnerabilities

REQUIREMENTS

HARDWARE

  • A cloud instance will be provided to the students. They must have an internet connection to SSH into their cloud machine.

SOFTWARE

  • 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.

ABOUT THE TRAINER

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.