一句话：提出用符号地址替代具体地址的可重定位寻址模型，使已分配对象的内存表示可在分配后动态修改，提升符号执行效率。
现有符号执行引擎通过将内存对象与具体地址关联来建模内存空间，每个已分配对象的表示在其分配时即被确定。本文提出一种新的寻址模型：不再使用具体地址，而是使用符号地址，从而使已分配对象的底层表示在分配之后仍可被动态修改。作者在两个应用场景中展示了该模型的优势：动态的跨对象划分与对象内划分。前者说明新近提出的分段内存模型可得到改进——动态合并多个对象表示，而非依赖静态指针分析预先完成合并；后者说明可将大对象的表示拆分为多个更小的表示，从而降低数组理论约束的求解开销。初步结果表明，该方法能显著提升符号探索的整体有效性。
Symbolic execution (SE) is a widely used program analysis technique. Existing SE engines model the memory space by associating memory objects with concrete addresses, where the representation of each allocated object is determined during its allocation. We present a novel addressing model where the underlying representation of an allocated object can be dynamically modified even after its allocation, by using symbolic addresses rather than concrete ones. We demonstrate the benefits of our model in two application scenarios: dynamic inter- and intra-object partitioning. In the former, we show how the recently proposed segmented memory model can be improved by dynamically merging several object representations into a single one, rather than doing that a-priori using static pointer analysis. In the latter, we show how the cost of solving array theory constraints can be reduced by splitting the representations of large objects into multiple smaller ones. Our preliminary results show that our approach can significantly improve the overall effectiveness of the symbolic exploration.
DOI 原文 ·
@inproceedings{paperbot6031,
title = {Relocatable addressing model for symbolic execution},
author = {David Trabish and Noam Rinetzky},
booktitle = {ISSTA},
year = {2020},
doi = {10.1145/3395363.3397363}
}