一句话：提出 MuSE，将约束求解与路径探索统一，一次求解探索多条路径以缓解符号执行的双重搜索问题。
符号执行面临路径爆炸与约束求解两大扩展性挑战。传统方法将路径探索与约束求解分离：前者搜索程序路径空间，后者以黑盒方式再次搜索以判定路径可行性，因此存在双重搜索问题。本文提出多路符号执行（MuSE），利用约束求解过程中的中间赋值生成新的程序输入，并将约束求解过程映射为符号执行的路径探索，从而在一次求解中探索多条路径。作者在基于 KLEE 和 JPF 的两个符号执行工具以及三种常用约束求解算法上实现了 MuSE，并在真实基准上开展广泛实验。结果表明，在达到相同覆盖率时，MuSE 可获得数量级加速。
Path explosion and constraint solving are two challenges to symbolic execution's scalability. Symbolic execution explores the program's path space with a searching strategy and invokes the underlying constraint solver in a black-box manner to check the feasibility of a path. Inside the constraint solver, another searching procedure is employed to prove or disprove the feasibility. Hence, there exists the problem of double searchings in symbolic execution. In this paper, we propose to unify the double searching procedures to improve the scalability of symbolic execution. We propose Multiplex Symbolic Execution (MuSE) that utilizes the intermediate assignments during the constraint solving procedure to generate new program inputs. MuSE maps the constraint solving procedure to the path exploration in symbolic execution and explores multiple paths in one time of solving. We have implemented MuSE on two symbolic execution tools (based on KLEE and JPF) and three commonly used constraint solving algorithms. The results of the extensive experiments on real-world benchmarks indicate that MuSE has orders of magnitude speedup to achieve the same coverage.
DOI 原文 ·
@inproceedings{paperbot6021,
title = {Multiplex symbolic execution},
author = {Yufeng Zhang and Zhenbang Chen and Ziqi Shuai and Tianqi Zhang and Kenli Li and Ji Wang},
booktitle = {ASE},
year = {2020},
doi = {10.1145/3324884.3416645}
}