一句话：提出延迟具体化算法与 symcrete 值，将符号执行中的具体化推迟到需要时，以减少路径发散并提高覆盖率。
符号执行中的具体化虽然能推进求解，但会导致覆盖率损失、路径发散以及无法复现目标缺陷的测试用例。本文提出延迟具体化（Deferred Concretization）算法，在符号执行中引入一类新的 symcrete 值，将具体化推迟到真正需要时再执行。作者实现了工具 COLOSSUS，并与当前先进的符号执行引擎 KLEE 进行对比评估。实验表明，COLOSSUS 平均提升覆盖率 66.94%，将路径发散降低超过 55%；同时能够恢复 KLEE 在符号执行树中丢失的约 38.60% 状态，说明其可覆盖更大的执行空间。
Concretization is an effective weapon in the armory of symbolic execution engines. However, concretization can lead to loss in coverage, path divergence, and generation of test-cases on which the intended bugs are not reproduced. In this paper, we propose an algorithm, Deferred Concretization, that uses a new category for values within symbolic execution (referred to as the symcrete values) to pend concretization till they are actually needed. Our tool, COLOSSUS, built around these ideas, was able to gain an average coverage improvement of 66.94% and reduce divergence by more than 55% relative to the state-of-the-art symbolic execution engine, KLEE. Moreover, we found that KLEE loses about 38.60% of the states in the symbolic execution tree that COLOSSUS is able to recover, showing that COLOSSUS is capable of covering a much larger coverage space.
DOI 原文 ·
@inproceedings{paperbot5386,
title = {Deferred concretization in symbolic execution via fuzzing},
author = {Awanish Pandey and Phani Raj Goutham Kotcharlakota and Subhajit Roy},
booktitle = {ISSTA},
year = {2019},
doi = {10.1145/3293882.3330554}
}