Prototyping Symbolic Execution Engines for Interpreted Languages

摘要

Symbolic execution is being successfully used to automatically test statically compiled code [4, 7, 9, 15]. However, increasingly more systems and applications are written in dynamic interpreted languages like Python. Building a new symbolic execution engine is a monumental effort, and so is keeping it up-to-date as the target language evolves. Furthermore, ambiguous language specifications lead to their implementation in a symbolic execution engine potentially differing from the production interpreter in subtle ways. We address these challenges by flipping the problem and using the interpreter itself as a specification of the language semantics. We present a recipe and tool (called CHEF) for turning a vanilla interpreter into a sound and complete symbolic execution engine. CHEF symbolically executes the target program by symbolically executing the interpreter's binary while exploiting inferred knowledge about the program's high-level structure. Using CHEF, we developed a symbolic execution engine for Python in 5 person-days and one for Lua in 3 persondays. They offer complete and faithful coverage of language features in a way that keeps up with future language versions at near-zero cost. CHEF-produced engines are up to 1000× more performant than if directly executing the interpreter symbolically without CHEF.