CRETE: A Versatile Binary-Level Concolic Testing Framework
CRETE: A Versatile Binary-Level Concolic Testing Framework
复制标题
DOI：
10.1007/978-3-319-89363-1_16
复制
发表时间：
2018-04
期刊：
影响因子：
--
通讯作者：
Bo Chen;Christopher Havlicek;Zhenkun Yang;Kai Cong;R. Kannavara;Fei Xie
中科院分区：
文献类型：
--
作者：
Bo Chen;Christopher Havlicek;Zhenkun Yang;Kai Cong;R. Kannavara;Fei Xie
在本文中，我们提出了一个通用的二进制级concolic测试框架crete，它具有开放和高度可扩展的架构，可以轻松集成具体执行前端和符号执行引擎后端。Crete的可扩展性源于其模块化设计，其中具体的和符号的执行仅通过标准化的执行跟踪和测试用例松散耦合。标准化的执行跟踪是基于llvm的、自包含的、可组合的，为符号执行引擎提供了简洁而充分的信息，以重现具体的执行。我们使用klee作为符号执行引擎和多个具体执行前端（如qemu和8051 Emulator）实现了具体执行。我们已经评估了crete在GNU coretils程序和UEFI BIOS的TianoCore实用程序上的有效性。对coretils程序的评估表明，crete实现了与直接分析coretils源代码的klee相当的代码覆盖率，并且总体上优于angr。对TianoCore实用程序的评估发现了许多以前未报告的可利用漏洞。
In this paper, we present crete, a versatile binary-level concolic testing framework, which features an open and highly extensible architecture allowing easy integration of concrete execution frontends and symbolic execution engine backends. crete’s extensibility is rooted in its modular design where concrete and symbolic execution is loosely coupled only through standardized execution traces and test cases. The standardized execution traces are llvm-based, self-contained, and composable, providing succinct and sufficient information for symbolic execution engines to reproduce the concrete executions. We have implemented crete with klee as the symbolic execution engine and multiple concrete execution frontends such as qemu and 8051 Emulator. We have evaluated the effectiveness of crete on GNU Coreutils programs and TianoCore utility programs for UEFI BIOS. The evaluation of Coreutils programs shows that crete achieved comparable code coverage as klee directly analyzing the source code of Coreutils and generally outperformed angr. The evaluation of TianoCore utility programs found numerous exploitable bugs that were previously unreported.