一种面向堆操作程序内存安全性的域敏感内存模型

摘要

Heap-manipulating programs usually operate memory cells directly through shared and mutable data-structures, which makes their memory safety more complex and harder to guarantee, A field-sensitive k-limit abstract memory model was proposed in this paper to support dynamic adjustment of the precision and efficiency of the analysis . We presented its framework, property and operations. And then, four kinds of memory-related errors were identified in the operational semantics of the abstract memory model according to the definition of memory safety. In the end, we proposed the dataflow iteration algorithm for detecting the memory safety of C programs.%堆操作程序具有通过共享易变数据结构动态操纵堆内存单元的特性,使得内存安全性难以保证.针对这个问题,提出了一种域敏感的k-limit内存抽象模型,以支持动态调整抽象的粒度,取得静态分析在精度和效率上的平衡.分别从框架、性质、操作方面介绍了该内存模型,然后结合内存安全性的定义,在基于该模型的操作语义框架内定义了4种与内存安全性相关的错误类型,最后设计了基于该模型内存安全性检测的数据流迭代算法.