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

1一种用于指针程序安全性证明的指针逻辑陈意云华保健葛琳王志芳（中国科学技术大学计算机科学与技术系，合肥230026）（中国科学技术大学苏州研究院软件安全实验室，苏州215123）摘要：在高可信软件的各种性质中，安全性是关注的重点，其中软件满足安全策略的证明方法是研究的热点之一。本文根据我们所设想的安全程序的设计和证明框架，为类C语言的一个子集设计了一个指针逻辑系统。该逻辑系统是Hoare逻辑系统的一种扩展，它用推理规则来表达每一种语句引起指针信息的变化情况。它可用来对指针程序进行精确的指针分析，所获得信息用来证明指针程序是否满足定型规则的附加条件，以支持程序的安全性验证。该逻辑系统也可用来证明指针程序的其它性质。关键词：软件安全，指针逻辑，Hoare逻辑，指针分析，类型系统中图法分类号：TP3011引言在高可信的各种要求中，安全性（包括safety和security）是关注的重点。Safety是指软件运行时不引起危险、灾难的能力，而security是指软件系统对数据和信息提供保密性、完整性、可用性、真实性保障的能力。本文所讲的安全性主要是指safety，但是软件的safety和security是有联系的，黑客通常就是利用缓冲区溢出、数组访问越界、悬空指针访问等低级的safety错误，来破坏系统和获取未经授权的控制等。因此提高safety有助于保证security。程序性质证明（而不是历史上的程序正确性证明）领域近十年来有了很大的发展，许多学者提出了不同的思路，这些思路主要采取基于类型的或基于逻辑的方法，用于高级语言程序或低级语言程序的性质证明。基于类型方法的典型研究有类型化汇编语言（TypedAssemblyLanguage）[1]和类型细化（typerefinement）理论[2]的研究。基于逻辑方法的典型研究有携带证明的代码（Proof-CarryingCode，简称PCC）[3]和FPCC（FoundationalProof-CarryingCode）框架[4]。ZhongShao的携带证明汇编编程项目CAP（CertifiedAssemblyProgramming）[5]和基于栈的CAP（SCAP）[6]是典型的基于逻辑的研究项目。基于逻辑的方法和基于类型论的方法有很大的互补性，近年来出现了一些结合这两种方法的研究。一种结合两者的研究是HongweiXi等进行的ATS（AppliedTypeSystem）项目的研究[7]，他们扩展类型系统，将程序状态引入类型系统，依靠ATS与Hoare逻辑的相似性，以ATS来编码Hoare逻辑，从而可以在他们的类型系统上模拟Hoare逻辑的推理。在国际上这些研究的基础上，我们认为，对于那些有高安全性要求的软件，程序设计和证明的一种新方式将是：（1）程序设计者将软件的安全策略等描述成程序应满足的规范，连同程序一起提交给编译器；（2）编译器生成为证明程序满足规范所需的验证条件，并且利用内嵌的定理证明器自动地或交互地证明这些验证条件；（3）编译器在把源程序翻译成目标代码的同时，将源程序满足规范的证明翻译成目标代码满足等效规范的证明，这样的编译器称为出具证明的编译器（certifyingcompiler）；（4）在目标代码一级由证明检验器利用代码所携带的证明自动进行代码满足规范的检验。该框架的优点是，它向程序设计者提供源级而不是目标级的程序性质证明方法，以提高安全程序的开发效率，同时它将编译器、证明器等排除出受信任的计算基础（TrustedComputingBase，简称TCB），以尽量缩小系统的TCB。本文介绍我们在这个框架的初步实现中，为类C语言的一个子集PointerC设计的一个指针逻辑系统，它是Hoare逻辑的一种扩展，本质上是一种精确的指针分析（pointeranalysis）工具。它可用来从前向后收集各指针是NULL指针、悬空指针（danglingpointer）还是有效指针（有指向对象的指针）的信息，收集各有效指针之间相等与否的信息。所收集信息用来证明指2针程序是否满足定型规则（typingrule）的附加条件，以支持对指针程序的安全性验证及其它性质的验证。本文的组织如下：第二节介绍有关指针安全的一些基本概念，第三节是指针逻辑的设计，第四节给出一个证明实例，第五节是相关工作比较，第六节是总结。2基本知识首先介绍PointerC在指针运算方面的限制。在PointerC中，指针类型的变量只能用于赋值、相等和不相等比较、存取指向对象等运算以及作为函数（包括free）的参数，指针算术和取地址运算（&）被禁止。malloc和free被看成是PointerC预定义的函数，并且满足安全程序的最基本要求。例如malloc任何一次调用都能成功并且所分配空间同尚未释放空间无任何重叠。上述限制的目的是为了便于静态检查程序的安全性。程序运行时出现对NULL指针或悬空指针进行存取指向对象的操作、把NULL指针或悬空指针作为free函数调用的实在参数、发生内存泄漏等都被认为不满足基本安全策略（类型安全和内存安全等）。该语言定型规则中的附加条件就是用来禁止这些情况的出现，本文指针逻辑的用途之一就是用来完成对这些附加条件的静态检查。下面明确本文有关指针类型的一些术语和约定。程序中显式声明的变量称为声明变量，由malloc函数显式和动态分配的空间称为动态对象。在程序中，动态对象的域只能通过指针类型的声明变量来访问，如s-data、和s-next-prior等，这种把脱引用（dereference）和域访问等组合的语法表达式称为相应声明变量或动态对象域的访问路径，它是一个语法概念，是变量的名字。注意，若s是NULL指针或悬空指针时，s-next，s-data等在本文中都不看成访问路径。下面用p，q和r作为代表一般访问路径的元变量，它们最简单的情况就是声明变量的名字。若访问路径p的后面并置一个非空字符串后形成访问路径q，则称p是q的前缀。在用此定义时，需要把*p这种语法形式看成p*的形式。为方便起见，对访问路径中重复出现的部分使用缩写表示，如s(-next)i用来表示s-next-next…-next（其中-next出现i次），若i=0则s(-next)i就表示s。各种类型的指针变量（包括动态对象中的指针类型的域）都简称为指针，NULL指针和悬空指针统称为无效指针，有指向对象的指针称为有效指针（effectivepointer）。区分NULL指针和悬空指针是因为程序通过判断指针是否等于NULL可区别它们。访问路径为p和q的两个有效指针相等时，则访问路径*p和*q（或p-next和q-next等）互为别名（alias）。由于PointerC对指针运算的限制，再加上函数的参数都是传值方式，一个声明变量的名字不会和其它变量的名字互为别名（本文没有讨论数组元素的动态别名问题）；当两个有效指针的值相等，在代表它们的访问路径上添加公共后缀后，所得两条访问路径形成别名。显然，若能掌握有效指针相等与否的信息，就能判断两条访问路径是否互为别名，及帮助选择访问路径的别名。3指针逻辑的设计为证明程序满足基本安全策略，除了要为PointerC设计一个类型系统外，还需要设计一个证明系统。因为该类型系统的某些定型规则中有附加条件，例如，下标表达式不能越界、s-next必须是一条访问路径等，它们不能由通常的类型系统来检查，本文采用一个证明系统来证明这些附加条件。我们通过对Hoare逻辑的扩展来设计这样一个证明系统，因为我们在目标语言级采用CAP方式。CAP证明目标程序的性质所采用的办法是：把Hoare逻辑的方法直接绑定到目标机器的操作语义上[6,7]。我们在源语言级使用Hoare逻辑方式有助于证明的翻译。该逻辑系统也需要类型系统的支持。例如，不同类型的赋值语句需采用不同的推理规则。我们把Hoare逻辑的这个扩展称为指针逻辑，它的设计基于下面的考虑。由于别名问题，Hoare逻辑不能直接用于有指针类型的语言，需要对Hoare逻辑的规则增加一些约束并且需要增加一些规则来解决问题。增加一些基本规则来表达值相等的访问路径或互为别名的访问路径的性质是简单的，下面是这类性质的一些例子：（1）值相等的访问路径中，若其中一个代表有效指针，则其它的也都是；（2）给值相等的访问路径添加同样的后缀，若形成访问路径，则结果互为别名；（3）互为别名的访问路径的值一定相等；（4）访问路径的别名关系满足自反性、传递性和对称性。在Hoare逻辑的公式{P}S{Q}中，S是语法结构，通常是语句，P和Q分别是它的前后条件。下面考虑两种语句，首先是指针类型的赋值语句p=q，Hoare逻辑的正向赋值公理是{Q}p=q{p.(p=q[pp]Q[pp])}3其中p{p}FV(q)FV(Q)，FV得到变元中自由变量的集合。考虑p是有效指针的情况，下面的约束得到满足时才能使用该公理。（1）前条件Q没有p的其它别名（其它别名指不是p本身）。若不满足，可以尝试用上面提到的基本规则把Q变换到满足这个条件。（2）访问路径q也不以p的其它别名为前缀（在此对程序加这点限制是为了简化讨论）。（3）前条件Q中一定有p==r这样的断言（r不是p的别名）。这是为了保证该赋值不会引起内存泄漏。再考虑为free(p)设计推理规则，仅考虑p所指向对象不含有效指针这种比较简单的情况。考虑该规则的前条件和使用该规则的约束：（1）p应该是有效指针。它直接出现在该规则的前条件中。（2）前条件中没有以p（或与p相等的访问路径）为前缀的访问路径，除非出现在p-next==NULL或p-data==e（e是整型表达式）这样的断言中。该规则要能体现：前条件中涉及p（包括和p相等的访问路径）的基本断言，在后条件中都被删除。这样的要求难以仅用语法代换来表达。例如，若当前程序点的断言是p==qeffective(p)p-next==NULLp-data==10，下一个语句是free(p)，则期望该语句后程序点的断言是dangling(p)dangling(q)。要想完成上述两种语句中的约束检查和断言删除等，需要寻找新的方式来表达推理规则。指针逻辑的推理规则设计基于下面的考虑：（1）若在某程序点能区分有效指针、NULL指针和悬空指针，并且知道有效指针之间是否相等，则就能判断有关指针的操作是否安全，还可以得出经过这步操作后指针信息的变化。（2）推理规则的设计要有利于用工具来进行自动推导。（3）把相等的指针表达在一个集合中，便于在推理规则中表示语句执行所引起的指针信息变化。本文主要介绍证明指针性质的推理规则的设计。3.1基本运算的定义在指针逻辑中，程序点的NULL指针集合用表示，悬空指针的集合用表示，有效指针集合用表示。中指针的具体值并不重要，重要的是它们是否相等，因此基于相等与否把它们划分成若干等价集合。例如，若中有等价集合{p,q}，它表示p和q是相等的有效指针，并且它们不等于其它集合中的指针。一个等价集合不能删掉任何元素，也不能分成若干子集，因为这样做都会使指针信息发生变化。因此，在指针逻辑的断言演算中，中的等价集合被看成命题常元；同样，和也都被看成命题常元。这些集合只能用本节为指针赋值等设计的推理规则来改变。在语法结构的前后条件中，中的等价集合、和虽以集合方式出现，但本质上是逻辑表达式，因此用“”连接它们。作为缩写，有时用表示。访问路径是满足一定语法要求的字符串，本文所说的串都是指构成访问路径的串或子串，并用Paths表示访问路径集合。若访问路径p是q的前缀，则谓词prefix(p,q)等于true，否则等于false。符号“·”用于两个串的连接；它也用于串的集合S和串s的连接，使得S中的每个串连接s：S·sSwheres·sSiffsS若s1·s2和s1（s1和s2都不是空串）是值相等的访问路径，则称s2是访问路径s1·s2·s3（s3也不是空串）中的环。符号表示语法上等同，表示语法上等同测试。下面先