一句话：提出有界符号大小模型与状态合并，缓解符号执行中具体大小导致的覆盖损失和路径爆炸。
现代符号执行工具通常对对象大小进行具体化建模，无法处理符号大小分配，迫使用户预先设定输入大小，容易导致具体化和覆盖率损失。本文提出有界符号大小模型：对象大小可取用户指定边界内的多个值。由于大小符号表达式增加，路径爆炸问题被放大；为此，作者提出基于状态合并的方法，通过特殊处理依赖符号大小的循环来减少分支。在真实世界基准测试中，该方法在性能与覆盖率上常取得显著提升，并发现此前未知的缺陷。
Symbolic execution is a powerful program analysis technique which allows executing programs with symbolic inputs. Modern symbolic execution tools use a concrete modeling of object sizes, that does not allow symbolic-size allocations. This leads to concretizations and enforces the user to set the size of the input ahead of time, thus potentially leading to loss of coverage during the analysis. We present a bounded symbolic-size model in which the size of an object can have a range of values limited by a user-specified bound. Unfortunately, this model amplifies the problem of path explosion, due to additional symbolic expressions representing sizes. To cope with this problem, we propose an approach based on state merging that reduces the forking by applying special treatment to symbolic-size dependent loops. In our evaluation on real-world benchmarks, we show that our approach can lead in many cases to substantial gains in terms of performance and coverage, and find previously unknown bugs.
DOI 原文 ·
@inproceedings{paperbot6363,
title = {A bounded symbolic-size model for symbolic execution},
author = {David Trabish and Shachar Itzhaky and Noam Rinetzky},
booktitle = {FSE},
year = {2021},
doi = {10.1145/3468264.3468596}
}