第31卷第3期 计 算机学报 Vol.31 No.3 2008年3月 CHINESE JOURNAL OF COMPUTERS Mar.2008 一种用于指针程序安全性证明的指针逻辑 陈意云华保健葛 琳王志芳 (中国科学技术大学计算机科学与技术系合肥230026) (中国科学技术大学苏州研究院软件安全实验室江苏苏州215123) 摘要在高可信软件的各种性质中，安全性是被关注的重点，其中软件满足安全策略的证明方法是研究的热点 之一，文中根据作者所设想的安全程序的设计和证明框架，为类C语言的一个子集设计了一个指针逻辑系统.该逻 辑系统是Hoae逻辑系统的一种扩展，它用推理规则来表达每一种语句引起指针信息的变化情况.它可用来对指 针程序进行精确的指针分析，所获得的信息用来证明指针程序是否满足定型规则的附加条件，以支持程序的安全 性验证.该逻辑系统也可用来证明指针程序的其它性质. 关键词软件安全；指针逻辑；Hoare逻辑；指针分析：类型系统 中图法分类号TP301 A Pointer Logic for Safety Verification of Pointer Programs CHEN Yi-Yun HUA Bao-Jian GE Lin WANG Zhi-Fang (Department of Computer Science.University of Science and Technology of China.Hefei 230026) (So ftware Security Laboratory.Suzhou Institute for Advanced Study. University of Science and Technology of China.Suzhou.Jiangsu 215123) Abstract Safety is an important issue among the properties of high-assurance software and de- veloping 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 sys- tem 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 informa- tion from the analysis can be used to verify if pointer programs satisfy the side conditions of typ- ing rules and then support safety verification for programs.The logic system can also be used to verify other properties of pointer programs. Keywords software safety;pointer logic;Hoare logic;pointer analysis;type system 引起危险、灾难的能力，而security是指软件系统对 引 数据和信息提供保密性、完整性、可用性、真实性保 障的能力.本文所讲的安全性主要是指safety,但是 在高可信的各种要求中，安全性（包括safety和 软件的safety和security是有联系的，黑客通常就 security)是关注的重点.Safety是指软件运行时不 是利用缓冲区溢出、数组访问越界、悬空指针访问等 收稿日期：2006-06-13：最终修改稿收到日期：2007-12-03.本课题得到国家自然科学基金(60673126)资助.陈意云，男，1946年生，教授， 博士生导师，主要研究领域为程序设计语言的理论和实现技术，形式描述技术、软件安全.E-mail:yiyun(@ustc.edu.cm.华保健，男，l979 年生，博士研究生，主要研究方向为程序验证、程序逻辑和软件安全.葛琳，女，19？9年生，博士研究生，主要研究方向为程序验证，软件 安全，类型理论和系统.王志芳，男，1982年生，博士研究生，主要研究方向为软件安全、程序逻辑和程序验证
书 第３１卷 第３期 ２００８年３月 计 算 机 学 报 ＣＨＩＮＥＳＥＪＯＵＲＮＡＬＯＦＣＯＭＰＵＴＥＲＳ Ｖｏｌ．３１ Ｎｏ．３ Ｍａｒ．２００８ 收稿日期：２００６０６１３；最终修改稿收到日期：２００７１２０３．本课题得到国家自然科学基金（６０６７３１２６）资助．陈意云，男，１９４６年生，教授， 博士生导师，主要研究领域为程序设计语言的理论和实现技术、形式描述技术、软件安全．Ｅｍａｉｌ：ｙｉｙｕｎ＠ｕｓｔｃ．ｅｄｕ．ｃｎ．华保健，男，１９７９ 年生，博士研究生，主要研究方向为程序验证、程序逻辑和软件安全．葛 琳，女，１９７９年生，博士研究生，主要研究方向为程序验证、软件 安全、类型理论和系统．王志芳，男，１９８２年生，博士研究生，主要研究方向为软件安全、程序逻辑和程序验证． 一种用于指针程序安全性证明的指针逻辑 陈意云 华保健 葛 琳 王志芳 （中国科学技术大学计算机科学与技术系 合肥 ２３００２６） （中国科学技术大学苏州研究院软件安全实验室 江苏 苏州 ２１５１２３） 摘 要 在高可信软件的各种性质中，安全性是被关注的重点，其中软件满足安全策略的证明方法是研究的热点 之一．文中根据作者所设想的安全程序的设计和证明框架，为类 Ｃ语言的一个子集设计了一个指针逻辑系统．该逻 辑系统是 Ｈｏａｒｅ逻辑系统的一种扩展，它用推理规则来表达每一种语句引起指针信息的变化情况．它可用来对指 针程序进行精确的指针分析，所获得的信息用来证明指针程序是否满足定型规则的附加条件，以支持程序的安全 性验证．该逻辑系统也可用来证明指针程序的其它性质． 关键词 软件安全；指针逻辑；Ｈｏａｒｅ逻辑；指针分析；类型系统 中图法分类号 ＴＰ３０１ 犃犘狅犻狀狋犲狉犔狅犵犻犮犳狅狉犛犪犳犲狋狔犞犲狉犻犳犻犮犪狋犻狅狀狅犳犘狅犻狀狋犲狉犘狉狅犵狉犪犿狊 ＣＨＥＮ ＹｉＹｕｎ ＨＵＡＢａｏＪｉａｎ ＧＥＬｉｎ ＷＡＮＧＺｈｉＦａｎｇ （犇犲狆犪狉狋犿犲狀狋狅犳犆狅犿狆狌狋犲狉犛犮犻犲狀犮犲，犝狀犻狏犲狉狊犻狋狔狅犳犛犮犻犲狀犮犲犪狀犱犜犲犮犺狀狅犾狅犵狔狅犳犆犺犻狀犪，犎犲犳犲犻 ２３００２６） （犛狅犳狋狑犪狉犲犛犲犮狌狉犻狋狔犔犪犫狅狉犪狋狅狉狔，犛狌狕犺狅狌犐狀狊狋犻狋狌狋犲犳狅狉犃犱狏犪狀犮犲犱犛狋狌犱狔， 犝狀犻狏犲狉狊犻狋狔狅犳犛犮犻犲狀犮犲犪狀犱犜犲犮犺狀狅犾狅犵狔狅犳犆犺犻狀犪，犛狌狕犺狅狌，犑犻犪狀犵狊狌 ２１５１２３） 犃犫狊狋狉犪犮狋 Ｓａｆｅｔｙｉｓａｎｉｍｐｏｒｔａｎｔｉｓｓｕｅａｍｏｎｇｔｈｅｐｒｏｐｅｒｔｉｅｓｏｆｈｉｇｈａｓｓｕｒａｎｃｅｓｏｆｔｗａｒｅａｎｄｄｅ ｖｅｌｏｐｉｎｇｔｈｅｖｅｒｉｆｉｃａｔｉｏｎｍｅｔｈｏｄｓｆｏｒｓｏｆｔｗａｒｅｔｏｍｅｅｔｓａｆｅｔｙｐｏｌｉｃｉｅｓｉｓｏｎｅｏｆｔｈｅｈｏｔｒｅｓｅａｒｃｈ．Ｉｎ ｔｅｒｍｓｏｆｔｈｅａｕｔｈｏｒｓ′ｓｋｅｔｃｈｏｆｄｅｓｉｇｎａｎｄｖｅｒｉｆｉｃａｔｉｏｎｏｆｓａｆｅｔｙｐｒｏｇｒａｍｓ，ａｐｏｉｎｔｅｒｌｏｇｉｃｓｙｓｔｅｍ ｉｓｄｅｓｉｇｎｅｄｆｏｒａｓｕｂｓｅｔｏｆＣｌｉｋｅｌａｎｇｕａｇｅ．ＴｈｉｓｌｏｇｉｃｓｙｓｔｅｍｉｓａｎｅｘｔｅｎｓｉｏｎｏｆＨｏａｒｅｌｏｇｉｃｓｙｓ ｔｅｍａｎｄｉｎｆｅｒｅｎｃｅｒｕｌｅｓａｒｅｄｅｓｉｇｎｅｄｔｏｅｘｐｒｅｓｓｔｈｅｍｏｄｉｆｉｃａｔｉｏｎｏｆｐｏｉｎｔｅｒｉｎｆｏｒｍａｔｉｏｎｆｏｒｅｖｅｒｙ ｋｉｎｄｏｆｓｔａｔｅｍｅｎｔｓ．Ｉｔｃａｎｂｅｕｓｅｄｆｏｒａｃｃｕｒａｔｅｐｏｉｎｔｅｒａｎａｌｙｓｉｓｏｆｐｏｉｎｔｅｒｐｒｏｇｒａｍｓ．Ｔｈｅｉｎｆｏｒｍａ ｔｉｏｎｆｒｏｍｔｈｅａｎａｌｙｓｉｓｃａｎｂｅｕｓｅｄｔｏｖｅｒｉｆｙｉｆｐｏｉｎｔｅｒｐｒｏｇｒａｍｓｓａｔｉｓｆｙｔｈｅｓｉｄｅｃｏｎｄｉｔｉｏｎｓｏｆｔｙｐ ｉｎｇｒｕｌｅｓａｎｄｔｈｅｎｓｕｐｐｏｒｔｓａｆｅｔｙｖｅｒｉｆｉｃａｔｉｏｎｆｏｒｐｒｏｇｒａｍｓ．Ｔｈｅｌｏｇｉｃｓｙｓｔｅｍｃａｎａｌｓｏｂｅｕｓｅｄｔｏ ｖｅｒｉｆｙｏｔｈｅｒｐｒｏｐｅｒｔｉｅｓｏｆｐｏｉｎｔｅｒｐｒｏｇｒａｍｓ． 犓犲狔狑狅狉犱狊 ｓｏｆｔｗａｒｅｓａｆｅｔｙ；ｐｏｉｎｔｅｒｌｏｇｉｃ；Ｈｏａｒｅｌｏｇｉｃ；ｐｏｉｎｔｅｒａｎａｌｙｓｉｓ；ｔｙｐｅｓｙｓｔｅｍ １ 引 言 在高可信的各种要求中，安全性（包括ｓａｆｅｔｙ和 ｓｅｃｕｒｉｔｙ）是关注的重点．Ｓａｆｅｔｙ是指软件运行时不 引起危险、灾难的能力，而ｓｅｃｕｒｉｔｙ是指软件系统对 数据和信息提供保密性、完整性、可用性、真实性保 障的能力．本文所讲的安全性主要是指ｓａｆｅｔｙ，但是 软件的ｓａｆｅｔｙ和ｓｅｃｕｒｉｔｙ是有联系的，黑客通常就 是利用缓冲区溢出、数组访问越界、悬空指针访问等
3期 陈意云等：一种用于指针程序安全性证明的指针逻辑 373 低级的safety错误，来破坏系统和获取未经授权的 从前向后收集各指针是NULL指针、悬空指针 控制等.因此提高safety有助于保证security. (dangling pointer)还是有效指针（有指向对象的指 程序性质证明（而不是传统的程序正确性证明） 针)的信息，收集各有效指针之间相等与否的信息， 领域近十年来有了很大的发展，许多学者提出了不 所收集信息用来证明指针程序是否满足定型规则 同的思路，这些思路主要采取基于类型的或基于 (typing rule)的附加条件，以支持对指针程序的安 逻辑的方法，用于高级语言程序或低级语言程序 全性验证及其它性质的验证. 的性质证明.基于类型方法的典型研究有类型化 本文第2节介绍有关指针安全的一些基本概 汇编语言(Typed Assembly Language))和类型细 念；第3节是指针逻辑的设计：第4节给出一个证明 化(type refinement)理论[)的研究.基于逻辑方法 实例：第5节是相关工作比较；第6节是总结. 的典型研究有携带证明的代码(Proof-Carrying Code,PCC)t3]FPCC(Foundational Proof-Carrying 2 基本知识 Code)框架[).Shao的携带证明汇编编程项目CAP (Certified Assembly Programming)[)和基于栈的 首先介绍PointerC在指针运算方面的限制.在 CAP(SCAP)[6是典型的基于逻辑的研究项目.基 PointerC中，指针类型的变量只能用于赋值、相等和 于逻辑的方法和基于类型论的方法有很大的互补 不相等比较、存取指向对象等运算以及作为函数（包 性，近年来出现了一些结合这两种方法的研究.一种 括free)的参数，指针算术和取地址运算(&.)被禁 结合两者的研究是Xi等进行的ATS(Applied Type 止，malloc和free被看成是PointerC预定义的函 System)项目的研究[)，他们扩展类型系统，将程序 数，并且满足安全程序的最基本要求.例如malloc 状态引入类型系统，依靠ATS与Hoare逻辑的相 任何一次调用都能成功并且所分配空间与尚未释放 似性，以ATS来编码Hoare逻辑，从而可以在他们 空间无任何重叠. 的类型系统上模拟Hoare逻辑的推理， 上述限制的目的是为了便于静态检查程序的安 基于国际上这些研究，我们认为，对于那些有高 全性.程序运行时出现对NULL指针或悬空指针进 安全性要求的软件，程序设计和证明的一种新方式 行存取指向对象的操作、把NULL指针或悬空指针 将是： 作为free函数调用的实在参数、发生内存泄漏等都 (1)程序设计者将软件的安全策略等描述成程 被认为不满足基本安全策略（类型安全和内存安全 序应满足的规范，连同程序一起提交给编译器； 等).该语言定型规则中的附加条件就是用来禁止这 (2)编译器生成为证明程序满足规范所需的验 些情况的出现，本文指针逻辑的用途之一就是用来 证条件，并且利用内嵌的定理证明器自动地或交互 完成对这些附加条件的静态检查， 地证明这些验证条件； 下面明确本文有关指针类型的一些术语和约 (3)编译器在把源程序翻译成目标代码的同 定，程序中显式声明的变量称为声明变量，由malloc 时，将源程序满足规范的证明翻译成目标代码满足 函数显式和动态分配的空间称为动态对象.在程序 等效规范的证明，这样的编译器称为出具证明的编 中，动态对象的域只能通过指针类型的声明变量来访 译器(certifying compiler); 问，如s>data和s>next->prior等，这种把 (4)在目标代码一级由证明检验器利用代码所 脱引用(dereference)和域访问等组合的语法表达式 携带的证明自动进行代码满足规范的检验： 称为相应声明变量或动态对象域的访问路径，它是一 该框架的优点是，它向程序设计者提供源级而 个语法概念，是变量的名字.注意，若s是NULL指 不是目标级的程序性质证明方法，以提高安全程序 针或悬空指针时，s->next,s->data等在本文中 的开发效率，同时它将编译器、证明器等排除出受信 都不看成访问路径.下面用p,9和r作为代表一般访 任的计算基础(Trusted Computing Base,TCB),以 问路径的元变量，它们最简单的情况就是声明变量的 尽量缩小系统的TCB. 名字.若访问路径p的后面并置一个非空字符串后 本文介绍我们在这个框架的初步实现中，为类 形成访问路径q,则称p是q的前缀.在用此定义 C语言的一个子集PointerC设计的一个指针逻辑 时，需要把p这种语法形式看成p￥的形式.为方便 系统，它是Hoare逻辑的一种扩展，本质上是一种 起见，对访问路径中重复出现的部分使用缩写表示， 精确的指针分析(pointer analysis)工具.它可用来 如s(->next)用来表示s>next一>next…->
低级的ｓａｆｅｔｙ错误，来破坏系统和获取未经授权的 控制等．因此提高ｓａｆｅｔｙ有助于保证ｓｅｃｕｒｉｔｙ． 程序性质证明（而不是传统的程序正确性证明） 领域近十年来有了很大的发展，许多学者提出了不 同的思路，这 些 思 路 主 要 采 取 基 于 类 型 的 或 基 于 逻辑的方法，用 于 高 级 语 言 程 序 或 低 级 语 言 程 序 的性质证明．基 于 类 型 方 法 的 典 型 研 究 有 类 型 化 汇编语言（ＴｙｐｅｄＡｓｓｅｍｂｌｙＬａｎｇｕａｇｅ）［１］和类型细 化（ｔｙｐｅｒｅｆｉｎｅｍｅｎｔ）理论［２］的研究．基于逻辑方法 的典 型 研 究 有 携 带 证 明 的 代 码 （ＰｒｏｏｆＣａｒｒｙｉｎｇ Ｃｏｄｅ，ＰＣＣ）［３］和ＦＰＣＣ（ＦｏｕｎｄａｔｉｏｎａｌＰｒｏｏｆＣａｒｒｙｉｎｇ Ｃｏｄｅ）框架［４］ ．Ｓｈａｏ的携带证明汇编编程项目 ＣＡＰ （ＣｅｒｔｉｆｉｅｄＡｓｓｅｍｂｌｙＰｒｏｇｒａｍｍｉｎｇ）［５］和基于栈的 ＣＡＰ（ＳＣＡＰ）［６］是典型的基于逻辑的研究项目．基 于逻辑的方法和基于类型论的方法有很大的互补 性，近年来出现了一些结合这两种方法的研究．一种 结合两者的研究是Ｘｉ等进行的 ＡＴＳ（ＡｐｐｌｉｅｄＴｙｐｅ Ｓｙｓｔｅｍ）项目的研究［７］，他们扩展类型系统，将程序 状态引入类型系统，依靠 ＡＴＳ与 Ｈｏａｒｅ逻辑的相 似性，以 ＡＴＳ来编码 Ｈｏａｒｅ逻辑，从而可以在他们 的类型系统上模拟 Ｈｏａｒｅ逻辑的推理． 基于国际上这些研究，我们认为，对于那些有高 安全性要求的软件，程序设计和证明的一种新方式 将是： （１）程序设计者将软件的安全策略等描述成程 序应满足的规范，连同程序一起提交给编译器； （２）编译器生成为证明程序满足规范所需的验 证条件，并且利用内嵌的定理证明器自动地或交互 地证明这些验证条件； （３）编译 器 在 把 源 程 序 翻 译 成 目 标 代 码 的 同 时，将源程序满足规范的证明翻译成目标代码满足 等效规范的证明，这样的编译器称为出具证明的编 译器（ｃｅｒｔｉｆｙｉｎｇｃｏｍｐｉｌｅｒ）； （４）在目标代码一级由证明检验器利用代码所 携带的证明自动进行代码满足规范的检验． 该框架的优点是，它向程序设计者提供源级而 不是目标级的程序性质证明方法，以提高安全程序 的开发效率，同时它将编译器、证明器等排除出受信 任的计算基础（ＴｒｕｓｔｅｄＣｏｍｐｕｔｉｎｇＢａｓｅ，ＴＣＢ），以 尽量缩小系统的 ＴＣＢ． 本文介绍我们在这个框架的初步实现中，为类 Ｃ语言的一个子集 ＰｏｉｎｔｅｒＣ 设计的一个指针逻辑 系统，它是 Ｈｏａｒｅ逻辑的一种扩展，本质上是一种 精确的指针分析（ｐｏｉｎｔｅｒａｎａｌｙｓｉｓ）工具．它可用来 从前 向 后 收 集 各 指 针 是 ＮＵＬＬ 指 针、悬 空 指 针 （ｄａｎｇｌｉｎｇｐｏｉｎｔｅｒ）还是有效指针（有指向对象的指 针）的信息，收集各有效指针之间相等与否的信息． 所收集信息用来证明指针程序是否满足定型规则 （ｔｙｐｉｎｇｒｕｌｅ）的附加条件，以支持对指针程序的安 全性验证及其它性质的验证． 本文第２节介绍有关指针安全的一些基本概 念；第３节是指针逻辑的设计；第４节给出一个证明 实例；第５节是相关工作比较；第６节是总结． ２ 基本知识 首先介绍 ＰｏｉｎｔｅｒＣ在指针运算方面的限制．在 ＰｏｉｎｔｅｒＣ中，指针类型的变量只能用于赋值、相等和 不相等比较、存取指向对象等运算以及作为函数（包 括ｆｒｅｅ）的参数，指针算术和取地址运算（＆）被禁 止．ｍａｌｌｏｃ和ｆｒｅｅ被看成是 ＰｏｉｎｔｅｒＣ 预定义的函 数，并且满足安全程序的最基本要求．例如 ｍａｌｌｏｃ 任何一次调用都能成功并且所分配空间与尚未释放 空间无任何重叠． 上述限制的目的是为了便于静态检查程序的安 全性．程序运行时出现对 ＮＵＬＬ指针或悬空指针进 行存取指向对象的操作、把 ＮＵＬＬ指针或悬空指针 作为ｆｒｅｅ函数调用的实在参数、发生内存泄漏等都 被认为不满足基本安全策略（类型安全和内存安全 等）．该语言定型规则中的附加条件就是用来禁止这 些情况的出现，本文指针逻辑的用途之一就是用来 完成对这些附加条件的静态检查． 下面明确本文有关指针类型的一些术语和约 定．程序中显式声明的变量称为声明变量，由 ｍａｌｌｏｃ 函数显式和动态分配的空间称为动态对象．在程序 中，动态对象的域只能通过指针类型的声明变量来访 问，如狊－＞犱犪狋犪 和狊 －＞狀犲狓狋－＞狆狉犻狅狉等，这种把 脱引用（ｄｅｒｅｆｅｒｅｎｃｅ）和域访问等组合的语法表达式 称为相应声明变量或动态对象域的访问路径，它是一 个语法概念，是变量的名字．注意，若狊是 ＮＵＬＬ 指 针或悬空指针时，狊－＞狀犲狓狋，狊－＞犱犪狋犪等在本文中 都不看成访问路径．下面用狆，狇和狉作为代表一般访 问路径的元变量，它们最简单的情况就是声明变量的 名字．若访问路径狆的后面并置一个非空字符串后 形成访问路径狇，则称 狆 是狇 的前缀．在用此定义 时，需要把狆这种语法形式看成狆的形式．为方便 起见，对访问路径中重复出现的部分使用缩写表示， 如狊（－＞狀犲狓狋）犻 用来表示狊 －＞狀犲狓狋－＞狀犲狓狋…－＞ ３ 期 陈意云等：一种用于指针程序安全性证明的指针逻辑 ３７３
374 计算 机学 报 2008年 next(其中>next出现i次)，若i=0,则s(->next)i 形成访问路径，则结果互为别名； 就表示s (3)互为别名的访问路径的值一定相等； 各种类型的指针变量（包括动态对象中的指针 (4)访问路径的别名关系满足自反性、传递性 类型的域)都简称为指针，NULL指针和悬空指针 和对称性 统称为无效指针，有指向对象的指针称为有效指针 在Hoare逻辑的公式{P}S{Q}中，S是语法结 (effective pointer).区分NULL指针和悬空指针是 构，通常是语句，P和Q分别是它的前后条件.下面 由程序通过判断指针是否等于NULL来区别的.访 考虑两种语句，首先是指针类型的赋值语句p=q, 问路径为p和q的两个有效指针相等时，访问路径 Hoare逻辑的正向赋值公理是 *p和*g(或p->next和q>next等)互为别名 {Q}p=q{3p.(p=q[p←p]∧Q[pp'])}, (alias).由于PointerC对指针运算的限制，再加上 其中p'任{p}UFV(q)UFV(Q),FV是得到变元中 函数的参数都是传值方式，一个声明变量的名字不 自由变量集合的函数.考虑p是有效指针的情况， 会和其它变量的名字互为别名（本文没有讨论数组 下面的约束得到满足时才能使用该公理， 元素的动态别名问题)：当两个有效指针的值相等 (1)前条件Q没有p的其它别名（其它别名指 时，在代表它们的访问路径上添加公共后缀后，所得 不是p本身).若不满足，可以尝试用上面提到的基 两条访问路径形成别名，显然，若能掌握有效指针相 本规则把Q变换到满足这个条件， 等与否的信息，就能判断两条访问路径是否互为别 (2)访问路径q也不以p的其它别名为前缀 名并且帮助选择访问路径的别名. (在此对程序加这点限制是为了简化讨论). (3)前条件Q中一定有p==r这样的断言(r 3 指针逻辑的设计 不是p的别名).这是为了保证该赋值不会引起内 存泄漏。 为证明程序满足基本安全策略，除了要为Point- 再考虑为free(p)设计推理规则，这里仅考虑p erC设计一个类型系统外，还需要设计一个证明系 所指向对象不含有效指针这种比较简单的情况.考 统.因为该类型系统的某些定型规则中有附加条件， 虑该规则的前条件和使用该规则的约束： 例如，下标表达式不能越界，s>next必须是一条 (1)p应该是有效指针.它直接出现在该规则的 访问路径等，它们不能由通常的类型系统来检查，本 前条件中 文采用一个证明系统来证明这些附加条件， (2)前条件中没有以p(或与p相等的访问路 我们可通过对Hoare逻辑的扩展来设计这样 径)为前缀的访问路径，除非出现在p>ext== 一个证明系统，因为我们在目标语言级采用CAP方 NULL或p->data==e(e是整型表达式)这样 式.CAP证明目标程序的性质所采用的办法是：把 的断言中， Hoare逻辑的方法直接绑定到目标机器的操作语义 该规则要能体现：前条件中涉及p(包括和p相 上[s-刃.我们在源语言级使用Hoare逻辑方式有助 等的访问路径)的基本断言，在后条件中都被删除 于证明的翻译.该逻辑系统也需要类型系统的支持， 这样的要求难以仅用语法代换来表达。 例如，不同类型的赋值语句需采用不同的推理规则. 例如，若当前程序点的断言是p==aN effec- 我们把Hoare逻辑的这个扩展称为指针逻辑， tive(p)Ap->next==NULL Ap->data== 它的设计基于下面的考虑. 10,下一个语句是free(p),则期望该语句后程序点 由于别名问题，Hoare逻辑不能直接用于有指 的断言是dangling(p)∧langling(q). 针类型的语言，需要对Hoare逻辑的规则增加一些 要想完成上述两种语句中的约束检查和断言删 约束并且需要增加一些规则来解决问题.增加一些 除等，需要寻找新的方式来表达推理规则.指针逻辑 基本规则来表达值相等的访问路径或互为别名的访 的推理规则设计基于下面的考虑： 问路径的性质是简单的，下面是这类性质的一些 (1)若在某程序点能区分有效指针、NULL指 例子： 针和悬空指针，并且知道有效指针之间是否相等，则 (1)值相等的访问路径中，若其中一个代表有 就能判断有关指针的操作是否安全，还可以得出经 效指针，则其它的也都是； 过这步操作后指针信息的变化， (2)给值相等的访问路径添加同样的后缀，若 (2)推理规则的设计要有利于用工具来进行自
狀犲狓狋（其中－＞狀犲狓狋出现犻次），若犻＝０，则狊（－＞狀犲狓狋）犻 就表示狊． 各种类型的指针变量（包括动态对象中的指针 类型的域）都简称为指针，ＮＵＬＬ 指针和悬空指针 统称为无效指针，有指向对象的指针称为有效指针 （ｅｆｆｅｃｔｉｖｅｐｏｉｎｔｅｒ）．区分 ＮＵＬＬ指针和悬空指针是 由程序通过判断指针是否等于 ＮＵＬＬ来区别的．访 问路径为狆和狇 的两个有效指针相等时，访问路径 狆 和 狇（或狆 －＞狀犲狓狋和狇 －＞狀犲狓狋等）互为别名 （ａｌｉａｓ）．由于 ＰｏｉｎｔｅｒＣ 对指针运算的限制，再加上 函数的参数都是传值方式，一个声明变量的名字不 会和其它变量的名字互为别名（本文没有讨论数组 元素的动态别名问题）；当两个有效指针的值相等 时，在代表它们的访问路径上添加公共后缀后，所得 两条访问路径形成别名．显然，若能掌握有效指针相 等与否的信息，就能判断两条访问路径是否互为别 名并且帮助选择访问路径的别名． ３ 指针逻辑的设计 为证明程序满足基本安全策略，除了要为Ｐｏｉｎｔ ｅｒＣ设计一个类型系统外，还需要设计一个证明系 统．因为该类型系统的某些定型规则中有附加条件， 例如，下标表达式不能越界，狊－＞狀犲狓狋必须是一条 访问路径等，它们不能由通常的类型系统来检查，本 文采用一个证明系统来证明这些附加条件． 我们可通过对 Ｈｏａｒｅ逻辑的扩展来设计这样 一个证明系统，因为我们在目标语言级采用 ＣＡＰ方 式．ＣＡＰ证明目标程序的性质所采用的办法是：把 Ｈｏａｒｅ逻辑的方法直接绑定到目标机器的操作语义 上［６７］ ．我们在源语言级使用 Ｈｏａｒｅ逻辑方式有助 于证明的翻译．该逻辑系统也需要类型系统的支持． 例如，不同类型的赋值语句需采用不同的推理规则． 我们把 Ｈｏａｒｅ逻辑的这个扩展称为指针逻辑， 它的设计基于下面的考虑． 由于别名问题，Ｈｏａｒｅ逻辑不能直接用于有指 针类型的语言，需要对 Ｈｏａｒｅ逻辑的规则增加一些 约束并且需要增加一些规则来解决问题．增加一些 基本规则来表达值相等的访问路径或互为别名的访 问路径的 性 质 是 简 单 的，下 面 是 这 类 性 质 的 一 些 例子： （１）值相等的访问路径中，若其中一个代表有 效指针，则其它的也都是； （２）给值相等的访问路径添加同样的后缀，若 形成访问路径，则结果互为别名； （３）互为别名的访问路径的值一定相等； （４）访问路径的别名关系满足自反性、传递性 和对称性． 在 Ｈｏａｒｅ逻辑的公式｛犘｝犛｛犙｝中，犛 是语法结 构，通常是语句，犘 和犙 分别是它的前后条件．下面 考虑两种语句，首先是指针类型的赋值语句狆＝狇， Ｈｏａｒｅ逻辑的正向赋值公理是 ｛犙｝狆＝狇｛狆′．（狆＝狇［狆←狆′］∧犙［狆←狆′］）｝， 其中狆′｛狆｝∪犉犞（狇）∪犉犞（犙），犉犞 是得到变元中 自由变量集合的函数．考虑狆 是有效指针的情况， 下面的约束得到满足时才能使用该公理． （１）前条件 犙 没有狆 的其它别名（其它别名指 不是狆本身）．若不满足，可以尝试用上面提到的基 本规则把犙 变换到满足这个条件． （２）访问路径狇 也不以狆 的 其 它 别 名 为 前 缀 （在此对程序加这点限制是为了简化讨论）． （３）前条件犙 中一定有狆＝＝狉这样的断言（狉 不是狆 的别名）．这是为了保证该赋值不会引起内 存泄漏． 再考虑为犳狉犲犲（狆）设计推理规则，这里仅考虑狆 所指向对象不含有效指针这种比较简单的情况．考 虑该规则的前条件和使用该规则的约束： （１）狆应该是有效指针．它直接出现在该规则的 前条件中． （２）前条件中没有以 狆（或与 狆 相等的访问路 径）为前缀的访问路径，除非出现在狆 －＞狀犲狓狋＝＝ ＮＵＬＬ或狆 －＞犱犪狋犪＝＝犲（犲是整型表达式）这样 的断言中． 该规则要能体现：前条件中涉及狆（包括和狆 相 等的访问路径）的基本断言，在后条件中都被删除． 这样的要求难以仅用语法代换来表达． 例如，若当前程序点的断言是狆＝＝狇∧犲犳犳犲犮 狋犻狏犲（狆）∧狆 －＞狀犲狓狋＝ ＝ ＮＵＬＬ∧狆 －＞犱犪狋犪＝ ＝ １０，下一个语句是犳狉犲犲（狆），则期望该语句后程序点 的断言是犱犪狀犵犾犻狀犵（狆）∧犱犪狀犵犾犻狀犵（狇）． 要想完成上述两种语句中的约束检查和断言删 除等，需要寻找新的方式来表达推理规则．指针逻辑 的推理规则设计基于下面的考虑： （１）若在某程序点能区分有效指针、ＮＵＬＬ 指 针和悬空指针，并且知道有效指针之间是否相等，则 就能判断有关指针的操作是否安全，还可以得出经 过这步操作后指针信息的变化． （２）推理规则的设计要有利于用工具来进行自 ３７４ 计 算 机 学 报 ２００８年
3期 陈意云等：一种用于指针程序安全性证明的指针逻辑 375 动推导. else let s1·s2·…sm-l·sn=pin (3)把相等的指针表达在一个集合中，便于在 com pression(e.r pansion(closure(s·s2·…·sm-i)·sw), 推理规则中表示语句执行所引起的指针信息变化， 其中，length(p)计算访问路径p的长度，它是指p 本文主要介绍证明指针性质的推理规则的 由几个有语法意义的部分组成，而不是指p的字符 设计. 个数，例如t->next->data的长度为3. 3.1基本运算的定义 ex pansion(S)用来在别名集合S中加入与其中 在指针逻辑中，程序点的NULL指针集合用W 访问路径相等的访问路径，其定义如下： 表示，悬空指针的集合用D表示，有效指针集合用Ⅱ expansion(S)△ 表示.Ⅱ中指针的具体值并不重要，重要的是它们是 if 3s':(IUUD)).(sns!=) 否相等，因此基于相等与否把它们划分成若干等价 then let(p1,..p.)=S'-S 集合.例如，若Ⅱ中有等价集合{p,q},则它表示p where S'∈（ⅡU{WU{D})AS∩S'I= 和g是相等的有效指针，并且它们不等于其它集合 in SUclosure(p1)U..Uclosure(p.) 中的指针.一个等价集合不能删掉任何元素，也不能 else☑. 分成若干子集，因为这样做都会使指针信息发生变 compression(S)用来删除别名集合S中带环的 化.因此，在指针逻辑的断言演算中，Ⅱ中的等价集 访问路径，其定义如下： 合被看成命题常元；同样，W和D也都被看成命题常 com pression(S)△S-S 元.这些集合只能用本节为指针赋值等设计的推理 where(S'CS)∧(s1·s2·sa)∈S'iff 规则来改变，在语法结构的前后条件中，Ⅱ中的等价 (s1I=e)∧(s2I=e)八(s3I=e)八 集合、W和D虽以集合方式出现，但本质上是逻辑表 ((s1·s3)∈S)Λ(s1·s2=s1). 达式，因此用“八”连接它们.作为缩写，有时用亚表 为清晰起见，上面给出的是closure的一个定 示ⅡANAD. 义，而不是closure的实现算法，例如，该定义没有考 访问路径是满足一定语法要求的字符串，本文 虑面临双向循环链表等带环数据结构时，递归计算 所说的串都是指构成访问路径的串或子串，并用 的终止问题.在closure的实现中是不难把计算的终 Paths表示访问路径集合.若访问路径p是q的前 止等问题考虑进去的.有了closure函数，也很容易 缀，则谓词prefix(p,q)等于true,否则等于false, 删掉访问路径中的环，为方便讨论，我们认为程序中 符号“·”用于两个串的连接；它也用于串的集合S 给出的都是最简访问路径. 和串s的连接，使得S中的每个串连接s: (2)访问路径的单个别名函数alias(p,q) S·s△S'where s'·s∈S'iff s'∈S 该函数从访问路径p的别名集合中任取p',满 若1·s2和s1(s1和s2都不是空串)是值相等的 足p'不以访问路径q的别名为前缀.若找不到这样 访问路径，则称s2是访问路径s·s2·s(s也不是 的p',则结果仍是p. 空串)中的环.符号=表示语法上等同，==表示语 alias(p,q)△ 法上等同测试. let S=(p':closure(p) 下面先定义访问路径上的一些函数，它们都以 Yq':closure(q).-prefix(g',p')} 程序点的指针信息平或Ⅱ为参数，下面统一都将参 in if S==☑then p else p'where p'∈S. 数忽略.这些定义中出现的关键字在一些软件语言 (3)访问路径所在等价集合函数equals(p) 中都出现过，在此忽略它们的解释.需要强调一下， 若p的别名出现在某个等价集合中，则返回该 访问路径p和q在本文中几乎总是指称指针，因此 集合，否则返回空集。 本文也经常直接称它们为指针：但是，在下面的函数 equals(p)△ 中，使用的是它们的语法表达式（访问路径） if3S:Ⅱ.(S∩closure(p)！=)then (1)别名集合的计算 S where S∈ⅡAS∩closure(p)！=☑ closure(p)计算访问路径p的最简别名集合， else☑. 称为p的闭包，它包含且仅包含p所有的无环别名. 下面介绍在推理规则中直接使用的运算或谓 closure(p)△ 词，这些运算表达语句后条件中的平是如何从前条 if length(p)==1 then (p) 件的亚得到的
动推导． （３）把相等的指针表达在一个集合中，便于在 推理规则中表示语句执行所引起的指针信息变化． 本文 主 要 介 绍 证 明 指 针 性 质 的 推 理 规 则 的 设计． ３１ 基本运算的定义 在指针逻辑中，程序点的 ＮＵＬＬ指针集合用! 表示，悬空指针的集合用"表示，有效指针集合用Π 表示．Π 中指针的具体值并不重要，重要的是它们是 否相等，因此基于相等与否把它们划分成若干等价 集合．例如，若Π 中有等价集合｛狆，狇｝，则它表示狆 和狇 是相等的有效指针，并且它们不等于其它集合 中的指针．一个等价集合不能删掉任何元素，也不能 分成若干子集，因为这样做都会使指针信息发生变 化．因此，在指针逻辑的断言演算中，Π 中的等价集 合被看成命题常元；同样，! 和"也都被看成命题常 元．这些集合只能用本节为指针赋值等设计的推理 规则来改变．在语法结构的前后条件中，Π 中的等价 集合、! 和"虽以集合方式出现，但本质上是逻辑表 达式，因此用“∧”连接它们．作为缩写，有时用 Ψ 表 示Π∧!∧"． 访问路径是满足一定语法要求的字符串，本文 所说的串 都 是 指 构 成 访 问 路 径 的 串 或 子 串，并 用 Ｐａｔｈｓ表示访问路径集合．若访问路径狆 是狇 的前 缀，则谓词狆狉犲犳犻狓（狆，狇）等于ｔｒｕｅ，否则等于ｆａｌｓｅ． 符号“·”用于两个串的连接；它也用于串的集合犛 和串狊的连接，使得犛中的每个串连接狊： 犛·狊犛′ｗｈｅｒｅ狊′·狊∈犛′ｉｆｆ狊′∈犛． 若狊１·狊２和狊１（狊１和狊２都不是空串）是值相等的 访问路径，则称狊２是访问路径狊１·狊２·狊３（狊３也不是 空串）中的环．符号≡表示语法上等同，≡≡ 表示语 法上等同测试． 下面先定义访问路径上的一些函数，它们都以 程序点的指针信息 Ψ 或Π 为参数，下面统一都将参 数忽略．这些定义中出现的关键字在一些软件语言 中都出现过，在此忽略它们的解释．需要强调一下， 访问路径狆和狇 在本文中几乎总是指称指针，因此 本文也经常直接称它们为指针；但是，在下面的函数 中，使用的是它们的语法表达式（访问路径）． （１）别名集合的计算 犮犾狅狊狌狉犲（狆）计算访问路径狆 的最简别名集合， 称为狆的闭包，它包含且仅包含狆所有的无环别名． 犮犾狅狊狌狉犲（狆） ｉｆ犾犲狀犵狋犺（狆）＝＝ １ｔｈｅｎ｛狆｝ ｅｌｓｅｌｅｔ狊１·狊２·…·狊狀－１·狊狀≡狆ｉｎ 犮狅犿狆狉犲狊狊犻狅狀（犲狓狆犪狀狊犻狅狀（犮犾狅狊狌狉犲（狊１·狊２·…·狊狀－１））·狊狀）， 其中，犾犲狀犵狋犺（狆）计算访问路径狆 的长度，它是指狆 由几个有语法意义的部分组成，而不是指狆 的字符 个数，例如狋－＞狀犲狓狋－＞犱犪狋犪的长度为３． 犲狓狆犪狀狊犻狅狀（犛）用来在别名集合犛中加入与其中 访问路径相等的访问路径，其定义如下： 犲狓狆犪狀狊犻狅狀（犛） ｉｆ犛′：（Π∪｛!｝∪｛"｝）．（犛∩犛′！＝） ｔｈｅｎｌｅｔ｛狆１，…，狆狀｝＝犛′－犛 ｗｈｅｒｅ犛′∈（Π∪｛!｝∪｛"｝）∧犛∩犛′！＝ ｉｎ犛∪犮犾狅狊狌狉犲（狆１）∪…∪犮犾狅狊狌狉犲（狆狀） ｅｌｓｅ． 犮狅犿狆狉犲狊狊犻狅狀（犛）用来删除别名集合犛 中带环的 访问路径，其定义如下： 犮狅犿狆狉犲狊狊犻狅狀（犛）犛－犛′ ｗｈｅｒｅ（犛′犛）∧（（狊１·狊２·狊３）∈犛′ｉｆｆ （狊１！＝ε）∧（狊２！＝ε）∧（狊３！＝ε）∧ （（狊１·狊３）∈犛）∧（狊１·狊２＝狊１））． 为清晰起见，上面给出的是ｃｌｏｓｕｒｅ的一个定 义，而不是ｃｌｏｓｕｒｅ的实现算法，例如，该定义没有考 虑面临双向循环链表等带环数据结构时，递归计算 的终止问题．在ｃｌｏｓｕｒｅ的实现中是不难把计算的终 止等问题考虑进去的．有了ｃｌｏｓｕｒｅ函数，也很容易 删掉访问路径中的环，为方便讨论，我们认为程序中 给出的都是最简访问路径． （２）访问路径的单个别名函数犪犾犻犪狊（狆，狇） 该函数从访问路径狆的别名集合中任取狆′，满 足狆′不以访问路径狇 的别名为前缀．若找不到这样 的狆′，则结果仍是狆． 犪犾犻犪狊（狆，狇） ｌｅｔ犛＝｛狆′：犮犾狅狊狌狉犲（狆）｜ 狇′：犮犾狅狊狌狉犲（狇）．狆狉犲犳犻狓（狇′，狆′）｝ ｉｎｉｆ犛＝＝ｔｈｅｎ狆ｅｌｓｅ狆′ｗｈｅｒｅ狆′∈犛． （３）访问路径所在等价集合函数犲狇狌犪犾狊（狆） 若狆的别名出现在某个等价集合中，则返回该 集合，否则返回空集． 犲狇狌犪犾狊（狆） ｉｆ犛：Π．（犛∩犮犾狅狊狌狉犲（狆）！＝）ｔｈｅｎ 犛 ｗｈｅｒｅ犛∈Π∧犛∩犮犾狅狊狌狉犲（狆）！＝ ｅｌｓｅ． 下面介绍在推理规则中直接使用的运算或谓 词，这些运算表达语句后条件中的 Ψ 是如何从前条 件的Ψ 得到的． ３ 期 陈意云等：一种用于指针程序安全性证明的指针逻辑 ３７５
376 计算 机 学 报 2008年 (4)有效指针的替换和删除运算 -把q加到Ⅱ中p所在的等价集合. 若S是Ⅱ的一个等价集合，p是一个有效指 (8)有效指针删除是否引起内存泄漏的测试 针，则S/p表示对S中以p的别名为前缀的每个指 leak(p) 针q都用alias(q,p)寻找一个别名来代替它，然后 对有效指针p所在等价集合S进行S/p计算， 将S中出现的p的别名和以它们为前缀的访问路 结果为空集合时则表示会出现内存泄漏；否则不会， 径都删除. leak(p)△equals(p)/p==⑦. S/p△ (9)一些基本谓词的定义 let S'=(q:SI Yp':closure(p).-prefix(p', 下面这些谓词用来测试指针p的别名是否在 q))U(g':Paths|3q:S.3p':closure(p). 某个集合中 (prefix(p',q)∧ pprior},{t,s> 遵守经典逻辑的演算，只是对于指针集合，不能使用 next},则Ⅱ/t={{s,s->next->prior},{s-> AAB→A和A∧B→B,因为这会丢失指针信息. next}〉. 另外，对指针集合需要引入一些专用的规则，受 (5)无效指针替换运算 篇幅限制，在此只列举部分规则。 W\p和D列p分别用来表示将N和D中以p的 (1)判断Ψ是否有矛盾 别名为前缀的访问路径用它们的其它别名来代替 例如，下面的规则表示一个有效指针不能同时 W\△ 出现在两个不同的等价集合中。 (q:NI Yp':closure(p).-prefix(p',q))U 3p:Paths..3S1:Ⅱ.3S2:Ⅱ. q':Pathsl3q:N.3p':closure(p).(prefix(p', (p<:S)∧(p<:S2)A(S!=S2) →false q）Aq'==alias(q,p)}. D八p的定义类似， (2)吸收指针相等关系断言 (6)无效指针删除运算 在PointerC的程序中，条件语句和循环语句的 NIp和D/p分别用来表示将N和D中出现的p 规则会把p==NULL和p==q等形式的断言分 的别名副除。 别引入两条件分支和循环体前程序点的断言中.需 要一些规则来把它们吸收到指针集合中或者推导出 Wlp△{q:W|7(q∈closure(p))}: 矛盾，下面列出其中的一部分： N/八p1,p2,…,p.}△(N/p1)/p2)…/pn). (p<:Ⅱ) D/p的定义类似， (7)指针添加运算 业A(p!=NULL)→业 (p<:W) 并集算符“U”直接用来表示向指针集合中添加 ΨA(p！=NULL)→false 一个指针，例如SU{p}.我们为Ⅱ中等价集合的增 <:N 加、剔除和替换使用新的记号，它们基于集合运算符 业A(p==NULL)→亚： 号“U”和“一”及它们的组合来定义。 p<:Ⅱ Ⅱ+p△ΠU{{p}} Ψ∧(p==NULL)→false 一把仅由p构成的等价集合加到Ⅱ中； (3)别名替换 Ⅱ-p△Ⅱ-{equals(p)} 有时需要用下面的规则来进行别名替换： 一删掉Ⅱ中p所在的等价集合； q∈closure(p) Ⅱadd g to p△（Ⅱ-p)U{equals(p)U{q}} Ψ∧Q→Ψ∧Q[p←-q]
（４）有效指针的替换和删除运算 若犛 是Π 的一个 等 价 集 合，狆 是 一 个 有 效 指 针，则犛／狆表示对犛 中以狆 的别名为前缀的每个指 针狇都用犪犾犻犪狊（狇，狆）寻找一个别名来代替它，然后 将犛 中出现的狆 的别名和以它们为前缀的访问路 径都删除． 犛／狆 ｌｅｔ犛′＝｛狇：犛｜狆′：犮犾狅狊狌狉犲（狆）．狆狉犲犳犻狓（狆′， 狇）｝∪｛狇′：犘犪狋犺狊｜狇：犛．狆′：犮犾狅狊狌狉犲（狆）． （狆狉犲犳犻狓（狆′，狇）∧ 狇′≡≡犪犾犻犪狊（狇，狆））｝ ｉｎ｛狇：犛′｜（狇∈犮犾狅狊狌狉犲（狆））∧ 狆′：犮犾狅狊狌狉犲（狆）．狆狉犲犳犻狓（狆′，狇）｝． 若需要对Π 中每个犛 进行替换和删除狆 的运 算，则用Π／狆表示． 当有效指针狇被赋予一个不等于狇 的值时，狇 和以狇 为前缀的访问路径都需要从原来的等价集合 中删 除，例 如，若 Π＝ ｛｛狊，狋 －＞狆狉犻狅狉｝，｛狋，狊 －＞ 狀犲狓狋｝｝，则 Π／狋＝｛｛狊，狊－＞狀犲狓狋－＞狆狉犻狅狉｝，｛狊－＞ 狀犲狓狋｝｝． （５）无效指针替换运算 !＼狆 和"＼狆 分别用来表示将! 和"中以狆 的 别名为前缀的访问路径用它们的其它别名来代替． !＼狆 ｛狇：!｜狆′：犮犾狅狊狌狉犲（狆）．狆狉犲犳犻狓（狆′，狇）｝∪ ｛狇′：犘犪狋犺狊｜狇：!．狆′：犮犾狅狊狌狉犲（狆）．（狆狉犲犳犻狓（狆′， 狇）∧狇′≡≡犪犾犻犪狊（狇，狆））｝． "＼狆的定义类似． （６）无效指针删除运算 !／狆和"／狆分别用来表示将! 和"中出现的狆 的别名删除． !／狆｛狇：!｜（狇∈犮犾狅狊狌狉犲（狆））｝； !／｛狆１，狆２，…，狆狀｝（（（!／狆１）／狆２）…／狆狀）． "／狆的定义类似． （７）指针添加运算 并集算符“∪”直接用来表示向指针集合中添加 一个指针，例如犛∪｛狆｝．我们为Π 中等价集合的增 加、删除和替换使用新的记号，它们基于集合运算符 号“∪”和“－”及它们的组合来定义． Π＋狆Π∪｛｛狆｝｝ ———把仅由狆构成的等价集合加到Π 中； Π－狆Π－｛犲狇狌犪犾狊（狆）｝ ———删掉Π 中狆 所在的等价集合； Πａｄｄ狇ｔｏ狆（Π－狆）∪｛犲狇狌犪犾狊（狆）∪｛狇｝｝ ———把狇加到Π 中狆 所在的等价集合． （８）有效 指 针 删 除 是 否 引 起 内 存 泄 漏 的 测 试 犾犲犪犽（狆） 对有效指针狆所在等价集合犛 进行犛／狆 计算， 结果为空集合时则表示会出现内存泄漏；否则不会． 犾犲犪犽（狆）犲狇狌犪犾狊（狆）／狆＝＝． （９）一些基本谓词的定义 下面这些谓词用来测试指针狆 的别名是否在 某个集合中． 狆＜：Π犛：Π．（犛∩犮犾狅狊狌狉犲（狆）！＝）； 狆＜：犛犛∩犮犾狅狊狌狉犲（狆）！＝ （犛是Π 中的一个等价集合）； 狆＜：!（! ∩犮犾狅狊狌狉犲（狆））！＝； 狆＜："（"∩犮犾狅狊狌狉犲（狆））！＝； 狆＜：Ψ（狆＜：Π）∨（狆＜：! ）∨（狆＜："）． ３２ 断言演算 把指针集合看成常元，断言上的演算基本上仍 遵守经典逻辑的演算，只是对于指针集合，不能使用 犃∧犅犃 和犃∧犅犅，因为这会丢失指针信息． 另外，对指针集合需要引入一些专用的规则，受 篇幅限制，在此只列举部分规则． （１）判断 Ψ 是否有矛盾 例如，下面的规则表示一个有效指针不能同时 出现在两个不同的等价集合中． 狆：犘犪狋犺狊．犛１：Π．犛２：Π． （（狆＜：犛１）∧（狆＜：犛２）∧（犛１！＝犛２）） Ψｆａｌｓｅ ． （２）吸收指针相等关系断言 在 ＰｏｉｎｔｅｒＣ的程序中，条件语句和循环语句的 规则会把狆＝＝ＮＵＬＬ 和狆＝＝狇等形式的断言分 别引入两条件分支和循环体前程序点的断言中．需 要一些规则来把它们吸收到指针集合中或者推导出 矛盾，下面列出其中的一部分： （狆＜：Π） Ψ∧（狆！＝ＮＵＬＬ）Ψ ； （狆＜：! ） Ψ∧（狆！＝ＮＵＬＬ）ｆａｌｓｅ； 狆＜：! Ψ∧（狆＝＝ＮＵＬＬ）Ψ ； 狆＜：Π Ψ∧（狆＝＝ＮＵＬＬ）ｆａｌｓｅ． （３）别名替换 有时需要用下面的规则来进行别名替换： 狇∈犮犾狅狊狌狉犲（狆） Ψ∧犙 Ψ∧犙［狆←狇］． ３７６ 计 算 机 学 报 ２００８年
3期 陈意云等：一种用于指针程序安全性证明的指针逻辑 377 3.3公理和推理规则 (4)复合、条件和循环语句的规则以及推论规 下面给出联系到PointerC各种语句的公理和 则等仍然使用Hoare逻辑的规则， 推理规则.这些规则体现了相应语句引起的指针集 (5)分配空间语句p=malloc(T),其中T是类 合的增、减和替换.在下面的所有规则中，其前提中的 型.若T是结构类型，r1,r2,…,rn是其中的指针域 断言都是基于语句前的那个程序点的亚来计算的， 在该类型中的访问路径， (1)指针之间的赋值语句p=q(包括q是常量 (a)p是NULL指针 NULL的情况，略去了g是悬空指针的规则)； r,…,p>r})》 3S:Ⅱ.(p q{((Ⅱ/p)add p to q)∧W\pAD叭p} 方，…，p>r。,则可把该语句看成语句序列 (c)p是NULL指针，q是有效指针 p->r=NULL;…;p->rm=NULL;free(p)来 pr1,…,p->rm}∧(DUequals(p)》 {ⅡANAD}p=q{(Ⅱadd p to q)AN∧D/p} (e)p是有效指针，q等于NULL 4 证明实例 pl)∧tree(p>r)为真： 缀的情况)，则除了用先前指针赋值的规则外，还需 tree(p)A(p!=NULL) 要用下面的赋值公理。 (p)xV((p)Atree(p-l)Atree(p-r)))A {ΨAQ}p=q{亚∧Q[r←p]》 (!=NULL) (r是closure(p)中的一个其它成员， 台({p}wA(p!=NULL)V 平由(1)的规则从平得到). ((p)Ntree(p-)Ntree(p-r)A(p!=NULL)) 换一种说法是，对指针p赋值时，对p的别名 falseV((p)Atree(p-1)Atree(p-r)) 替换还需要出现在亚以外的断言中.该规则也用在 台{p}∧tree(p->l)A tree(p->r). malloc和free语句场合. 程序设计者只要给出函数前后条件和循环不变
３３ 公理和推理规则 下面给出联系到 ＰｏｉｎｔｅｒＣ 各种语句的公理和 推理规则．这些规则体现了相应语句引起的指针集 合的增、减和替换．在下面的所有规则中，其前提中的 断言都是基于语句前的那个程序点的Ψ 来计算的． （１）指针之间的赋值语句狆＝狇（包括狇是常量 ＮＵＬＬ的情况，略去了狇是悬空指针的规则）； 不同情况的指针赋值用不同的规则． （ａ）狆和狇 是相等的有效指针，或都等于 ＮＵＬＬ 犛：Π．（狆＜：犛∧狇＜：犛）∨ （狆＜：!∧（狇＜：! ∨狇≡≡ ＮＵＬＬ）） ｛Π∧!∧"｝狆＝狇｛Π∧!∧"｝ ． （ｂ）狆和狇 是不相等的有效指针 犛１：Π．犛２：Π．（犛１！＝犛２∧ 狆＜：犛１∧狇＜：犛２）∧犾犲犪犽（狆） ｛Π∧!∧"｝狆＝ 狇｛（（Π／狆）ａｄｄ狆ｔｏ狇）∧!＼狆∧"＼狆｝ ． （ｃ）狆是 ＮＵＬＬ指针，狇是有效指针 狆＜：!∧狇＜：Π ｛Π∧!∧"｝狆＝狇｛（Πａｄｄ狆ｔｏ狇）∧!／狆∧"｝． （ｄ）狆是悬空指针，狇是有效指针 狆＜："∧狇＜：Π ｛Π∧!∧"｝狆＝狇｛（Πａｄｄ狆ｔｏ狇）∧!∧"／狆｝． （ｅ）狆是有效指针，狇等于 ＮＵＬＬ 狆＜：Π∧（狇＜：! ∨狇 ≡≡ ＮＵＬＬ）∧犾犲犪犽（狆） ｛Π∧!∧"｝狆＝狇｛Π／狆∧（!＼狆∪｛狆｝）∧"＼狆｝． （ｆ）狆是悬空指针，狇等于 ＮＵＬＬ 狆＜："∧（狇＜：! ∨狇 ≡≡ ＮＵＬＬ） ｛Π∧!∧"｝狆＝狇｛Π∧（! ∪｛狆｝）∧"／狆｝． （２）非指针类型的赋值公理 ｛Ψ∧（犙［狔１←狓］…［狔狀←狓］［狓←犲］）｝狓＝犲｛Ψ∧犙｝ （狔１，狔２，…，狔狀构成犮犾狅狊狌狉犲（狓）的所有成员）． 这是考虑了别名情况后的 Ｈｏａｒｅ逻辑赋值公 理，它不改变 Ψ．该公理中的断言 犙 只含整型数据 的子断言．以下使用的犙 也都满足这个限制． （３）对于指针类型的赋值，若前条件是 Ψ∧犙， 并且犙 中也有访问路径（包括作为犙 中访问路径前 缀的情况），则除了用先前指针赋值的规则外，还需 要用下面的赋值公理． ｛Ψ∧犙｝狆＝狇｛Ψ′∧犙［狉←狆］｝ （狉是犮犾狅狊狌狉犲（狆）中的一个其它成员， Ψ′由（１）的规则从 Ψ 得到）． 换一种说法是，对指针狆 赋值时，对狆 的别名 替换还需要出现在Ψ 以外的断言中．该规则也用在 ｍａｌｌｏｃ和ｆｒｅｅ语句场合． （４）复合、条件和循环语句的规则以及推论规 则等仍然使用 Ｈｏａｒｅ逻辑的规则． （５）分配空间语句狆＝犿犪犾犾狅犮（犜），其中 犜 是类 型．若犜 是结构类型，狉１，狉２，…，狉狀是其中的指针域 在该类型中的访问路径． （ａ）狆是 ＮＵＬＬ指针 狆＜：! ｛Π∧!∧"｝狆＝犿犪犾犾狅犮（犜）｛（Π＋狆）∧!／狆∧ （"∪｛狆－＞狉１，…，狆－＞狉狀｝）｝ ． （ｂ）狆是悬空指针的规则和（ａ）类似． （ｃ）狆是有效指针．把该语句看成语句序列狆＝ ＮＵＬＬ；狆＝犿犪犾犾狅犮（犜），并将相应的规则用于证明． （６）释放空间语句犳狉犲犲（狆） 下面的规则用于狆所指向对象不含有效指针的场 合．若从Π知道狆所指向的对象中含有有效指针狆 －＞ 狉１，…，狆 －＞狉狀，则 可 把 该 语 句 看 成 语 句 序 列 狆 －＞狉１＝ＮＵＬＬ；…；狆 －＞狉狀 ＝ＮＵＬＬ；犳狉犲犲（狆）来 进行证明．这样做的目的是简化犳狉犲犲（狆）的规则． 狆＜：Π ｛Π∧!∧"｝犳狉犲犲（狆）｛（Π－狆）∧ （!／｛狆－＞狉１，…，狆－＞狉狀｝∧（"∪犲狇狌犪犾狊（狆）｝ ． ４ 证明实例 我们已经用指针逻辑系统证明了单链表、双向 链表和二叉树等数据结构的一些函数．本节以删除 二叉排序树一个结点并重接它的左或右子树的函数 ｓｔｒｕｃｔｎｏｄｅ犇犲犾犲狋犲犖狅犱犲（狊狋狉狌犮狋狀狅犱犲 狆）为例． 在证明该函数时，参数所指向的树上，有效指针 和 ＮＵＬＬ 指针的布局是不清楚的，但它必须满足 树的定义．若树结点定义是ｓｔｒｕｃｔｎｏｄｅ｛ｉｎｔ犱犪狋犪； ｓｔｒｕｃｔｎｏｄｅ犾，狉；｝，那么以狆 为根结点指针的树 的定义如下： 狋狉犲犲（狆）｛狆｝犖∨（｛狆｝∧狋狉犲犲（狆－＞犾）∧狋狉犲犲（狆－＞狉））． 如果狆不是空指针，通过下面的演算可以知道狆 是有效指针并且狋狉犲犲（狆－＞犾）∧狋狉犲犲（狆－＞狉）为真： 狋狉犲犲（狆）∧（狆！＝ＮＵＬＬ） ≡（｛狆｝犖∨（｛狆｝∧狋狉犲犲（狆－＞犾）∧狋狉犲犲（狆－＞狉）））∧ （狆！＝ＮＵＬＬ） （｛狆｝犖 ∧（狆！＝ＮＵＬＬ））∨ （｛狆｝∧狋狉犲犲（狆－＞犾）∧狋狉犲犲（狆－＞狉）∧（狆！＝ＮＵＬＬ）） 犳犪犾狊犲∨（｛狆｝∧狋狉犲犲（狆 －＞犾）∧狋狉犲犲（狆 －＞狉）） ｛狆｝∧狋狉犲犲（狆 －＞犾）∧狋狉犲犲（狆 －＞狉）． 程序设计者只要给出函数前后条件和循环不变 ３ 期 陈意云等：一种用于指针程序安全性证明的指针逻辑 ３７７
378 计算 机 学报 2008年 式，其它程序点的断言可以通过指针逻辑得到.图1 来表示Ⅱ，W和D用下标{…}x和{…}D来区分，它们 仅对形参p的左右子树都非空的大部分程序点插 为空时则不出现在断言中.我们没有给出return语 入了断言（该函数要求参数是非空树），其它部分在 句后的断言，因为本文没有提供return语句的推理 关键点插入了断言.在断言中，直接列出各等价集合 规则. p!=NULLAtree(p)) struct node *DeleteNode(struct node *p) struct node *q.*s: p)Atree(p>l)Atree(p->r)Aiq.s)D) if(r==NULL) /￥右子树为空，只需重接它的左子树/ q=p:s=pl:free(q):(p.qlp Atree(s))return s:} else if(==NULL) /左子树为空，只需重接它的右子树/ (q=p:s=p>r:free(q):(s)Aip.q)p Atree(s))retum s:} else /左右子树均不空/ {(p)Aip->1)Aip->r)Alg.s)D Atree(p>D Atree(p->r)} q=p:s=p>l: if(sr==NULL) /重接g的左子树*/ q>1=s->1:p->data=s->data:free(s):p.q)Atree(p))return p:} else (p.q)Aipr)Atp->1.s)hisr)Atree(pID Atree(plr)Atree(pr)) g=s:s=8->r: {3n:N.({p}A{p->ryAi:0n-1.{p->l(->r)}A{p->(->r),g}A{p->l(->r)+1,s}N Hi:0n.tree(p->l(->r)->l)Atree(p->l(->r)"+1)Atree(p->r)》/x循环不变式*/ while(s->r！=NULL) /￥转左，然后向右前进到尽头/ (q=s:s=s>r:) {3n:N.({p}{p->r}AHi:0n-1.{p->l(->r)}A{p->l(->r)",q}A{p->l(->r)+1,}A{s->r}NN Yi:0.n.tree(p(r)iD Atree(p(r)+1)Atree(pr))) p->data=s->data: g->r=s->l: /*重接q的右子树*/ {3n:N.({p}A{p->r}Ai:0n-1.{p->1(->r}A{p->l(->r)",g}A{s}A({s->l,g->r}A{s->r}v) Vis>r.sqrx)AYi:0.n.tree(p(r)iD)Atree(p(r)+1)Atree(pr))) free(s): (3n:N.(p)Aipr)AYi:0.n-1.p(r)i)Aipr)"q)A(qr)Viqr)x)Ats)DA Yi:0.n.tree(p(r)i)Atree(p(r)"+1)Atree(pr))) /如果在返回调用者前，忽略g和s的信息，可以得到{p}Atree(p)}*/ return P: 图1删除二叉树结点的程序和断言 在指向对象集合的精度上，不同的应用要求不 5 相关工作 同的粒度.不同的精度要求采用不同的分析方法，有 流敏感和流不敏感的区分，路径敏感和路径不敏感 Hoare逻辑的一个重要特征是用变量代换来抓 的区分以及过程内和过程间的区分.例如，Steens-- 住赋值的语义，本文的指针逻辑系统本质上是一种 gaard对C语言的一个禁止指针强制和指针算术等 指针分析工具，它用访问路径的增加、删除和替换来 的子集，描述了一种基于类型推导的过程间的、流不 抓住指针操作带来的影响.指针分析已经研究了20 敏感的和路径不敏感的指针分析).该方法基于变 多年，历史上的指针分析主要回答：对指针类型的变 量的存储模型，定义了类型系统及推导指针指向的 量，它们运行时可能指向的对象集合是什么.这样的 规则集合，用以分析运行时指针变量可能指向的对 指针分析可用在程序的静态分析和优化的很多方 象集合.Berndl等首先把二叉决策图用于流不敏感 面，如寄存器分配和常量传播所需的活跃变量分析， 和路径不敏感的指针分析[町，比较成功地解决了这 还有像NULL指针脱引用这样的潜在运行错误的 类分析的效率问题.Hind对这方面的研究做了一个 静态检查等.近年来它还用在发现危及安全的缓冲 总结町，列出了一些待解决的问题. 区溢出和打印格式串错误等.和其它静态技术类似， 出于软件安全方面的要求，本文实现的是精确 指针分析受到可判定性问题的困扰，对大多数语言 而不是近似的指针分析，因此在不影响语言功能的 来说，所得到的解总是一个近似 情况下，对C语言中难以判定的指针使用方式进行
式，其它程序点的断言可以通过指针逻辑得到．图１ 仅对形参狆 的左右子树都非空的大部分程序点插 入了断言（该函数要求参数是非空树），其它部分在 关键点插入了断言．在断言中，直接列出各等价集合 来表示Π，! 和"用下标｛…｝犖 和｛…｝犇 来区分，它们 为空时则不出现在断言中．我们没有给出ｒｅｔｕｒｎ语 句后的断言，因为本文没有提供ｒｅｔｕｒｎ语句的推理 规则． ｛狆！＝ＮＵＬＬ∧狋狉犲犲（狆）｝ ｓｔｒｕｃｔｎｏｄｅ犇犲犾犲狋犲犖狅犱犲（ｓｔｒｕｃｔｎｏｄｅ狆） ｛ ｓｔｒｕｃｔｎｏｄｅ狇，狊； ｛｛狆｝∧狋狉犲犲（狆 －＞犾）∧狋狉犲犲（狆 －＞狉）∧｛狇，狊｝犇｝ ｉｆ（狆 －＞狉＝＝ＮＵＬＬ） ／右子树为空，只需重接它的左子树／ ｛狇＝狆；狊＝狆 －＞犾；犳狉犲犲（狇）；｛｛狆，狇｝犇 ∧狋狉犲犲（狊）｝ｒｅｔｕｒｎ狊；｝ ｅｌｓｅｉｆ（狆 －＞犾＝＝ＮＵＬＬ） ／左子树为空，只需重接它的右子树／ ｛狇＝狆；狊＝狆 －＞狉；犳狉犲犲（狇）；｛｛狊｝∧｛狆，狇｝犇 ∧狋狉犲犲（狊）｝ｒｅｔｕｒｎ狊；｝ ｅｌｓｅ ／左右子树均不空／ ｛ ｛｛狆｝∧｛狆 －＞犾｝∧｛狆 －＞狉｝∧｛狇，狊｝犇 ∧狋狉犲犲（狆 －＞犾）∧狋狉犲犲（狆 －＞狉）｝ 狇＝狆；狊＝狆 －＞犾； ｉｆ（狊－＞狉＝＝ＮＵＬＬ） ／重接狇的左子树／ ｛狇－＞犾＝狊－＞犾；狆 －＞犱犪狋犪＝狊－＞犱犪狋犪；犳狉犲犲（狊）；｛｛狆，狇｝∧狋狉犲犲（狆）｝ｒｅｔｕｒｎ狆；｝ ｅｌｓｅ ｛ ｛｛狆，狇｝∧｛狆 －＞狉｝∧｛狆 －＞犾，狊｝∧｛狊－＞狉｝∧狋狉犲犲（狆 －＞犾－＞犾）∧狋狉犲犲（狆 －＞犾－＞狉）∧狋狉犲犲（狆 －＞狉）｝ 狇＝狊；狊＝狊－＞狉； ｛狀：犖!（｛狆｝∧｛狆 －＞狉｝∧犻：０!狀! －１．｛狆 －＞犾（－＞狉）犻｝∧｛狆 －＞犾（－＞狉）狀，狇｝∧｛狆 －＞犾（－＞狉）狀＋１，狊｝∧ 犻：０!狀! 狋!狉犲犲（狆 －＞犾（－＞狉）犻－＞犾）∧狋狉犲犲（狆 －＞犾（－＞狉）狀＋１）∧狋狉犲犲（狆 －＞狉））｝ ／／循环不变式／／ ｗｈｉｌｅ（狊－＞狉！＝ＮＵＬＬ） ／转左，然后向右前进到尽头／ ｛狇＝狊；狊＝狊－＞狉；｝ ｛狀：犖!（｛狆｝∧｛狆 －＞狉｝∧犻：０!狀! －１．｛狆 －＞犾（－＞狉）犻｝∧｛狆 －＞犾（－＞狉）狀，狇｝∧｛狆 －＞犾（－＞狉）狀＋１，狊｝∧｛狊－＞狉｝犖 ∧ 犻：０!狀! ．狋狉犲犲（狆 －＞犾（－＞狉）犻－＞犾）∧狋狉犲犲（狆 －＞犾（－＞狉）狀＋１）∧狋狉犲犲（狆 －＞狉））｝ 狆 －＞犱犪狋犪＝狊－＞犱犪狋犪； 狇－＞狉＝狊－＞犾； ／重接狇的右子树／ ｛狀：犖．（｛狆｝∧｛狆 －＞狉｝∧犻：０!狀! －１．｛狆 －＞犾（－＞狉）犻｝∧｛狆 －＞犾（－＞狉）狀，狇｝∧｛狊｝∧（（｛狊－＞犾，狇－＞狉｝∧｛狊－＞狉｝犖） ∨｛狊－＞狉，狊－＞犾，狇－＞狉｝犖）∧犻：０!狀! ．狋狉犲犲（狆 －＞犾（－＞狉）犻－＞犾）∧狋狉犲犲（狆 －＞犾（－＞狉）狀＋１）∧狋狉犲犲（狆 －＞狉））｝ 犳狉犲犲（狊）； ｛狀：犖．（｛狆｝∧｛狆 －＞狉｝∧犻：０!狀! －１．｛狆 －＞犾（－＞狉）犻｝∧｛狆 －＞犾（－＞狉）狀，狇｝∧（｛狇－＞狉｝∨｛狇－＞狉｝犖）∧｛狊｝犇 ∧ 犻：０!狀! ．狋狉犲犲（狆 －＞犾（－＞狉）犻－＞犾）∧狋狉犲犲（狆 －＞犾（－＞狉）狀＋１）∧狋狉犲犲（狆 －＞狉））｝ ／如果在返回调用者前，忽略狇和狊的信息，可以得到｛｛狆｝∧狋狉犲犲（狆）｝／ ｒｅｔｕｒｎ狆； ｝ ｝ ｝ 图 １ 删除二叉树结点的程序和断言 ５ 相关工作 Ｈｏａｒｅ逻辑的一个重要特征是用变量代换来抓 住赋值的语义，本文的指针逻辑系统本质上是一种 指针分析工具，它用访问路径的增加、删除和替换来 抓住指针操作带来的影响．指针分析已经研究了２０ 多年，历史上的指针分析主要回答：对指针类型的变 量，它们运行时可能指向的对象集合是什么．这样的 指针分析可用在程序的静态分析和优化的很多方 面，如寄存器分配和常量传播所需的活跃变量分析， 还有像 ＮＵＬＬ指针脱引用这样的潜在运行错误的 静态检查等．近年来它还用在发现危及安全的缓冲 区溢出和打印格式串错误等．和其它静态技术类似， 指针分析受到可判定性问题的困扰，对大多数语言 来说，所得到的解总是一个近似． 在指向对象集合的精度上，不同的应用要求不 同的粒度．不同的精度要求采用不同的分析方法，有 流敏感和流不敏感的区分，路径敏感和路径不敏感 的区分以及过程内和过程间的区分．例如，Ｓｔｅｅｎｓ ｇａａｒｄ对 Ｃ语言的一个禁止指针强制和指针算术等 的子集，描述了一种基于类型推导的过程间的、流不 敏感的和路径不敏感的指针分析［８］ ．该方法基于变 量的存储模型，定义了类型系统及推导指针指向的 规则集合，用以分析运行时指针变量可能指向的对 象集合．Ｂｅｒｎｄｌ等首先把二叉决策图用于流不敏感 和路径不敏感的指针分析［９］，比较成功地解决了这 类分析的效率问题．Ｈｉｎｄ对这方面的研究做了一个 总结［１０］，列出了一些待解决的问题． 出于软件安全方面的要求，本文实现的是精确 而不是近似的指针分析，因此在不影响语言功能的 情况下，对 Ｃ语言中难以判定的指针使用方式进行 ３７８ 计 算 机 学 报 ２００８年
3期 陈意云等：一种用于指针程序安全性证明的指针逻辑 379 了限制，正是这种限制使得本文可以采用与通常的 逻辑系统，它可用来证明指针程序是否满足定型规 C语言指针分析完全不同的方法. 则的附加条件，以支持指针程序的安全性证明及其 本文的指针逻辑和分离逻辑(separation log- 它性质证明.我们已经利用证明辅助工具Cog「1]完 ic)u-)都是通过对Hoare逻辑的拓展，来证明在共 成了指针逻辑对PointerC操作语义可靠的证明. 享易变数据结构(shared mutable data structure)上 PointerC及其类型系统、指针逻辑的断言语言、指针 带指针操作的程序的性质.分离逻辑适合于对使用 逻辑可靠性证明、一些应用程序的证明实例以及基 这些数据结构的低级命令式语言的程序进行推理. 于第1节所提框架的出具证明编译器的一些实现工 这样的简单语言包括了访问和修改共享结构的命 作，可在我们的项目网页http:/ssg.ustcsz..edu. 令，包括了显式分配存储和释放存储的命令，分离逻 cn/lss/doc/index.html上找到. 辑在断言语言中引入了“分离合取”等空间连接词， 下一步我们将考虑放宽对指针运算的约束范 它们可用来断言存储空间分离部分的性质，例如 围，有限制地允许指针算术，以适应编程中经常使用 P*Q表示P和Q在两部分不相交的存储空间上 的calloc存储分配.加上面向对象的语言构造，使程 分别成立.分离提供了分离逻辑最关键的特征一 序性质证明具有更好的模块性也是下一步需要考虑 局部推理.分离逻辑还使用在抽象数据结构上递归 的内容 定义的谓词，这些谓词允许简洁和灵活地描述有控 制的共享的结构.分离逻辑在证明单链表、双向链表 参考文献 和二叉树等易变数据结构的程序上的成功已经展示 出它的优点.近来分离逻辑已经出现在用低级语言 [1]Morrisett G.Walker D.Crary K,Glew N.From system F 写的操作系统一些核心程序的正确性证明上] to typed assembly language//Proceedings of the 25th ACM 本文的指针逻辑和分离逻辑的主要区别有两 Symposium on Principles of Programming Languages.San 点.分离逻辑面向低级编程语言，指针逻辑面向高级 Diego,1998:85-97 编程语言.另外，由于PointerC不允许指针指向动 [2]Mandelbaum Y,Walker D.Harper R.An effective theory of 态申请存储块的中间，那么从指针是否相等就可以 type refinements//Proceedings of the 8th International Con- ference on Functional Programming.Uppsala,Sweden. 判断它们指向的空间是否分离，因此指针逻辑不必 2003:213-225 引入分离合取这样的空间连接词. [3]Necula G.Proof-carrying code//Proceedings of the 24th Bornat也采用Hoare逻辑来证明指针程序的性 ACM Symposium On Principles of Programming Languages. 质，采用类似方法的还有Mehta和Nipkow[]. New York,1997:106-119 Bornat把堆看成由指针索引的一群对象，把对象看 [4]Appel A W.Foundational proof-carrying code//Proceedings 成由名字索引的一组成员，然后把Hoare逻辑赋值 of the 16th Annual IEEE Symposium on Logic in Computer Science.Baston.Massachusetts.USA.2001:247-258 公理拓展成能用于对象成员赋值的场合，用它来证 [5]Yu D.Hamid N A.Shao Z.Building certified libraries for 明一些指针程序的性质.由指针索引相等与否来判 PCC:Dynamic storage allocation.Science of Computer Pro- 断别名，基于此来拓展赋值公理是他和我们方法的 gramming,2004,50(1-3):101-127 共同特征，但是他的方法只能用于不提供free操作 [6]Feng X.Shao Z,Vaynberg A,Xiang S,Ni Z.Modular Ver- 并且有无用单元收集(garbage collection)的语言， ification of Assembly Code with Stack-Based Control Ab- 我们的方法虽然适用于提供free操作的场合，但是 stractions//Proceedings of the 2006 ACM SIGPLAN Confer- 却导致了指针逻辑的复杂.例如，在free(p)时，为防 ence on Programming Language Design and Implementation. Ottawa.Canada.2006:401-414 止悬空指针引用，需要保证以后不会用p或与p相 [7]Xi H.Applied type system:Extended abstract//Proceedings 等的指针去访问：再例如，在对有效指针p赋值时， of TYPES 2003.LNCS 3085.Springer-Verlag.2004:394- 为防止出现内存泄漏，需要知道有和p相等的指针 408 存在，这就导致指针逻辑像是从前向后计算最强后 [8]Steensgaard B.Points-to analysis in almost linear time//Pro- 条件，而不是从后向前计算最弱前条件. ceedings of the 23th Annual ACM Symposium on Principles of Programming Languages.Florida.USA.1996:32-41 [9]Berndl M,Lhotak O.Qian F,Hendren L.Umanee N. 6 结束语 Points-to analysis using BDDs//Proceedings of the ACM SIGPLAN 2003 Conference on Programming Language De- 本文提出了一种可对指针程序进行精确分析的 sign and Implementation.San Diego,2003:103-114
了限制，正是这种限制使得本文可以采用与通常的 Ｃ语言指针分析完全不同的方法． 本 文 的 指 针 逻 辑 和 分 离 逻 辑 （ｓｅｐａｒａｔｉｏｎｌｏｇ ｉｃ）［１１１２］都是通过对 Ｈｏａｒｅ逻辑的拓展，来证明在共 享易变数据结构（ｓｈａｒｅｄｍｕｔａｂｌｅｄａｔａｓｔｒｕｃｔｕｒｅ）上 带指针操作的程序的性质．分离逻辑适合于对使用 这些数据结构的低级命令式语言的程序进行推理． 这样的简单语言包括了访问和修改共享结构的命 令，包括了显式分配存储和释放存储的命令．分离逻 辑在断言语言中引入了“分离合取”等空间连接词， 它们可 用 来 断 言 存 储 空 间 分 离 部 分 的 性 质，例 如 犘犙 表示犘 和犙 在两部分不相交的存储空间上 分别成立．分离提供了分离逻辑最关键的特征——— 局部推理．分离逻辑还使用在抽象数据结构上递归 定义的谓词，这些谓词允许简洁和灵活地描述有控 制的共享的结构．分离逻辑在证明单链表、双向链表 和二叉树等易变数据结构的程序上的成功已经展示 出它的优点．近来分离逻辑已经出现在用低级语言 写的操作系统一些核心程序的正确性证明上［１３］ ． 本文的指针逻辑和分离逻辑的主要区别有两 点．分离逻辑面向低级编程语言，指针逻辑面向高级 编程语言．另外，由于 ＰｏｉｎｔｅｒＣ 不允许指针指向动 态申请存储块的中间，那么从指针是否相等就可以 判断它们指向的空间是否分离，因此指针逻辑不必 引入分离合取这样的空间连接词． Ｂｏｒｎａｔ也采用 Ｈｏａｒｅ逻辑来证明指针程序的性 质［１４］，采用类似方法的还有 Ｍｅｈｔａ和 Ｎｉｐｋｏｗ［１５］ ． Ｂｏｒｎａｔ把堆看成由指针索引的一群对象，把对象看 成由名字索引的一组成员，然后把 Ｈｏａｒｅ逻辑赋值 公理拓展成能用于对象成员赋值的场合，用它来证 明一些指针程序的性质．由指针索引相等与否来判 断别名，基于此来拓展赋值公理是他和我们方法的 共同特征，但是他的方法只能用于不提供ｆｒｅｅ操作 并且有无用单元收集（ｇａｒｂａｇｅｃｏｌｌｅｃｔｉｏｎ）的语言． 我们的方法虽然适用于提供ｆｒｅｅ操作的场合，但是 却导致了指针逻辑的复杂．例如，在犳狉犲犲（狆）时，为防 止悬空指针引用，需要保证以后不会用狆 或与狆 相 等的指针去访问；再例如，在对有效指针狆 赋值时， 为防止出现内存泄漏，需要知道有和狆 相等的指针 存在．这就导致指针逻辑像是从前向后计算最强后 条件，而不是从后向前计算最弱前条件． ６ 结束语 本文提出了一种可对指针程序进行精确分析的 逻辑系统，它可用来证明指针程序是否满足定型规 则的附加条件，以支持指针程序的安全性证明及其 它性质证明．我们已经利用证明辅助工具 Ｃｏｑ［１６］完 成了 指 针 逻 辑 对 ＰｏｉｎｔｅｒＣ 操 作 语 义 可 靠 的 证 明． ＰｏｉｎｔｅｒＣ及其类型系统、指针逻辑的断言语言、指针 逻辑可靠性证明、一些应用程序的证明实例以及基 于第１节所提框架的出具证明编译器的一些实现工 作，可 在 我 们 的 项 目 网 页 ｈｔｔｐ：／／ｓｓｇ．ｕｓｔｃｓｚ．ｅｄｕ． ｃｎ／ｌｓｓ／ｄｏｃ／ｉｎｄｅｘ．ｈｔｍｌ上找到． 下一步我们将考虑放宽对指针运算的约束范 围，有限制地允许指针算术，以适应编程中经常使用 的ｃａｌｌｏｃ存储分配．加上面向对象的语言构造，使程 序性质证明具有更好的模块性也是下一步需要考虑 的内容． 参 考 文 献 ［１］ ＭｏｒｒｉｓｅｔｔＧ，ＷａｌｋｅｒＤ，ＣｒａｒｙＫ，Ｇｌｅｗ Ｎ．Ｆｒｏｍｓｙｓｔｅｍ Ｆ ｔｏｔｙｐｅｄａｓｓｅｍｂｌｙｌａｎｇｕａｇｅ／／Ｐｒｏｃｅｅｄｉｎｇｓｏｆｔｈｅ２５ｔｈ ＡＣＭ Ｓｙｍｐｏｓｉｕｍ ｏｎ ＰｒｉｎｃｉｐｌｅｓｏｆＰｒｏｇｒａｍｍｉｎｇ Ｌａｎｇｕａｇｅｓ．Ｓａｎ Ｄｉｅｇｏ，１９９８：８５９７ ［２］ Ｍａｎｄｅｌｂａｕｍ Ｙ，ＷａｌｋｅｒＤ，ＨａｒｐｅｒＲ．Ａｎｅｆｆｅｃｔｉｖｅｔｈｅｏｒｙｏｆ ｔｙｐｅｒｅｆｉｎｅｍｅｎｔｓ／／Ｐｒｏｃｅｅｄｉｎｇｓｏｆｔｈｅ８ｔｈＩｎｔｅｒｎａｔｉｏｎａｌＣｏｎ ｆｅｒｅｎｃｅ ｏｎ Ｆｕｎｃｔｉｏｎａｌ Ｐｒｏｇｒａｍｍｉｎｇ． Ｕｐｐｓａｌａ，Ｓｗｅｄｅｎ， ２００３：２１３２２５ ［３］ Ｎｅｃｕｌａ Ｇ．Ｐｒｏｏｆｃａｒｒｙｉｎｇ ｃｏｄｅ／／Ｐｒｏｃｅｅｄｉｎｇｓ ｏｆｔｈｅ ２４ｔｈ ＡＣＭＳｙｍｐｏｓｉｕｍ ＯｎＰｒｉｎｃｉｐｌｅｓｏｆＰｒｏｇｒａｍｍｉｎｇＬａｎｇｕａｇｅｓ． ＮｅｗＹｏｒｋ，１９９７：１０６１１９ ［４］ ＡｐｐｅｌＡ Ｗ．Ｆｏｕｎｄａｔｉｏｎａｌｐｒｏｏｆｃａｒｒｙｉｎｇｃｏｄｅ／／Ｐｒｏｃｅｅｄｉｎｇｓ ｏｆｔｈｅ１６ｔｈＡｎｎｕａｌＩＥＥＥＳｙｍｐｏｓｉｕｍｏｎＬｏｇｉｃｉｎＣｏｍｐｕｔｅｒ Ｓｃｉｅｎｃｅ．Ｂａｓｔｏｎ，Ｍａｓｓａｃｈｕｓｅｔｔｓ，ＵＳＡ，２００１：２４７２５８ ［５］ ＹｕＤ，ＨａｍｉｄＮ Ａ，ＳｈａｏＺ．Ｂｕｉｌｄｉｎｇｃｅｒｔｉｆｉｅｄｌｉｂｒａｒｉｅｓｆｏｒ ＰＣＣ：Ｄｙｎａｍｉｃｓｔｏｒａｇｅａｌｌｏｃａｔｉｏｎ．ＳｃｉｅｎｃｅｏｆＣｏｍｐｕｔｅｒＰｒｏ ｇｒａｍｍｉｎｇ，２００４，５０（１３）：１０１１２７ ［６］ ＦｅｎｇＸ，ＳｈａｏＺ，ＶａｙｎｂｅｒｇＡ，ＸｉａｎｇＳ，ＮｉＺ．ＭｏｄｕｌａｒＶｅｒ ｉｆｉｃａｔｉｏｎｏｆ Ａｓｓｅｍｂｌｙ Ｃｏｄｅ ｗｉｔｈ ＳｔａｃｋＢａｓｅｄ Ｃｏｎｔｒｏｌ Ａｂ ｓｔｒａｃｔｉｏｎｓ／／Ｐｒｏｃｅｅｄｉｎｇｓｏｆｔｈｅ２００６ＡＣＭＳＩＧＰＬＡＮＣｏｎｆｅｒ ｅｎｃｅｏｎＰｒｏｇｒａｍｍｉｎｇＬａｎｇｕａｇｅＤｅｓｉｇｎａｎｄＩｍｐｌｅｍｅｎｔａｔｉｏｎ． Ｏｔｔａｗａ，Ｃａｎａｄａ，２００６：４０１４１４ ［７］ ＸｉＨ．Ａｐｐｌｉｅｄｔｙｐｅｓｙｓｔｅｍ：Ｅｘｔｅｎｄｅｄａｂｓｔｒａｃｔ／／Ｐｒｏｃｅｅｄｉｎｇｓ ｏｆＴＹＰＥＳ２００３．ＬＮＣＳ３０８５．ＳｐｒｉｎｇｅｒＶｅｒｌａｇ，２００４：３９４ ４０８ ［８］ ＳｔｅｅｎｓｇａａｒｄＢ．Ｐｏｉｎｔｓｔｏａｎａｌｙｓｉｓｉｎａｌｍｏｓｔｌｉｎｅａｒｔｉｍｅ／／Ｐｒｏ ｃｅｅｄｉｎｇｓｏｆｔｈｅ２３ｔｈＡｎｎｕａｌＡＣＭ ＳｙｍｐｏｓｉｕｍｏｎＰｒｉｎｃｉｐｌｅｓ ｏｆＰｒｏｇｒａｍｍｉｎｇＬａｎｇｕａｇｅｓ．Ｆｌｏｒｉｄａ，ＵＳＡ，１９９６：３２４１ ［９］ ＢｅｒｎｄｌＭ，Ｌｈｏｔｋ Ｏ，Ｑｉａｎ Ｆ，Ｈｅｎｄｒｅｎ Ｌ，Ｕｍａｎｅｅ Ｎ． Ｐｏｉｎｔｓｔｏａｎａｌｙｓｉｓ ｕｓｉｎｇ ＢＤＤｓ／／Ｐｒｏｃｅｅｄｉｎｇｓ ｏｆｔｈｅ ＡＣＭ ＳＩＧＰＬＡＮ２００３ＣｏｎｆｅｒｅｎｃｅｏｎＰｒｏｇｒａｍｍｉｎｇＬａｎｇｕａｇｅＤｅ ｓｉｇｎａｎｄＩｍｐｌｅｍｅｎｔａｔｉｏｎ．ＳａｎＤｉｅｇｏ，２００３：１０３１１４ ３ 期 陈意云等：一种用于指针程序安全性证明的指针逻辑 ３７９
380 计 算 机 学 报 2008年 [10]Hind M.Pointer analysis:Haven't we solved this problem ACM Symposium on Principles of Programming Languages. yet?//Proceedings of the ACM Workshop on Program Long Beach.California,USA.2005:259-270 Analysis for Software.Tools and Engineering.Snowbird. [14]Bornat R.Proving pointer programs in Hoare logic//Pro- Utab,USA,2001:54-61 ceedings of the 5th International Conference on Mathematics [11]Reynolds J C.Separation logic:A logic for shared mutable of Program Construction.Pontede Lima,Portugal.2000: data structures//Proceedings of the 17th Annual IEEE Sym- 102-126 posium on Logic in Computer Science.Washington.DC. [15]Mehta F.Nipkow T.Proving pointer programs in higher- USA,2002:55-74 order logic.Information and Computation.2005.199(1-2): [12]Parkinson M.Bierman G.Separation logic and abstraction// 200-227 Proceedings of the 32nd ACM Symposium on Principles of [16]Bertot Y,Casteran P.Interactive Theorem Proving and Pro- Programming Languages.Long Beach,California,USA. gram Development:Coq'Art:The Calculus of Inductive Con- 2005：247-258 struction.Texts in Theoretical Computer Science,an [13]Bornat R.Calcagno C.O'Hearn P.Parkinson W.Permis- EATCS series.Berlin:Springer Verlag,2004 sion accounting in separation logic//Proceedings of the 32nd CHEN Yi-Yun,born in 1946,pro- HUA Bao-Jian.born in 1979.Ph.D.candidate.His re- fessor.Ph.D.supervisor.His research search interests include program verification.program logic. interests include theory and implementa- and software safety and security. tion of programming languages,formal GE Lin,born in 1979,Ph.D.candidate.Her research description technologies,and software interests include program verification.software safety and safety and security. security.and type theory and system. WANG Zhi-Fang,born in 1982,Ph.D.candidate.His research interests include software safety and security,pro- gram logic.and program verification. Background This research is supported by the National Natural Sci- first challenge.A pointer logic is designed for PointerC lan- ence Foundation of China Verification and Compilation of guage,a subset with explicit memory allocation and dealloca- Software Safety,grant No.60673126). tion of C-like programming languages,in the authors're- Proof-Carrying Code (PCC)brings two grand challenges search.As an extension of Hoare logic.the pointer logic is to the research field of programming languages.One is to used to prove properties of pointer programs.The main char- seek more expressive logic or type systems to specify or rea- acteristic of the pointer logic is that its inference rules are son about the properties of high-level or low-level programs. used to catch the modification of pointer information caused The other is to study the technology of certifying compilation by the execution of each statement.Based on these rules,we in which the compiler generates proofs for programs with an- can reason out the null pointers.dangling pointers and equal- notations.For the first challenge.Typed Assembly Lan-ity of effective pointers at each point in a program,and then guage and the theory of type refinements are two typical re- calculate alias set of each pointer.These are the base infor- search projects in type-based approaches,while PCC.Foun- mation to prove safety and other properties of pointer pro- dational Proof-Carrying Code and Certified Assembly Pro- grams. gramming are typical research projects on logic-based tech- The main contribution of this paper is the elementary de- niques.Type-based and logic-based techniques are comple- sign of the pointer logic.In the project.the authors'have mentary to each other,some researchers have tried to com- implemented a certifying compiler based on the pointer logic bine those techniques. and proved safety of PointerC language and soundness of the This paper presents the authors'research progress in the pointer logic
［１０］ ＨｉｎｄＭ．Ｐｏｉｎｔｅｒａｎａｌｙｓｉｓ：Ｈａｖｅｎ′ｔｗｅｓｏｌｖｅｄｔｈｉｓｐｒｏｂｌｅｍ ｙｅｔ？／／Ｐｒｏｃｅｅｄｉｎｇｓ ｏｆｔｈｅ ＡＣＭ Ｗｏｒｋｓｈｏｐ ｏｎ Ｐｒｏｇｒａｍ ＡｎａｌｙｓｉｓｆｏｒＳｏｆｔｗａｒｅ．Ｔｏｏｌｓａｎｄ Ｅｎｇｉｎｅｅｒｉｎｇ．Ｓｎｏｗｂｉｒｄ， Ｕｔａｂ，ＵＳＡ，２００１：５４６１ ［１１］ ＲｅｙｎｏｌｄｓＪＣ．Ｓｅｐａｒａｔｉｏｎｌｏｇｉｃ：Ａｌｏｇｉｃｆｏｒｓｈａｒｅｄ ｍｕｔａｂｌｅ ｄａｔａｓｔｒｕｃｔｕｒｅｓ／／Ｐｒｏｃｅｅｄｉｎｇｓｏｆｔｈｅ１７ｔｈＡｎｎｕａｌＩＥＥＥＳｙｍ ｐｏｓｉｕｍ ｏｎ Ｌｏｇｉｃｉｎ ＣｏｍｐｕｔｅｒＳｃｉｅｎｃｅ． Ｗａｓｈｉｎｇｔｏｎ，ＤＣ， ＵＳＡ，２００２：５５７４ ［１２］ ＰａｒｋｉｎｓｏｎＭ，ＢｉｅｒｍａｎＧ．Ｓｅｐａｒａｔｉｏｎｌｏｇｉｃａｎｄａｂｓｔｒａｃｔｉｏｎ／／ Ｐｒｏｃｅｅｄｉｎｇｓｏｆｔｈｅ３２ｎｄ ＡＣＭ Ｓｙｍｐｏｓｉｕｍ ｏｎＰｒｉｎｃｉｐｌｅｓｏｆ Ｐｒｏｇｒａｍｍｉｎｇ Ｌａｎｇｕａｇｅｓ．Ｌｏｎｇ Ｂｅａｃｈ，Ｃａｌｉｆｏｒｎｉａ，ＵＳＡ， ２００５：２４７２５８ ［１３］ ＢｏｒｎａｔＲ，ＣａｌｃａｇｎｏＣ，Ｏ′ＨｅａｒｎＰ，Ｐａｒｋｉｎｓｏｎ Ｗ．Ｐｅｒｍｉｓ ｓｉｏｎａｃｃｏｕｎｔｉｎｇｉｎｓｅｐａｒａｔｉｏｎｌｏｇｉｃ／／Ｐｒｏｃｅｅｄｉｎｇｓｏｆｔｈｅ３２ｎｄ ＡＣＭ ＳｙｍｐｏｓｉｕｍｏｎＰｒｉｎｃｉｐｌｅｓｏｆＰｒｏｇｒａｍｍｉｎｇＬａｎｇｕａｇｅｓ． ＬｏｎｇＢｅａｃｈ，Ｃａｌｉｆｏｒｎｉａ，ＵＳＡ，２００５：２５９２７０ ［１４］ ＢｏｒｎａｔＲ．Ｐｒｏｖｉｎｇｐｏｉｎｔｅｒｐｒｏｇｒａｍｓｉｎ Ｈｏａｒｅｌｏｇｉｃ／／Ｐｒｏ ｃｅｅｄｉｎｇｓｏｆｔｈｅ５ｔｈＩｎｔｅｒｎａｔｉｏｎａｌＣｏｎｆｅｒｅｎｃｅｏｎ Ｍａｔｈｅｍａｔｉｃｓ ｏｆＰｒｏｇｒａｍ Ｃｏｎｓｔｒｕｃｔｉｏｎ，ＰｏｎｔｅｄｅＬｉｍａ，Ｐｏｒｔｕｇａｌ，２０００： １０２１２６ ［１５］ ＭｅｈｔａＦ，Ｎｉｐｋｏｗ Ｔ．Ｐｒｏｖｉｎｇｐｏｉｎｔｅｒｐｒｏｇｒａｍｓｉｎｈｉｇｈｅｒ ｏｒｄｅｒｌｏｇｉｃ．ＩｎｆｏｒｍａｔｉｏｎａｎｄＣｏｍｐｕｔａｔｉｏｎ，２００５，１９９（１２）： ２００２２７ ［１６］ ＢｅｒｔｏｔＹ，ＣａｓｔéｒａｎＰ．ＩｎｔｅｒａｃｔｉｖｅＴｈｅｏｒｅｍＰｒｏｖｉｎｇａｎｄＰｒｏ ｇｒａｍＤｅｖｅｌｏｐｍｅｎｔ：Ｃｏｑ′Ａｒｔ：ＴｈｅＣａｌｃｕｌｕｓｏｆＩｎｄｕｃｔｉｖｅＣｏｎ ｓｔｒｕｃｔｉｏｎ． Ｔｅｘｔｓ ｉｎ Ｔｈｅｏｒｅｔｉｃａｌ Ｃｏｍｐｕｔｅｒ Ｓｃｉｅｎｃｅ， ａｎ ＥＡＴＣＳｓｅｒｉｅｓ．Ｂｅｒｌｉｎ：ＳｐｒｉｎｇｅｒＶｅｒｌａｇ，２００４ 犆犎犈犖犢犻犢狌狀，ｂｏｒｎｉｎ１９４６，ｐｒｏ ｆｅｓｓｏｒ，Ｐｈ．Ｄ．ｓｕｐｅｒｖｉｓｏｒ．Ｈｉｓｒｅｓｅａｒｃｈ ｉｎｔｅｒｅｓｔｓｉｎｃｌｕｄｅｔｈｅｏｒｙａｎｄｉｍｐｌｅｍｅｎｔａ ｔｉｏｎｏｆｐｒｏｇｒａｍｍｉｎｇｌａｎｇｕａｇｅｓ，ｆｏｒｍａｌ ｄｅｓｃｒｉｐｔｉｏｎｔｅｃｈｎｏｌｏｇｉｅｓ，ａｎｄ ｓｏｆｔｗａｒｅ ｓａｆｅｔｙａｎｄｓｅｃｕｒｉｔｙ． 犎犝犃犅犪狅犑犻犪狀，ｂｏｒｎｉｎ１９７９，Ｐｈ．Ｄ．ｃａｎｄｉｄａｔｅ．Ｈｉｓｒｅ ｓｅａｒｃｈｉｎｔｅｒｅｓｔｓｉｎｃｌｕｄｅｐｒｏｇｒａｍｖｅｒｉｆｉｃａｔｉｏｎ，ｐｒｏｇｒａｍｌｏｇｉｃ， ａｎｄｓｏｆｔｗａｒｅｓａｆｅｔｙａｎｄｓｅｃｕｒｉｔｙ． 犌犈犔犻狀，ｂｏｒｎｉｎ１９７９，Ｐｈ．Ｄ．ｃａｎｄｉｄａｔｅ．Ｈｅｒｒｅｓｅａｒｃｈ ｉｎｔｅｒｅｓｔｓｉｎｃｌｕｄｅｐｒｏｇｒａｍ ｖｅｒｉｆｉｃａｔｉｏｎ，ｓｏｆｔｗａｒｅｓａｆｅｔｙａｎｄ ｓｅｃｕｒｉｔｙ，ａｎｄｔｙｐｅｔｈｅｏｒｙａｎｄｓｙｓｔｅｍ． 犠犃犖犌犣犺犻犉犪狀犵，ｂｏｒｎｉｎ１９８２，Ｐｈ．Ｄ．ｃａｎｄｉｄａｔｅ．Ｈｉｓ ｒｅｓｅａｒｃｈｉｎｔｅｒｅｓｔｓｉｎｃｌｕｄｅｓｏｆｔｗａｒｅｓａｆｅｔｙａｎｄｓｅｃｕｒｉｔｙ，ｐｒｏ ｇｒａｍｌｏｇｉｃ，ａｎｄｐｒｏｇｒａｍｖｅｒｉｆｉｃａｔｉｏｎ． 犅犪犮犽犵狉狅狌狀犱 ＴｈｉｓｒｅｓｅａｒｃｈｉｓｓｕｐｐｏｒｔｅｄｂｙｔｈｅＮａｔｉｏｎａｌＮａｔｕｒａｌＳｃｉ ｅｎｃｅＦｏｕｎｄａｔｉｏｎｏｆＣｈｉｎａ（Ｖｅｒｉｆｉｃａｔｉｏｎａｎｄ Ｃｏｍｐｉｌａｔｉｏｎｏｆ ＳｏｆｔｗａｒｅＳａｆｅｔｙ，ｇｒａｎｔＮｏ．６０６７３１２６）． ＰｒｏｏｆＣａｒｒｙｉｎｇＣｏｄｅ（ＰＣＣ）ｂｒｉｎｇｓｔｗｏｇｒａｎｄｃｈａｌｌｅｎｇｅｓ ｔｏｔｈｅｒｅｓｅａｒｃｈｆｉｅｌｄｏｆｐｒｏｇｒａｍｍｉｎｇｌａｎｇｕａｇｅｓ．Ｏｎｅｉｓｔｏ ｓｅｅｋｍｏｒｅｅｘｐｒｅｓｓｉｖｅｌｏｇｉｃｏｒｔｙｐｅｓｙｓｔｅｍｓｔｏｓｐｅｃｉｆｙｏｒｒｅａ ｓｏｎａｂｏｕｔｔｈｅｐｒｏｐｅｒｔｉｅｓｏｆｈｉｇｈｌｅｖｅｌｏｒｌｏｗｌｅｖｅｌｐｒｏｇｒａｍｓ． Ｔｈｅｏｔｈｅｒｉｓｔｏｓｔｕｄｙｔｈｅｔｅｃｈｎｏｌｏｇｙｏｆｃｅｒｔｉｆｙｉｎｇｃｏｍｐｉｌａｔｉｏｎ ｉｎｗｈｉｃｈｔｈｅｃｏｍｐｉｌｅｒｇｅｎｅｒａｔｅｓｐｒｏｏｆｓｆｏｒｐｒｏｇｒａｍｓｗｉｔｈａｎ ｎｏｔａｔｉｏｎｓ．Ｆｏｒｔｈｅｆｉｒｓｔｃｈａｌｌｅｎｇｅ，Ｔｙｐｅｄ Ａｓｓｅｍｂｌｙ Ｌａｎ ｇｕａｇｅａｎｄｔｈｅｔｈｅｏｒｙｏｆｔｙｐｅｒｅｆｉｎｅｍｅｎｔｓａｒｅｔｗｏｔｙｐｉｃａｌｒｅ ｓｅａｒｃｈｐｒｏｊｅｃｔｓｉｎｔｙｐｅｂａｓｅｄａｐｐｒｏａｃｈｅｓ，ｗｈｉｌｅＰＣＣ，Ｆｏｕｎ ｄａｔｉｏｎａｌＰｒｏｏｆＣａｒｒｙｉｎｇ Ｃｏｄｅａｎｄ Ｃｅｒｔｉｆｉｅｄ Ａｓｓｅｍｂｌｙ Ｐｒｏ ｇｒａｍｍｉｎｇａｒｅｔｙｐｉｃａｌｒｅｓｅａｒｃｈｐｒｏｊｅｃｔｓｏｎｌｏｇｉｃｂａｓｅｄｔｅｃｈ ｎｉｑｕｅｓ．Ｔｙｐｅｂａｓｅｄａｎｄｌｏｇｉｃｂａｓｅｄｔｅｃｈｎｉｑｕｅｓａｒｅｃｏｍｐｌｅ ｍｅｎｔａｒｙｔｏｅａｃｈｏｔｈｅｒ，ｓｏｍｅｒｅｓｅａｒｃｈｅｒｓｈａｖｅｔｒｉｅｄｔｏｃｏｍ ｂｉｎｅｔｈｏｓｅｔｅｃｈｎｉｑｕｅｓ． Ｔｈｉｓｐａｐｅｒｐｒｅｓｅｎｔｓｔｈｅａｕｔｈｏｒｓ′ｒｅｓｅａｒｃｈｐｒｏｇｒｅｓｓｉｎｔｈｅ ｆｉｒｓｔｃｈａｌｌｅｎｇｅ．ＡｐｏｉｎｔｅｒｌｏｇｉｃｉｓｄｅｓｉｇｎｅｄｆｏｒＰｏｉｎｔｅｒＣｌａｎ ｇｕａｇｅ，ａｓｕｂｓｅｔｗｉｔｈｅｘｐｌｉｃｉｔｍｅｍｏｒｙａｌｌｏｃａｔｉｏｎａｎｄｄｅａｌｌｏｃａ ｔｉｏｎｏｆＣｌｉｋｅｐｒｏｇｒａｍｍｉｎｇｌａｎｇｕａｇｅｓ，ｉｎｔｈｅａｕｔｈｏｒｓ′ｒｅ ｓｅａｒｃｈ．ＡｓａｎｅｘｔｅｎｓｉｏｎｏｆＨｏａｒｅｌｏｇｉｃ，ｔｈｅｐｏｉｎｔｅｒｌｏｇｉｃｉｓ ｕｓｅｄｔｏｐｒｏｖｅｐｒｏｐｅｒｔｉｅｓｏｆｐｏｉｎｔｅｒｐｒｏｇｒａｍｓ．Ｔｈｅｍａｉｎｃｈａｒ ａｃｔｅｒｉｓｔｉｃｏｆｔｈｅｐｏｉｎｔｅｒｌｏｇｉｃｉｓｔｈａｔｉｔｓｉｎｆｅｒｅｎｃｅｒｕｌｅｓａｒｅ ｕｓｅｄｔｏｃａｔｃｈｔｈｅｍｏｄｉｆｉｃａｔｉｏｎｏｆｐｏｉｎｔｅｒｉｎｆｏｒｍａｔｉｏｎｃａｕｓｅｄ ｂｙｔｈｅｅｘｅｃｕｔｉｏｎｏｆｅａｃｈｓｔａｔｅｍｅｎｔ．Ｂａｓｅｄｏｎｔｈｅｓｅｒｕｌｅｓ，ｗｅ ｃａｎｒｅａｓｏｎｏｕｔｔｈｅｎｕｌｌｐｏｉｎｔｅｒｓ，ｄａｎｇｌｉｎｇｐｏｉｎｔｅｒｓａｎｄｅｑｕａｌ ｉｔｙｏｆｅｆｆｅｃｔｉｖｅｐｏｉｎｔｅｒｓａｔｅａｃｈｐｏｉｎｔｉｎａｐｒｏｇｒａｍ，ａｎｄｔｈｅｎ ｃａｌｃｕｌａｔｅａｌｉａｓｓｅｔｏｆｅａｃｈｐｏｉｎｔｅｒ．Ｔｈｅｓｅａｒｅｔｈｅｂａｓｅｉｎｆｏｒ ｍａｔｉｏｎｔｏｐｒｏｖｅｓａｆｅｔｙａｎｄｏｔｈｅｒｐｒｏｐｅｒｔｉｅｓｏｆｐｏｉｎｔｅｒｐｒｏ ｇｒａｍｓ． Ｔｈｅｍａｉｎｃｏｎｔｒｉｂｕｔｉｏｎｏｆｔｈｉｓｐａｐｅｒｉｓｔｈｅｅｌｅｍｅｎｔａｒｙｄｅ ｓｉｇｎｏｆｔｈｅｐｏｉｎｔｅｒｌｏｇｉｃ．Ｉｎｔｈｅｐｒｏｊｅｃｔ，ｔｈｅａｕｔｈｏｒｓ′ｈａｖｅ ｉｍｐｌｅｍｅｎｔｅｄａｃｅｒｔｉｆｙｉｎｇｃｏｍｐｉｌｅｒｂａｓｅｄｏｎｔｈｅｐｏｉｎｔｅｒｌｏｇｉｃ ａｎｄｐｒｏｖｅｄｓａｆｅｔｙｏｆＰｏｉｎｔｅｒＣｌａｎｇｕａｇｅａｎｄｓｏｕｎｄｎｅｓｓｏｆｔｈｅ ｐｏｉｎｔｅｒｌｏｇｉｃ． ３８０ 计 算 机 学 报 ２００８年