SEDiff: scope-aware differential fuzzing to test internal function models in symbolic execution
SEDiff: scope-aware differential fuzzing to test internal function models in symbolic execution
复制标题
DOI：
10.1145/3540250.3549080
复制
发表时间：
2022-11
期刊：
影响因子：
--
通讯作者：
Penghui Li;W. Meng;Kangjie Lu
中科院分区：
文献类型：
--
作者：
Penghui Li;W. Meng;Kangjie Lu
符号执行已经成为一种基本的程序分析技术。执行符号执行不可避免地会遇到提供诸如字符串处理等基本操作的内部函数(例如，库函数)。许多符号执行引擎构建内部函数模型，以抽象出于可伸缩性和兼容性考虑的函数行为。由于构建模型的高度复杂性，开发人员故意只总结模型中功能的部分行为，即建模功能。内部函数模型的正确性至关重要，因为它会影响符号执行的所有应用，例如错误检测和模型检查。测试内部功能模型的正确性的一个天真的解决方案是交叉检查模型的行为是否符合其对应的原始功能实现。然而，这样的解决方案主要会检测到关于未建模功能的压倒性不一致，这些功能不在模型的范围内，因此被认为是虚假报告。我们认为，合理的测试方法应该只针对开发人员打算建模的功能。虽然有必要，但自动识别建模的功能，即范围，是一个巨大的挑战。在本文中，我们提出了一个基于作用域的差异测试框架SEDiff来解决这个问题。我们设计了一种新的算法来自动将建模的功能映射到原始实现中的代码。然后，SEDiff将作用域感知灰盒差分模糊应用于原始实现中的相关代码。它还配备了一个新的作用域感知输入生成器和一个定制的错误检查器，可以有效和正确地检测错误的不一致。我们在针对二进制、Web和内核的几个流行的现实符号执行引擎上对SEDiff进行了广泛的评估。我们的人工调查表明，SEDiff准确地识别了建模的功能，并在符号执行引擎中使用的内部函数模型中检测到46个新的错误。
Symbolic execution has become a foundational program analysis technique. Performing symbolic execution unavoidably encounters internal functions (e.g., library functions) that provide basic operations such as string processing. Many symbolic execution engines construct internal function models that abstract function behaviors for scalability and compatibility concerns. Due to the high complexity of constructing the models, developers intentionally summarize only partial behaviors of a function, namely modeled functionalities, in the models. The correctness of the internal function models is critical because it would impact all applications of symbolic execution, e.g., bug detection and model checking. A naive solution to testing the correctness of internal function models is to cross-check whether the behaviors of the models comply with their corresponding original function implementations. However, such a solution would mostly detect overwhelming inconsistencies concerning the unmodeled functionalities, which are out of the scope of models and thus considered false reports. We argue that a reasonable testing approach should target only the functionalities that developers intend to model. While being necessary, automatically identifying the modeled functionalities, i.e., the scope, is a significant challenge. In this paper, we propose a scope-aware differential testing framework, SEDiff, to tackle this problem. We design a novel algorithm to automatically map the modeled functionalities to the code in the original implementations. SEDiff then applies scope-aware grey-box differential fuzzing to relevant code in the original implementations. It also equips a new scope-aware input generator and a tailored bug checker that efficiently and correctly detect erroneous inconsistencies. We extensively evaluated SEDiff on several popular real-world symbolic execution engines targeting binary, web and kernel. Our manual investigation shows that SEDiff precisely identifies the modeled functionalities and detects 46 new bugs in the internal function models used in the symbolic execution engines.