Automatic testing of symbolic execution engines via program generation and differential testing
Automatic testing of symbolic execution engines via program generation and differential testing
复制标题
DOI：
10.1109/ase.2017.8115669
复制
发表时间：
2017-10
期刊：
影响因子：
--
通讯作者：
Timotej Kapus;Cristian Cadar
中科院分区：
文献类型：
--
作者：
Timotej Kapus;Cristian Cadar
近年来，象征性执行引起了极大的关注，在软件测试，安全性，网络等方面的应用程序，例如Crest，Klee，Fuzzball和象征性的探路者，使研究人员和从业人员可以尝试新的想法在较大的应用程序上，将其应用于新的应用程序域。引擎使用的方法依赖于一种新颖的方式来创建程序版本，以结合结合，单路和多路径 - 在与现有的程序生成技术结合使用时，可以执行不同的功能。 ，这种方法可以在单个符号执行引擎中进行差异测试。 ，部门，模型，铸造，向量指令等，以及与约束解决，编译器优化和测试输入重播有关的问题。
Symbolic execution has attracted significant attention in recent years, with applications in software testing, security, networking and more. Symbolic execution tools, like CREST, KLEE, FuzzBALL, and Symbolic PathFinder, have enabled researchers and practitioners to experiment with new ideas, scale the technique to larger applications and apply it to new application domains. Therefore, the correctness of these tools is of critical importance. In this paper, we present our experience extending compiler testing techniques to find errors in both the concrete and symbolic execution components of symbolic execution engines. The approach used relies on a novel way to create program versions, in three different testing modes—concrete, single-path and multi-path—each exercising different features of symbolic execution engines. When combined with existing program generation techniques and appropriate oracles, this approach enables differential testing within a single symbolic execution engine. We have applied our approach to the KLEE, CREST and FuzzBALL symbolic execution engines, where it has discovered 20 different bugs exposing a variety of important errors having to do with the handling of structures, division, modulo, casting, vector instructions and more, as well as issues related to constraint solving, compiler optimisations and test input replay.