Technical Perspective: Veritesting Tackles Path-Explosion Problem

To view the accompanying paper, visit http://cacm.acm.org/magazines/2016/6/202649

Imagine you are working on a large piece of software for a safety-critical system, such as the braking system of a car. How would you make sure the car will not accelerate under any circumstance when the driver applies the brake? How would you know that someone other than the driver would not be able to stop a moving car by exploiting a remote security vulnerability in the software system? How would you confirm the braking system will not fail suddenly due to a fatal crash in the software system?

Testing is the only predominant technique used by the software industry to answer such questions and to make software systems reliable. Studies show that testing accounts for more than half of the total software development cost in industry. Although testing is a widely used and a well-established technique for building reliable software, existing techniques for testing are mostly ad hoc and ineffective—serious bugs are often exposed post-deployment. Wouldn’t it be nice if one could build a software system that could exhaustively test any software and report all critical bugs in the software to its developer?

In recent years, symbolic execution has emerged as one such automated technique to generate high-coverage test suites. Such test suites could find deep errors and security vulnerabilities in complex software applications. Symbolic execution analyzes the source code or the object code of a program to determine what inputs would execute the different paths of the program. The key idea behind symbolic execution was introduced almost 40 years ago. However, it has only recently been made practical, as a result of significant advances in program analysis and constraint-solving techniques, and due to the invention of dynamic symbolic execution (DSE) or concolic testing, which combines concrete and symbolic execution.

Since its introduction in 2005, DSE and concolic testing have inspired the development of several scalable symbolic execution tools such as DART, CUTE, jCUTE, KLEE, JPF, SAGE, PEX, CREST, BitBlaze, S2E, Jalangi, CATG, Triton, CONBOL, and SymDroid. Such tools have been used to find crashing inputs, to generate high-coverage test-suites, and to expose security vulnerabilities. For example, Microsoft’s SAGE has discovered one-third of all bugs revealed during the development of Windows 7.

Although modern symbolic execution tools have been successful in finding high-impact bugs and security vulnerabilities, it has been observed that symbolic execution techniques do not scale well to large realistic programs because the number of feasible execution paths of a program often increases exponentially with the length of an execution path. Therefore, most modern symbolic execution tools achieve poor coverage when they are applied to large programs. Most of the research in symbolic execution nowadays is, therefore, focusing on mitigating the path-explosion problem.

To mitigate the path-explosion problem, a number of techniques have been proposed to merge symbolic execution paths at various program points. Symbolic path merging, also known as static symbolic execution (SSE), enables carrying out symbolic execution of multiple paths simultaneously. However, this form of path merging often leads to large and complex formula that are difficult to solve. Moreover, path merging fails to work for real-world programs that perform system calls. Despite these recent proposals for mitigating the path explosion problem, the proposed techniques are not effective enough to handle large systems code.

The following work by Avgerinos et al. is a landmark in further addressing the path-explosion problem for real-world software systems. The authors have proposed an effective technique called veritesting that addresses the scalability limitations of path merging in symbolic execution. They have implemented veritesting in MergePoint, a tool for automatically testing all program binaries in a Linux distribution. A key attraction of MergePoint is that the tool can be applied to any binary without any source information or re-compilation or preprocessing or user-setup. A broader impact of this work is that users can now apply symbolic execution to larger software systems and achieve better code coverage while finding deep functional and security bugs.

Veritesting works by alternating between dynamic symbolic execution and path merging or static symbolic execution. DSE helps to handle program fragments that cannot be handled by SSE, such as program fragments making system calls and indirect jumps. SSE, on the other hand, helps to avoid repeated exploration of exponential number of paths in small program fragments by summarizing their behavior as a formula. What I find truly remarkable is this clever combination of DSE and SSE has enabled veritesting to scale to thousands of binaries in a Linux distribution. The tool has found more than 10,000 bugs in the distribution and Debian maintainers have already applied patches to 229 such bugs. These results and impact on real-world software have demonstrated that symbolic execution has come out of its infancy and has become a viable alternative for testing real-world software systems without user-intervention.