Prototyping symbolic execution engines for interpreted languages
Prototyping symbolic execution engines for interpreted languages
复制标题
解释型语言的符号执行引擎原型
DOI：
--
复制
发表时间：
2014
期刊：
影响因子：
--
通讯作者：
George Candea
中科院分区：
文献类型：
--
作者：
Stefan Bucur;Johannes Kinder;George Candea
符号执行被成功地用于自动测试静态编译的代码。然而，越来越多的系统和应用程序是用Python等动态解释语言编写的。构建一个新的符号执行引擎是一项巨大的工作，随着目标语言的发展，保持它的更新也是如此。此外，模糊的语言规范导致它们在符号执行引擎中的实现可能以微妙的方式与生产解释器不同。我们通过翻转问题并使用解释器本身作为语言语义的规范来解决这些挑战。我们提出了一个食谱和工具（称为厨师），把香草解释器变成一个声音和完整的符号执行引擎。Chef象征性地执行目标程序，通过象征性地执行解释器的二进制文件，同时利用有关程序高级结构的推断知识。使用Chef，我们在5个人天内为Python开发了一个符号执行引擎，在3个人天内为Lua开发了一个符号执行引擎。它们以接近零成本的方式提供完整和忠实的语言功能，与未来的语言版本保持一致。Chef生成的引擎的性能比直接执行没有Chef的解释器要高出1000倍。
Symbolic execution is being successfully used to automatically test statically compiled code. 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 person-days. 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 times more performant than if directly executing the interpreter symbolically without Chef.