一句话：提出将符号执行状态记录到磁盘并选择性恢复路径的技术，使符号执行能够无限期运行。
符号执行在分析真实应用时，常常在较短时间内耗尽所有可用内存，导致无法长时间分析。本文提出一种技术，可将正在进行的符号执行分析记录到磁盘，并在之后选择性地恢复感兴趣的路径，从而使符号执行能够无限期运行。为实现这一目标，作者解决了若干关键研究挑战：检测重执行时的分歧、高效存储长时间运行的状态、在重执行时改变搜索启发式，以及提供存储执行的全局视图。对93个Linux应用的广泛评估表明，该方法切实可行，使这些应用能够运行数天并持续探索新的执行路径。
When symbolic execution is used to analyse real-world applications, it often consumes all available memory in a relatively short amount of time, sometimes making it impossible to analyse an application for an extended period. In this paper, we present a technique that can record an ongoing symbolic execution analysis to disk and selectively restore paths of interest later, making it possible to run symbolic execution indefinitely. To be successful, our approach addresses several essential research challenges related to detecting divergences on re-execution, storing long-running executions efficiently, changing search heuristics during re-execution, and providing a global view of the stored execution. Our extensive evaluation of 93 Linux applications shows that our approach is practical, enabling these applications to run for days while continuing to explore new execution paths.
DOI 原文 ·
@inproceedings{paperbot6028,
title = {Running symbolic execution forever},
author = {Frank Busse and Martin Nowack and Cristian Cadar},
booktitle = {ISSTA},
year = {2020},
doi = {10.1145/3395363.3397360}
}