一种用于类C语言环境的安全的类型化内存模型  

A Kind of Safe Typed Memory Model for C-Like Languages

作　　者：何炎祥[1,2] 吴伟[2] 陈勇[2] 李清安[2] 刘健博[2] 

机构地区：[1]武汉大学计算机学院,武汉430072 [2]武汉大学软件工程国家重点实验室,武汉430072

出　　处：《计算机研究与发展》2012年第11期2440-2449,共10页Journal of Computer Research and Development

基　　金：国家自然科学基金项目(90818018;91018009)

摘　　要：使用形式化方法对程序进行验证是保证软件可信的重要手段.对于像C语言这样的较低级的命令式语言可以直接对内存进行操作,对其操作语义或公理语义的形式化需要基于合适的内存模型.传统的字节内存模型可以很好地描述各种内存操作,但是无法保证安全性,同时使程序验证变得异常复杂.面向对象语言的内存模型则具有较高的抽象性,便于程序验证,但不适合描述低级的内存操作.结合字节内存模型和面向对象语言内存模型,提出一种安全的类型化的内存模型,既可用于对语义的形式化,也可用于基于霍尔逻辑的程序验证.此内存模型既允许指针算术、结构赋值、类型转换等内存操作,同时也可以有效减少因指针别名给程序验证带来的复杂度.基于Coq辅助定理证明工具,对内存模型进行了形式化实现和验证.Verifying program by formal method is an important way to ensure software trusted. For low level imperative language like C language which can operate memory directly, a suitable memory model is needed to formalize the operational semantics or axiomatic semantics. The traditional byte memory model can describe various memory operations very well, however, it can＇t guarantee safety and make program-verifying complex. The memory model of object oriented language is high-level. It is suitable for program verification but not for describing low level memory operation. A safe typed memory model is proposed by combining the previous two kind models. It can be used to formalize semantics and to verify program based on Hoare logic. This memory model allows pointer arithmetic, structure assignment, type cast and other memory operations, and makes pointer-based programs verification easier. The memory model is formalized and verified using Coq proof assistant.

关 键 词：操作语义 形式化验证 内存模型 霍尔逻辑 内存安全 

分 类 号：TP311.52[自动化与计算机技术—计算机软件与理论]