一句话：提出作用域感知的差分模糊测试方法，检测符号执行引擎内部函数模型的正确性。
符号执行已成为基础性的程序分析技术，但其执行过程不可避免会遇到提供字符串处理等基本操作的内部函数（如库函数）。为兼顾可扩展性与兼容性，许多符号执行引擎会构造内部函数模型来抽象函数行为。由于构造模型复杂度高，开发者往往只对函数的部分行为建模，即只实现“已建模功能”。这些内部函数模型的正确性至关重要，因为其错误会影响符号执行的所有应用，例如缺陷检测与模型检测。本文提出 SEDiff，一种作用域感知的差分模糊测试方法，用于测试符号执行中的内部函数模型。其核心思路是通过差分方式暴露模型行为与真实函数行为之间的偏差，从而提升符号执行引擎的可靠性。摘要未给出具体实验设置与结果。
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.
DOI 原文 ·
@inproceedings{paperbot7002,
title = {SEDiff: scope-aware differential fuzzing to test internal function models in symbolic execution},
author = {Penghui Li and Wei Meng and Kangjie Lu},
booktitle = {FSE},
year = {2022},
doi = {10.1145/3540250.3549080}
}