Selective Symbolic Execution
Vitaly Chipounov, Vlad Georgescu, Cristian Zamfir · Infoscience (Ecole Polytechnique Fédérale de Lausanne) · 2009
Symbolic execution is a powerful technique for analyz-ing program behavior, finding bugs, and generating tests, but suffers from severely limited scalability: the largest pro-grams that can be symbolically executed today are on the order of thousands of lines of code. To ensure feasibil-ity of symbolic execution, even small programs must cur-tail their interactions with libraries, the operating system, and hardware devices. This paper introduces selective sym-bolic 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 con-crete and back. Our technique makes symbolic execution practical for large software that runs in real environments, without requiring explicit modeling of these environments. 1