Multi-Pass Targeted Dynamic Symbolic Execution

TL;DR

This paper introduces a Multi-Pass Targeted Dynamic Symbolic Execution method that enhances program analysis by reducing path explosion and improving bug detection efficiency through backward and forward reasoning, implemented in the DESTINA tool.

Contribution

It proposes a novel multi-pass approach combining backward and forward reasoning with an abstract address space to improve targeted symbolic execution.

Findings

DESTINA detects memory vulnerabilities precisely.

It reduces path exploration by 4X on average.

It speeds up analysis by 2X on average.

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.