Field-sensitive Memory Model for Memory Safety of Heap-manipulating Programs
一种面向堆操作程序内存安全性的域敏感内存模型

Heap-manipulating programs usually operate memory cells directly through shared and mutable data-struc- tures,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 pro- posed the dataflow iteration algorithm for detecting the memory safety of C programs.