Symbolic execution for testing complex software

This dissertation presents a novel symbolic execution technique for comprehensively testing complex software. The main insight behind our technique is that code can automatically generate its own (potentially highly complex) test cases. To this end, the code is run on symbolic input, whose value is initially unconstrained. As the checked code runs, we track the constraints on each memory location whose value depends on the symbolic input. If the code reaches a branch involving such a memory location and both sides are feasible, we fork execution and follow each path, constraining the expression to be true on the true path and false on the other. When a path terminates or hits a bug, we can automatically generate a test case exercising that path by solving the current path constraints for concrete values. By keeping track of the exact constraints on each explored path, our technique gains the ability to reason about all possible values on these paths, and thus can be effectively used to find deep errors. At potentially dangerous operations (e.g., a pointer dereference), our technique can detect if the current path constraints allow any values that cause a bug. This is a significant advantage over traditional dynamic execution techniques, which can only detect an error if they are provided with a specific test case that triggers it (e.g., one where the pointer value is out-of-bounds). We present two main systems based on this technique, EXE and KLEE, and show that they can automatically generate high-coverage test suites and find deep errors in a variety of complex applications, ranging from user-level utilities to network servers, device drivers, packet filters and file systems. For example, we apply KLEE to all 89 stand-alone applications in the GNU C OREUTILS suite, which forms the core user-level environment installed on millions of UNIX systems, and is arguably one of the most heavily tested sets of open-source programs in existence. KLEE-generated test suites achieve on average over 90% line coverage, significantly beating the coverage of an extensive manual test suite built incrementally over a period of more than fifteen years. As an additional illustrative example we use EXE to mount attacks against file systems code, by automatically generating raw ext2, ext3 and JFS disk images that cause the kernel to panic when mounted under LINUX.