Dynamic Symbolic Execution Using Eclipse CDT

Finding software bugs before deployment is essential to achieve software safety and security. The achievable code coverage and input coverage with manual test suite development at reasonable cost is limited. Therefore, complementary automated methods for bug detection are of interest. This paper describes automated context-sensitive detection of software bugs with dynamic symbolic execution. The program under test is executed in a debugger, and program execution is automatically driven into all program paths that are satisfiable with any program input. Program input and dependent data are treated as symbolic variables. Dynamic analysis and consistent partial static analysis are combined to automatically detect both inputdependent and input-independent bugs. The implementation is a plug-in extension of the Eclipse C/C++ development tools. It uses Eclipse’s code analysis framework, its debugger services framework and a Satisfiability Modulo Theories automated theorem prover. The resulting dynamic symbolic execution engine allows for consistent partially concrete program execution. Compared to static symbolic execution, it transfers as much work as possible to concrete execution in a debugger, without losing bug detection accuracy. The engine is evaluated in terms of bug detection accuracy and runtime on buffer overflow test cases from the Juliet test suite for program analyzers. Keywords–Testing; Program analysis; Symbolic execution.