Multi-Pass Targeted Dynamic Symbolic Execution

TL;DR

This work addresses the path explosion problem in dynamic symbolic execution by introducing Multi-Pass Targeted Dynamic Symbolic Execution (MPBSE), which starts analysis from a program target and moves backward toward an entry point. Implemented as DESTINA on top of KLEE, it uses a byte-precise abstract address space and unification to map abstract objects to concrete memory, enabling precise detection of memory vulnerabilities and generation of replay constraints to guide forward exploration. Empirical evaluation on SvComp benchmarks shows DESTINA achieves significant improvements, including an average 4x reduction in explored paths and 2x speedups when guiding DSE toward targets, while maintaining precise memory error detection (e.g., NULL dereferences, OOB, use-after-free). The approach supports pointer arithmetic and dynamic memory, providing a practical tool for targeted bug finding and test generation with potential integration into standard symbolic execution pipelines. Overall, DESTINA demonstrates that backward-targeted reasoning coupled with forward unification can tightly couple reachability analysis with memory modeling to enhance both precision and efficiency in DSE.

Abstract

Dynamic symbolic execution (DSE) provides a precise means to analyze programs and it can be used to generate test cases and to detect a variety of bugs including memory vulnerabilities. However, the path explosion problem may prevent a symbolic executor from covering program locations or paths of interest. In this paper, we present a Multi-Pass Targeted Dynamic Symbolic Execution approach that starts from a target program location and moves backward until it reaches a specified entry point to check for reachability, to detect bugs on the feasible paths between the entry point and the target, and to collect constraints about the memory locations accessed by the code. Our approach uses a mix of backward and forward reasoning passes. It introduces an abstract address space that gets populated during the backward pass and uses unification to precisely map the abstract objects to the objects in the concrete address space. We have implemented our approach in a tool called DESTINA using KLEE, a DSE tool. We have evaluated DESTINA using SvComp benchmarks from the memory safety and control-flow categories. Results show that DESTINA can detect memory vulnerabilities precisely and it can help DSE reach target locations faster when it struggles with the path explosion. Our approach achieves on average 4X reduction in the number of paths explored and 2X speedup.

Figures (4)

• Figure 1: A path explosion example with a NULL pointer dereferencing error. W and Y are symbolic.
• Figure 2: Syntax for a simple while language with pointers.
• Figure 3: An example that involves pointers and aliasing.
• Figure 4: $\textit{PointerExecuteBackward}$ ($\textit{PEB}$): Backward Symbolic Execution operational semantic with respect to pointer related side effects on $(\mathcal{O},\Phi,\mathcal{U})$. $\textbf{A}(e)$ is a shorthand notation for $A(B,e)$ (see Table \ref{['table:addressexp']}). $\textit{PEB}(B)$ is a shorthand notation for $\textit{PEB}(B,\textit{CS})$ for the syntax specified as $[E:\textit{CS}]$ or $[S:\textit{CS}]$ for expressions or statements, respectively. $\textit{Uop}$ and $\textit{Bop}$ denote unary and binary arithmetic, relational, or logical operators, respectively.

Theorems & Definitions (4)

• Lemma 1: Def-Use Correctness
• proof
• Theorem 1: Soundness
• proof