Sydr: Cutting Edge Dynamic Symbolic Execution

TL;DR

Sydr enhances dynamic symbolic execution by introducing performance and accuracy improvements, including skipping non-symbolic instructions, formula simplification, and handling multi-threaded programs, leading to faster and more precise security analysis.

Contribution

The paper presents novel techniques for improving dynamic symbolic execution, integrated into the Sydr tool, with significant performance and accuracy gains for security applications.

Findings

Path predicate construction is 1.2--3.5 times faster.

Formula simplification improves symbolic execution efficiency.

Effective handling of multi-threaded programs enhances analysis accuracy.

Abstract

The security development lifecycle (SDL) is becoming an industry standard. Dynamic symbolic execution (DSE) has enormous amount of applications in computer security (fuzzing, vulnerability discovery, reverse-engineering, etc.). We propose several performance and accuracy improvements for dynamic symbolic execution. Skipping non-symbolic instructions allows to build a path predicate 1.2--3.5 times faster. Symbolic engine simplifies formulas during symbolic execution. Path predicate slicing eliminates irrelevant conjuncts from solver queries. We handle each jump table (switch statement) as multiple branches and describe the method for symbolic execution of multi-threaded programs. The proposed solutions were implemented in Sydr tool. Sydr performs inversion of branches in path predicate. Sydr combines DynamoRIO dynamic binary instrumentation tool with Triton symbolic engine. We evaluated Sydr features on 64-bit Linux executables.