一句话：提出待定约束技术，优先探索已知可行的路径、推迟其余路径，提升符号执行的可扩展性与覆盖率。
符号执行是软件测试与分析中的成熟技术，但其可扩展性始终受限于约束求解开销与路径爆炸两大难题。本文提出一种新的符号执行方法：将可行性尚未确认的路径对应的约束视为「待定约束」并推迟其探索，从而激进地优先执行那些已知可行的路径，把有限的计算资源集中在更有希望的分支上。作者在 SQLite3、make 和 tcpdump 等九个真实应用上进行了评估，结果表明该技术在有种子与无种子两种探索模式下均能取得更高的覆盖率。
Symbolic execution is a well established technique for software testing and analysis. However, scalability continues to be a challenge, both in terms of constraint solving cost and path explosion. In this work, we present a novel approach for symbolic execution, which can enhance its scalability by aggressively prioritising execution paths that are already known to be feasible, and deferring all other paths. We evaluate our technique on nine applications, including SQLite3, make and tcpdump and show it can achieve higher coverage for both seeded and non-seeded exploration.
DOI 原文 ·
@inproceedings{paperbot5977,
title = {Pending constraints in symbolic execution for better exploration and seeding},
author = {Timotej Kapus and Frank Busse and Cristian Cadar},
booktitle = {ASE},
year = {2020},
doi = {10.1145/3324884.3416589}
}