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

Field-sensitive Memory Model for Memory Safety of Heap-manipulating Programs

作　　者：董龙明[1] 王戟[1] 陈立前[1] 刘江潮[1] 

机构地区：[1]国防科技大学计算机学院并行与分布处理国家重点实验室,长沙410073

出　　处：《计算机科学》2012年第9期109-114,151,共7页Computer Science

基　　金：国家自然科学基金(61120106006;90818024)资助

摘　　要：堆操作程序具有通过共享易变数据结构动态操纵堆内存单元的特性,使得内存安全性难以保证。针对这个问题,提出了一种域敏感的k-limit内存抽象模型,以支持动态调整抽象的粒度,取得静态分析在精度和效率上的平衡。分别从框架、性质、操作方面介绍了该内存模型,然后结合内存安全性的定义,在基于该模型的操作语义框架内定义了4种与内存安全性相关的错误类型,最后设计了基于该模型内存安全性检测的数据流迭代算法。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内存抽象模型 动态可调节 

分 类 号：TP301[自动化与计算机技术—计算机系统结构]