Facebook-f Twitter Youtube Linkedin
Cart

Practical Symbolic Execution for VR and RE

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.

EUR $4,299.00

REGISTER
Attend In-person

Duration

4 days

Delivery Method

in-person

Level

intermediate

Seats Available

20

Duration

4 days

Delivery Method

in-person

Level

intermediate

ATTEND IN-PERSON: Onsite in Amsterdam

DATE: 17-20 April 2023

TIME: 09:00 to 17:00 CEST/GMT+2

Date Day Time Duration
17 Apr Monday 09:00 to 17:00 CEST/GMT+2 8 Hours – Presentations & Hands-on exercises
18 Apr Tuesday 09:00 to 17:00 CEST/GMT+2 8 Hours – Presentations & Hands-on exercises
19 Apr Wednesday 09:00 to 17:00 CEST/GMT+2 8 Hours – Presentations & Hands-on exercises
20 Apr Thursday 09:00 to 17:00 CEST/GMT+2 8 Hours – Presentations & Hands-on exercises

 

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.

 

Topics Covered
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
  • 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

Why You Should Take This Course

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.

Who Should Attend

  • Those who have some experience finding vulnerabilities and want to be able to write custom tooling to aid their discovery process.
  • Researchers who want to be able to better reason about the properties of an opaque executable.
  • Analysts who work with obfuscated code and want better inspection abilities.

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

    • Prerequisite Knowledge

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

    Hardware / Software Requirements

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

    Your Instructor

    Jordan Whitehead

    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.

    HACK IN THE BOX LIMITED

    Masdar City, United Arab Emirates