一种用于指针程序安全性证明的指针逻辑

摘要：

在高可信软件的各种性质中,安全性是被关注的重点,其中软件满足安全策略的证明方法是研究的热点之一.文中根据作者所设想的安全程序的设计和证明框架,为类C语言的一个子集设计了一个指针逻辑系统.该逻辑系统是Hoare逻辑系统的一种扩展,它用推理规则来表达每一种语句引起指针信息的变化情况.它可用来对指针程序进行精确的指针分析,所获得的信息用来证明指针程序是否满足定型规则的附加条件,以支持程序的安全性验证.该逻辑系统也可用来证明指针程序的其它性质.

关键词：软件安全、指针逻辑、Hoare逻辑、指针分析、类型系统

所属期刊栏目：31

分类号：TP301(计算技术、计算机技术)

资助基金：国家自然科学基金60673126

在线出版日期：2008-05-26（万方平台首次上网日期，不代表论文的发表时间）

页数：共9页

页码：372-380