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

一种用于指针程序安全性证明的指针逻辑
陈意云 华保健 葛 琳 王志芳
（中国科学技术大学计算机科学与技术系，合肥 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，简称PCC）[3]和FPCC（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）编译器在把源程序翻译成目标代码的同时，将源程序满足规范的证明翻译成目标代码满足等效规范的证明，这样的编译器称为出具证明的编译器（certifying compiler）；
（4）在目标代码一级由证明检验器利用代码所携带的证明自动进行代码满足规范的检验。
该框架的优点是，它向程序设计者提供源级而不是目标级的程序性质证明方法，以提高安全程序的开发效率，同时它将编译器、证明器等排除出受信任的计算基础（Trusted Computing Base，简称TCB），以尽量缩小系统的TCB。
本文介绍我们在这个框架的初步实现中，为类C语言的一个子集PointerC设计的一个指针逻辑系统，它是Hoare逻辑的一种扩展，本质上是一种精确的指针分析（pointer analysis）工具。它可用来从前向后收集各指针是NULL指针、悬空指针（dangling pointer）还是有效指针（有指向对象的指针）的信息，收集各有效指针之间相等与否的信息。所收集信息用来证明指针程序是否满足定型规则（typing rule）的附加条件，以支持对指针程序的安全性验证及其它性质的验证。本文的组织如下：第二节介绍有关指针安全的一些基本概念，第三节是指针逻辑的设计，第四节给出一个证明实例，第五节是相关工作比较，第六节是总结。
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指针和悬空指针统称为无效指针，有指向对象的指针称为有效指针（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变换到满足这个条件。
（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指针集合用N表示，悬空指针的集合用D表示，有效指针集合用P表示。P中指针的具体值并不重要，重要的是它们是否相等，因此基于相等与否把它们划分成若干等价集合。例如，若P中有等价集合{p, q}，它表示p和q是相等的有效指针，并且它们不等于其它集合中的指针。一个等价集合不能删掉任何元素，也不能分成若干子集，因为这样做都会使指针信息发生变化。因此，在指针逻辑的断言演算中，P中的等价集合被看成命题常元；同样，N和D也都被看成命题常元。这些集合只能用本节为指针赋值等设计的推理规则来改变。在语法结构的前后条件中，P中的等价集合、N和D 虽以集合方式出现，但本质上是逻辑表达式，因此用“Ù”连接它们。作为缩写，有时用Y表示P Ù N Ù D。
访问路径是满足一定语法要求的字符串，本文所说的串都是指构成访问路径的串或子串，并用Paths表示访问路径集合。若访问路径p是q的前缀，则谓词prefix(p, q)等于true，否则等于false。符号“·”用于两个串的连接；它也用于串的集合S和串s的连接，使得S中的每个串连接s：
S·sS¢ where s¢·s Î S¢ iff s¢Î S
若s1·s2和s1（s1和s2都不是空串）是值相等的访问路径，则称s2是访问路径s1·s2·s3（s3也不是空串）中的环。符号º表示语法上等同，ºº表示语法上等同测试。
下面先定义访问路径上的一些函数，它们都以程序点的指针信息Y或P为参数，下面统一都将它忽略。这些定义中出现的关键字在一些软件语言中都出现过，在此忽略它们的解释。需要强调一下，访问路径p和q在本文中几乎总是指称指针，因此本文也经常直接称它们为指针；但是，在下面的函数中，使用的是它们的语法表达式（访问路径）。
1）别名集合的计算
closure(p)计算访问路径p的最简别名集合，称为p的闭包，它包含且仅包含p所有的无环别名。
closure(p)
if length(p)==1then {p}
else let s1·…· sn-1· sn º p in compression
(expansion(closure(s1·…· sn-1)) · sn)
其中length(p)计算访问路径p的长度，它是指p由几个有语法意义的部分组成，而不是指p的字符个数，例如t->next->data的长度为3。
expansion(S)用来在别名集合S中加入与其中访问路径相等的访问路径，其定义如下：
expansion(S)
if $S¢: (PÈ{N}È{D}).(S ÇS¢ !=Æ)
then let {p1, …, pn}= S¢- S
where S¢Î (PÈ{N}È{D}) Ù S ÇS¢ !=Æ
in S Èclosure(p1) È…È closure(pn)
else Æ
compression(S)用来删除别名集合S中带环的访问路径，其定义如下：
compression(S)S-S¢
where (S¢ÌS) Ù ( (s1· s2· s3)ÎS¢ iff
(s1!=e) Ù (s2!=e) Ù (s3!=e) Ù
((s1· s3)ÎS) Ù (s1· s2= s1) )
为清晰起见，上面给出的是closure的一个定义，而不是closure的实现算法，例如，该定义没有考虑面临双向循环链表等带环数据结构时，递归计算的终止问题。在closure的实现中是不难把计算的终止等问题考虑进去的。有了closure函数，也很容易删掉访问路径中的环，为方便讨论，我们认为程序中给出的都是最简访问路径。
2）访问路径的单个别名函数alias(p, q)
该函数从访问路径p的别名集合中任取p¢，满足p¢不以访问路径q的别名为前缀。若找不到这样的p¢，则结果仍是p。
alias(p, q)
let S = {p¢ : closure(p) |
"q¢: closure(q). Øprefix(q¢, p¢) }
in if S == Æ then p else p¢ where p¢ÎS
3）访问路径所在等价集合函数equals(p)
若p的别名出现在某个等价集合中，则返回该集合，否则返回空集。
equals(p)
if $S:P.(SÇclosure(p) != Æ) then
S where SÎP Ù SÇclosure(p) != Æ
else Æ
下面介绍在推理规则中直接使用的运算或谓词，这些运算表达语句后条件中的Y是如何从前条件的Y得到的。
4）有效指针的替换和删除运算
若S是P的一个等价集合，p是一个有效指针，则S/p表示对S中以p的别名为前缀的每个指针q，都用alias(q, p)寻找一个别名来代替它，然后将S中出现的p的别名和以它们为前缀的访问路径都删除。
S/p
let S¢={q : S | "p¢:closure(p). Øprefix(p¢, q)} È {q¢:Paths | $q:S.$p¢:closure(p).(prefix(p¢,q) Ù
q¢ ºº alias(q, p))}
in {q: S¢| Ø(qÎclosure(p)) Ù
"p¢:closure(p).Øprefix(p¢, q)}
若需要对P中每个S进行替换和删除p的运算，则用P/p表示。
当有效指针q被赋予一个不等于q的值时，q和以q为前缀的访问路径都需要从原来的等价集合中删除，例如，若P={{s, t->prior}, {t, s->next}}，则P/t={{s, s->next->prior}, {s->next}}。
5）无效指针替换运算
N\p和D\p分别用来表示将N和D中以p的别名为前缀的访问路径用它们的其它别名来代替。
N\p
{q:N | "p¢:closure(p).Øprefix(p¢, q)} È
{q¢:Paths | $q:N.$p¢:closure(p).(prefix(p¢,q)Ù
q¢ ºº alias(q, p))}
D\p的定义类似。
6）无效指针删除运算
N/p和D/p分别用来表示将N和D中出现的p的别名删除。
N/p{q : N | Ø(qÎclosure(p))}
N/{p1, …, pn}((N/p1) … /pn)
D/p的定义类似。
7）指针添加运算
并集算符“È”直接用来表示向指针集合中添加一个指针，例如S È {p}。我们为P中等价集合的增加、删除和替换使用新的记号，它们基于集合运算符号“È”和“-”及它们的组合来定义。
P+pPÈ{{p}}
――把仅由p构成的等价集合加到P中
P-pP-{equals(p)}
――删掉P中p所在的等价集合
P add q to p(P- p) È {equals(p) È{q}}
――把q加到P中p所在的等价集合
8）有效指针删除是否引起内存泄漏的测试leak(p)
对有效指针p所在等价集合S进行S/p计算，结果为空集合时则表示会出现内存泄漏；否则不会。
leak(p)equals(p)/p == Æ
9）一些基本谓词的定义
下面这些谓词用来测试指针p的别名是否在某个集合中。
p <: P$S:P.(SÇclosure(p) != Æ)
p <: SSÇclosure(p) != Æ
（S是P中的一个等价集合）
p <: N(N Ç closure(p)) != Æ
p <: D(D Ç closure(p)) != Æ
p <: Y(p <: P) Ú (p <: N)Ú (p <: D)
3.2 断言演算
把指针集合看成常元，断言上的演算基本上仍遵守经典逻辑的演算，只是对于指针集合，不能使用A Ù B Þ A和A Ù B Þ B，因为这会丢失指针信息。
另外，对指针集合需要引入一些专用的规则，受篇幅限制，在此只列举部分规则。
1）判断Y是否有矛盾
例如，下面的规则表示一个有效指针不能同时出现在两个不同的等价集合中。

2）吸收指针相等关系断言
在PointerC的程序中，条件语句和循环语句的规则会把p==NULL和p==q等形式的断言分别引入两条件分支和循环体前程序点的断言中。需要一些规则来把它们吸收到指针集合中或者推导出矛盾，下面列出其中的一部分。

3）别名替换
有时需要用下面的规则来进行别名替换。

3.3公理和推理规则
下面给出联系到PointerC各种语句的公理和推理规则。这些规则体现了相应语句引起的指针集合的增、减和替换。在下面的所有规则中，其前提中的断言都是基于语句前的那个程序点的Y来计算的。
1）指针之间的赋值语句p=q（包括q是常量NULL的情况，略去了q是悬空指针的规则）
不同情况的指针赋值用不同的规则。
（1）p和q是相等的有效指针，或都等于NULL

（2）p和q是不相等的有效指针

（3）p是NULL指针，q是有效指针

（4）p是悬空指针，q是有效指针

（5）p是有效指针，q等于NULL

（6）p是悬空指针，q等于NULL

2）非指针类型的赋值公理
{YÙ(Q[y1¬x]…[yn¬x][x¬e])} x = e {YÙQ}
（y1, …, yn构成closure(x)的所有成员）
这是考虑了别名情况后的Hoare逻辑赋值公理, 它不改变Y。该公理中的断言Q只含整型数据的子断言。以下使用的Q也都满足这个限制。
3）对于指针类型的赋值，若前条件是YÙQ，并且Q中也有访问路径（包括作为Q中访问路径前缀的情况），则除了用先前指针赋值的规则外，还需要用下面的赋值公理。
{YÙQ} p=q {Y¢ÙQ[r¬p]}
（r是closure(p)中的一个其它成员，
Y¢由1)的规则从Y得到）
换一种说法是，对指针p赋值时，对p的别名替换还需要出现在Y以外的断言中。该规则也用在malloc和free语句场合。
4）复合、条件和循环语句的规则以及推论规则等仍然使用Hoare逻辑的规则。
5）分配空间语句p = malloc(T)，其中T是类型。若T是结构类型，r1, …, rn是其中的指针域在该类型中的访问路径。
（1）p是NULL指针

（2）p是悬空指针的规则和（1）类似。
（3）p是有效指针。把该语句看成语句序列p = NULL; p = malloc(T)，并将相应的规则用于证明。
6）释放空间语句free(p)
下面的规则用于p所指向对象不含有效指针的场合。若从P知道p所指向对象中含有有效指针p->r1,…,p->rn的话，则可把该语句看成语句序列p->r1=NULL; …;p->rn=NULL; free(p)来进行证明。这样做的目的是简化free(p)的规则。

4 证明实例
我们已经用指针逻辑系统证明了单链表、双向链表和二叉树等数据结构的一些函数。本节以删除二叉排序树一个结点并重接它的左或右子树的函数struct node * DeleteNode(struct node *p)为例。
在证明该函数时，参数所指向的树上，有效指针和NULL指针的布局是不清楚的，但它必须满足树的定义。若树结点定义是struct node {int data; struct node *l，*r; }，那么以p为根结点指针的树的定义如下：
tree(p){p}N Ú ({p} Ù tree(p->l) Ù tree(p->r) )
如果p不是空指针，通过下面的演算可以知道p是有效指针并且tree(p->l) Ù tree(p->r)为真。
tree(p) Ù (p!=NULL)
º ({p}N Ú ({p} Ù tree(p->l) Ù tree(p->r) ) )
Ù (p!=NULL)
Û ({p}N Ù (p!=NULL)) Ú
({p}Ù tree(p->l)Ù tree(p->r)Ù (p!=NULL))
Û false Ú ({p} Ù tree(p->l) Ù tree(p->r))
Û {p} Ù tree(p->l) Ù tree(p->r)
程序设计者只要给出函数前后条件和循环不变式，其它程序点的断言可以通过指针逻辑得到。图1仅对形参p的左右子树都非空的大部分程序点插入了断言（该函数要求参数是非空树），其它部分在关键点插入了断言。在断言中，直接列出各等价集合来表示P，N和D用下标{…}N和{…}D来区分，它们为空时则不出现在断言中。我们没有给出return语句后的断言，因为本文没有提供return语句的推理规则。
5 相关工作
Hoare逻辑的一个重要特征是用变量代换来抓住赋值的语义，本文的指针逻辑系统本质上是一种指针分析工具，它用访问路径的增加、删除和替换来抓住指针操作带来的影响。指针分析已经研究了20多年，历史上的指针分析主要回答：对指针类型的变量，它们运行时可能指向的对象集合是什么。这样的指针分析可用在程序的静态分析和优化的很多方面：寄存器分配和常量传播所需的活跃变量分析，还有像NULL指针脱引用这样的潜在运行错误的静态检查等。近年来它还用在发现危及安全的缓冲区溢出和打印格式串错误等。和其它静态技术类似，指针分析受到可判定性问题的困扰，对大多数语言来说，所得到的解总是一个近似。
在指向对象集合的精度上，不同的应用要求不同的粒度。不同的精度要求采用不同的分析方法，有流敏感和流不敏感的区分，路径敏感和路径不敏感的区分以及过程内和过程间的区分。例如，Bjame Steensgaard对C语言的一个禁止指针强制和指针算术等的子集，描述了一种基于类型推导的过程间的、流不敏感的和路径不敏感的指针分析[8]。该方法基于变量的存储模型，定义了类型系统及推导指针指向的规则集合，用以分析运行时指针变量可能指向的对象集合。Marc Berndl等首先把二叉决策图用于流不敏感和路径不敏感的指针分析[9]，比较成功地解决了这类分析的效率问题。Michael Hind对这方面的研究做了一个总结[10]，列出了一些待解决的问题。
出于软件安全方面的要求，本文实现的是精确而不是近似的指针分析，因此在不影响语言功能的情况下，对C语言中难以判定的指针使用方式进行了限制，正是这种限制使得本文可以采用与通常的C语言指针分析完全不同的方法。

{ p!=NULL Ù tree(p) }
struct node * DeleteNode(struct node *p)
{ struct node *q, *s;
{ {p} Ù tree(p->l) Ù tree(p->r) Ù {q, s}D }
if(p->r==NULL) /* 右子树为空，只需重接它的左子树 */
{ q = p; s = p->l; free(q); { {p, q}D Ù tree(s) } return s; }
else if(p->l==NULL) /* 左子树为空，只需重接它的右子树 */
{ q = p; s = p->r; free(q); { {s} Ù {p, q}D Ù tree(s) } return s; }
else /* 左右子树均不空 */
{ { {p} Ù {p->l} Ù {p->r} Ù {q, s}D Ù tree(p->l) Ù tree(p->r) }
q = p; s = p->l;
if(s->r == NULL) /* 重接*q的左子树 */
{ q->l = s->l; p->data = s->data; free(s); { {p, q} Ù tree(p) } return p; }
else
{ { {p, q} Ù {p->r} Ù {p->l, s} Ù {s->r} Ù tree(p->l->l) Ù tree(p->l->r) Ù tree(p->r) }
q = s; s = s->r;
{ $n:N.( {p} Ù {p->r} Ù "i:0..n-1.{p->l(->r)i} Ù {p->l(->r)n, q} Ù {p->l(->r)n+1, s} Ù
"i:0..n.tree(p->l(->r)i->l) Ù tree(p->l(->r)n+1) Ù tree(p->r) ) } ――循环不变式
while(s->r != NULL) /* 转左，然后向右前进到尽头 */
{ q = s; s = s->r; }
{ $n:N.( {p} Ù {p->r} Ù "i:0..n-1.{p->l(->r)i} Ù {p->l(->r)n, q} Ù {p->l(->r)n+1, s} Ù {s->r}N Ù
"i:0..n.tree(p->l(->r)i->l) Ù tree(p->l(->r)n+1) Ù tree(p->r) ) }
p->data = s->data;
q->r = s->l; /* 重接*q的右子树 */
{ $n:N.( {p} Ù {p->r} Ù "i:0..n-1.{p->l(->r)i} Ù {p->l(->r)n, q} Ù {s} Ù ( ({s->l, q->r} Ù{s->r}N)
Ú {s->r, s->l, q->r}N ) Ù "i:0..n.tree(p->l(->r)i->l) Ù tree(p->l(->r)n+1) Ù tree(p->r) ) }
free(s);
{ $n:N.( {p} Ù {p->r} Ù "i:0..n-1.{p->l(->r)i} Ù {p->l(->r)n, q} Ù ({q->r}Ú{q->r}N)Ù {s}D Ù
"i:0..n.tree(p->l(->r)i->l) Ù tree(p->l(->r)n+1) Ù tree(p->r) ) }
/* 如果在返回调用者前，忽略q和s的信息，可以得到{ {p} Ù tree(p) } */
return p;
}
}
}
图1 删除二叉树结点的程序和断言
本文的指针逻辑和分离逻辑（separation logic）[11, 12]都是通过对Hoare逻辑的拓展，来证明在共享易变数据结构（shared mutable data structure）上带指针操作的程序的性质。分离逻辑适合于对使用这些数据结构的低级命令式语言的程序进行推理。这样的简单语言包括了访问和修改共享结构的命令，包括了显式分配存储和释放存储的命令。分离逻辑在断言语言中引入了“分离合取”等空间连接词，它们可用来断言存储空间分离部分的性质，例如P*Q表示P和Q在两部分不相交的存储空间上分别成立。分离提供了分离逻辑最关键的特征——局部推理。分离逻辑还使用在抽象数据结构上递归定义的谓词，这些谓词允许简洁和灵活地描述有控制地共享的结构。分离逻辑在证明单链表、双向链表和二叉树等易变数据结构的程序上的成功已经展示出它的优点。近来分离逻辑已经出现在用低级语言写的操作系统一些核心程序的正确性证明上[13]。
本文的指针逻辑和分离逻辑的主要区别有两点。分离逻辑面向低级编程语言，指针逻辑面向高级编程语言。另外，由于PointerC不允许指针指向动态申请存储块的中间，那么从指针是否相等就可以判断它们指向的空间是否分离，因此指针逻辑不必引入分离合取这样的空间连接词。
Bornat也采用Hoare逻辑来证明指针程序的性质[14]，采用类似方法的还有Mehta和Nipkow [15]。Bornat把堆看成由指针索引的一群对象，把对象看成由名字索引的一组成员，然后把Hoare逻辑赋值公理拓展成能用于对象成员赋值的场合，用它来证明一些指针程序的性质。由指针索引相等与否来判断别名，基于此来拓展赋值公理是他和我们方法的共同特征，但是他的方法只能用于不提供free操作并且有无用单元收集（garbage collection）的语言。我们的方法虽然适用于提供free操作的场合，但是却导致了指针逻辑的复杂。例如，在free(p)时，为防止悬空指针引用，需要保证以后不会用p或与p相等的指针去访问；再例如，在对有效指针p赋值时，为防止出现内存泄漏，需要知道有和p相等的指针存在。这就导致指针逻辑像是从前向后计算最强后条件，而不是从后向前计算最弱前条件。
6 结束语
本文提出了一种可对指针程序进行精确分析的逻辑系统，它可用来证明指针程序是否满足定型规则的附加条件，以支持指针程序的安全性证明及其它性质证明。我们已经利用证明辅助工具Coq[16]完成了指针逻辑对PointerC操作语义可靠的证明。PointerC及其类型系统、指针逻辑的断言语言、指针逻辑可靠性证明、一些应用程序的证明实例以及基于第1节所提框架的出具证明编译器的一些实现工作，可在我们项目网页
下一步我们将考虑放宽对指针运算的限制，有限制地允许指针算术，以适应编程中经常使用的calloc存储分配。加上面向对象的语言构造，使程序性质证明具有更好的模块性也是下一步需要考虑的内容。

参 考 文 献
[1] Morrisett G, Walker D, Crary K, Glew N. From system F to typed assembly language. Proceedings of 25th ACM Symposium on Principles of Programming Languages, San Diego, 1998: 85-97.
[2] Mandelbaum Y, Walker D, Harper R. An effective theory of type refinements. Proceedings of the 8th International Conference on Functional Programming, Uppsala, Sweden, 2003: 213-225.
[3] Necula G. Proof-carrying code, Proc.24th ACM Symposium On Principles of Programming Languages. New York, 1997: 106-119.
[4] Appel A. W. Foundational proof-carrying code. Proc. 16th Annual IEEE Symposium on Logic in Computer Science, 2001: 247-258.
[5] Yu D, Hamid N. A., Shao Z. Building certified libraries for PCC: dynamic storage allocation. Science of Computer Programming, 2004, 50(1-3):101-127.
[6] Feng X, Shao Z, Vaynberg A, Xiang S, Ni Z. Modular Verification of Assembly Code with Stack-Based Control Abstractions. Proceedings of the 2006 ACM SIGPLAN Conference on Programming Language Design and Implementation, Ottawa, Canada, 2006: 401-414.
[7] Xi H. Applied type system: extended abstract. In the post-workshop proceedings of TYPES 2003, volume 3085 of LNCS, Springer-Verlag, 2004: 394-408.
[8] Steensgaard B. Point