SEDiff: scope-aware differential fuzzing to test internal function models in symbolic execution
Penghui Li, Wei Meng, Kangjie Lu · Proceedings of the 30th ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering · 2022
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.