Home // ICSEA 2015, The Tenth International Conference on Software Engineering Advances // View article

Dynamic Symbolic Execution using Eclipse CDT

Authors:
Andreas Ibing

Keywords: Testing; Program analysis; Symbolic execution.

Abstract:
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 input-dependent 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.

Pages: 280 to 285

Copyright: Copyright (c) IARIA, 2015

Publication date: November 15, 2015

Published in: conference

ISSN: 2308-4235

ISBN: 978-1-61208-438-1

Location: Barcelona, Spain

Dates: from November 15, 2015 to November 20, 2015