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

A Pointer Logic for Safety Verification of Pointer Programs

作　　者：陈意云[1,2] 华保健[1,2] 葛琳[1,2] 王志芳[1,2] 

机构地区：[1]中国科学技术大学计算机科学与技术系,合肥230026 [2]中国科学技术大学苏州研究院软件安全实验室,江苏苏州215123

出　　处：《计算机学报》2008年第3期372-380,共9页Chinese Journal of Computers

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

摘　　要：在高可信软件的各种性质中,安全性是被关注的重点,其中软件满足安全策略的证明方法是研究的热点之一.文中根据作者所设想的安全程序的设计和证明框架,为类C语言的一个子集设计了一个指针逻辑系统.该逻辑系统是Hoare逻辑系统的一种扩展,它用推理规则来表达每一种语句引起指针信息的变化情况.它可用来对指针程序进行精确的指针分析,所获得的信息用来证明指针程序是否满足定型规则的附加条件,以支持程序的安全性验证.该逻辑系统也可用来证明指针程序的其它性质.Safety is an important issue among the properties of high-assurance software and developing the verification methods for software to meet safety policies is one of the hot research. In terms of the authors＇ sketch of design and verification of safety programs, a pointer logic system is designed for a subset of C-like language. This logic system is an extension of Hoare logic system and inference rules are designed to express the modification of pointer information for every kind of statements. It can be used for accurate pointer analysis of pointer programs. The information from the analysis can be used to verify if pointer programs satisfy the side conditions of typing rules and then support safety verification for programs. The logic system can also be used to verify other properties of pointer programs.

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

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