Selective Symbolic Execution

Symbolic execution is a powerful technique for analyzing program behavior, finding bugs, and generating tests, but suffers from severely limited scalability: the largest programs that can be symbolically executed today are on the order of thousands of lines of code. To ensure feasibility of symbolic execution, even small programs must curtail their interactions with libraries, the operating system, and hardware devices. This paper introduces selective symbolic execution, a technique for creating the illusion of full-system symbolic execution, while symbolically running only the code that is of interest to the developer. We describe a prototype that can symbolically execute arbitrary portions of a full system, including applications, libraries, operating system, and device drivers. It seamlessly transitions back and forth between symbolic and concrete execution, while transparently converting system state from symbolic to concrete and back. Our technique makes symbolic execution practical for large software that runs in real environments, without requiring explicit modeling of these environments.