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

一种用于指针程序安全性证明的指针逻辑
陈意云 华保健 葛 琳 王志芳
（中国科学技术大学计算机科学与技术系，合肥 230026）
（中国科学技术大学苏州研究院软件安全实验室，苏州 215123）
摘 要：在高可信软件的多种interC预定义的函数，并且满足安全程序的最基本规定。例如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指针和悬空指针统称为无效指针，有指向对象的指针称为有效指针（effective pointer）。辨别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¢])}
其中p¢Ï{p}ÈFV(q)ÈFV(Q)，FV得到变元中自由变量的集合。考虑p是有效指针的状况，下面的约束得到满足时才干使用该公理。
（1）前条件Q没有p的其他别名（其他别名指不是p自身）。若不满足，可以尝试用上面提到的基本规则把Q变换