一句话：在 KLEE 中提出细粒度内存对象表示，大幅降低符号执行状态的内存占用并显著加速。
动态符号执行（DSE）能自动检查程序中的错误模式，但其最大挑战是状态空间爆炸：DSE 需为每条执行路径表示已分配内存及其访问，并行分析大量状态。状态过多时无法全部驻留内存，只能提前终止或中途转存磁盘。本文提出一种细粒度、高效的内存表示，模仿被测程序的实际分配行为，从而在同等内存下容纳更多状态。作者在符号执行引擎 KLEE 之上实现该表示，并以三种搜索策略（DFS、BFS、覆盖率）在 Coreutils 上进行评测。结果显示，状态内存消耗最多降低 99.06%（均值 DFS 2%、BFS 51%、Cov. 49%），总执行时间最多降低 97.81%（均值 DFS 9%、BFS 7%、Cov. 4%），相比基线 KLEE 最高取得 49 倍加速。
Dynamic Symbolic Execution (DSE) has seen rising popularity as it allows to check applications for behaviours such as error patterns automatically. One of its biggest challenges is the state space explosion problem: DSE tries to evaluate all possible execution paths of an application. For every path, it needs to represent the allocated memory and its accesses. Even though different approaches have been proposed to mitigate the state space explosion problem, DSE still needs to represent a multitude of states in parallel to analyse them. If too many states are present, they cannot fit into memory, and DSE needs to terminate them prematurely or store them on disc intermediately. With a more efficient representation of allocated memory, DSE can handle more states simultaneously, improving its performance. In this work, we introduce an enhanced, fine-grain and efficient representation of memory that mimics the allocations of tested applications. We tested Coreutils using three different search strategies with our implementation on top of the symbolic execution engine KLEE. We achieve a significant reduction of the memory consumption of states by up to 99.06% (mean DFS: 2%, BFS: 51%, Cov.: 49%), allowing to represent more states in memory more efficiently. The total execution time is reduced by up to 97.81% (mean DFS: 9%, BFS: 7%, Cov.:4%)-a speedup of 49x in comparison to baseline KLEE.
DOI 原文 ·
@inproceedings{paperbot5243,
title = {Fine-Grain Memory Object Representation in Symbolic Execution},
author = {Martin Nowack},
booktitle = {ASE},
year = {2019},
doi = {10.1109/ase.2019.00089}
}