Home // SECURWARE 2014, The Eighth International Conference on Emerging Security Information, Systems and Technologies // View article

A Backtracking Symbolic Execution Engine with Sound Path Merging

Authors:
Andreas Ibing

Keywords: static analysis, symbolic execution

Abstract:
Software vulnerabilities are a major security threat and can often be exploited by an attacker to intrude into systems. One approach to mitigation is to automatically analyze software source code in order to find and remove software bugs before release. A method for context-sensitive static bug detection is symbolic execution. If applied with approximate path coverage, it faces the state explosion problem. The number of paths in the program execution tree grows exponentially with the number of decision nodes in the program for which both branches are satisfiable. In combination with the standard approach using the worklist algorithm with state cloning, this also leads to exponential memory consumption during analysis. This paper considers a source-level symbolic execution engine which uses backtracking of symbolic states instead of state cloning, and extends it with a sound method for merging redundant program paths, based on live variable analysis. An implementation as plug-in extension of the Eclipse C/C++ development tools (CDT) is described. The resulting analysis speedup through path merging is evaluated on the buffer overflow test cases from the Juliet test suite for static analyzers on which the original engine had been evaluated.

Pages: 180 to 185

Copyright: Copyright (c) IARIA, 2014

Publication date: November 16, 2014

Published in: conference

ISSN: 2162-2116

ISBN: 978-1-61208-376-6

Location: Lisbon, Portugal

Dates: from November 16, 2014 to November 20, 2014