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

一种用于指针程序安全性证明的指针逻辑
陈意云华保健葛琳王志芳
(中国科学技术大学计算机科学与技术系,合肥 230026)
(中国科学技术大学苏州研究院软件安全实验室,苏州 215123)
摘要:在高可信软件的各种性质中,安全性是关注的重点,其中软件满足安全策略的证明方法是研究的热点之一。本文根据我们所设想的安全程序的设计和证明框架,为类C语言的一个子集设计了一个指针逻辑系统。该逻辑系统是Hoare逻辑系统的一种扩展,它用推理规则来表达每一种语句引起指针信息的变化情况。它可用来对指针程序进行精确的指针分析,所获得信息用来证明指针程序是否满足定型规则的附加条件,以支持程序的安全性验证。该逻辑系统也可用来证明指针程序的其它性质。
关键词: 软件安全,指针逻辑,Hoare逻辑,指针分析,类型系统
中图法分类号:TP301
1 引言
在高可信的各种要求中,安全性(包括safety和security)是关注的重点。Safety是指软件运行时不引起危险、灾难的能力,而security是指软件系统对数据和信息提供保密性、完整性、可用性、真实性保障的能力。本文所讲的安全性主要是指safety,但是软件的safety和security是有联系的,黑客通常就是利用缓冲区溢出、数组访问越界、悬空指针访问等低级的safety错误,来破坏系统和获取未经授权的控制等。因此提高safety有助于保证security。
程序性质证明(而不是历史上的程序正确性证明)领域近十年来有了很大的发展,许多学者提出了不同的思路,这些思路主要采取基于类型的或基于逻辑的方法,用于高级语言程序或低级语言程序的性质证明。基于类型方法的典型研究有类型化汇编语言(Typed Assembly Language)[1]和类型细化(type refinement)理论[2]的研究。基于逻辑方法的典型研究有携带证明的代码(Proof-Carrying Code,)[3](Foundational Proof-Carrying Code)框架[4]。Zhong Shao的携带证明汇编编程项目CAP(Certified Assembly Programming)[5]和基于栈的CAP(SCAP)[6]是典型的基于逻辑的研究项目。基于逻辑的方法和基于类型论的方法有很大的互补性,近年来出现了一些结合这两种方法的研究。一种结合两者的研究是Hongwei Xi等进行的ATS(Applied Type System)项目的研究[7],他们扩展类型系统,将程序状态引入类型系统,依靠ATS与Hoare逻辑的相似性,以ATS来编码Hoare逻辑,从而可以在他们的类型系统上模拟Hoare 逻辑的推理。
在国际上这些研究的基础上,我们认为,对于那些有高安全性要求的软件,程序设计和证明的一种新方式将是:
(1)程序设计者将软件的安全策略等描述成程序应满足的规范,连同程序一起提交给编译器;
(2)编译器生成为证明程序满足规范所需的验证条件,并且利用内嵌的定理证明器自动地或交互地证明这些验证条件;
(3)编译器在把源程序翻译成目标代码的同时,将源程序满足规范的证明翻译成目标代码满足等效规范的证明,这样的编译器称为出具证明的编译器(piler);
(4)在目标代码一级由证明检验器利用代码所携带的证明自动进行代码满足