第31卷第4期 计算机学报 Vol. 31 No. 4 2008年4月 CHINESE JOURNAL OF COMPUTERS Apr. 2008 安全语言PointerC的设计及形式证明 华保健陈意云李兆鹏王志芳葛琳 (中国科学技术大学计算机科学技术系合肥230026) (中国科学技术大学苏州研究院软件安全实验室江苏苏州215123) 摘要程序设计语言本身的安全性在高安全需求软件的设计和实现中起着基础作用。该文在用于系统级编程的 安全语言的设计和性质证明方面，做了有益的尝试.作者设计了一个类C的命令式语言PointerC,其主要特点在于 其类型系统中包含显式的副条件(sideconditions),这些副条件本质上是约束程序语法表达式值的逻辑公式.该文 证明了PointerC语言的安全性定理，即满足这些副条件的程序，在执行时不会违反语言的安全策略.为静态推理副 条件中涉及指针的命题，作者已经提出了一种指针逻辑(pointerlogic),文中证明了指针逻辑对操作语义是可靠的. 关键词软件安全；语言设计；类型系统；Hoare逻辑；指针逻辑 中图法分类号TP301 Design and Proof of a Safe Programming Language PointerC HUA Bao-Jian CHEN Yi-Yun LI Zhao-Peng WANG Zhi-Fang GE Lin (Department of Computer Science and Technology.Uwiversity of Science and Technology of Chinea,Hefei 230026) (Softuare Security Laboratory,Suxhou Institute for Advanced Study. University of Science and Technology of China,Suzhou.Jiangsu 215123) Abstract The safety property of programming languages plays a fundamental role in the design and implementation of safety-critical software systems. And the authors have made investigation towards the design and proof of safe languages suitable for system programming. This paper presents the design of a C-like imperative programming language PointerC. One novelty of Point- erC is that typing rules in its type system are accompanied by logic propositions which are called side conditions. And this paper proves PointerC is safe—The executions of programs will not vio- late the safety policy of the language, if these side conditions hold. A pointer logic, as an exten- sion of Hoare logic, has been designed for the purpose of proving pointer-related side conditions statically. This paper presents the soundness proof for the pointer logic. Keywords software safety; language design; type systems; Hoare logic; pointer logic 计算机病毒应急处理中心(CNCERT/CC)最近的一 1引言 份统计报告显示，仅在2006年，我国就有超过 74%的计算机受到计算机病毒的感染和破坏，直接 现代社会的正常运转越来越多依赖计算机软件 经济损失数亿元；并且，近四年国内报告的安全事件 系统，软件系统所引发的安全问题也日益突出.国家 数量（不包括扫描攻击），年平均增长超过200%，去 收稿日期：2007-11-26.本课题得到国家自然科学基金(60673126)、Intel中国研究中心资助.华保健，男，1979年生，博士研究生，主要研 究方向为程序验证，软件安全.E-mail:huabj@mail.ustc.edu.cn.陈意云，男，1946年生，教授，博士生导师，主要研究领域为程序设计语 言理论和实现技术、程序验证、软件安全.李兆鹏，男，1978年生，博士研究生，主要研究方向为程序验证、软件安全、类型系统和理论. 王志芳，男，1982年生，博士研究生，主要研究方向为指针程序的安全性证明.葛琳，女，1979年生，博士研究生，主要研究方向为程序验 证、软件安全、类型系统和理论
书 第３１卷 第４期 ２００８年４月 计 算 机 学 报 ＣＨＩＮＥＳＥＪＯＵＲＮＡＬＯＦＣＯＭＰＵＴＥＲＳ Ｖｏｌ．３１ Ｎｏ．４ Ａｐｒ．２００８ 收稿日期：２００７１１２６．本课题得到国家自然科学基金（６０６７３１２６）、Ｉｎｔｅｌ中国研究中心资助．华保健，男，１９７９年生，博士研究生，主要研 究方向为程序验证、软件安全．Ｅｍａｉｌ：ｈｕａｂｊ＠ｍａｉｌ．ｕｓｔｃ．ｅｄｕ．ｃｎ．陈意云，男，１９４６年生，教授，博士生导师，主要研究领域为程序设计语 言理论和实现技术、程序验证、软件安全．李兆鹏，男，１９７８年生，博士研究生，主要研究方向为程序验证、软件安全、类型系统和理论． 王志芳，男，１９８２年生，博士研究生，主要研究方向为指针程序的安全性证明．葛 琳，女，１９７９年生，博士研究生，主要研究方向为程序验 证、软件安全、类型系统和理论． 安全语言犘狅犻狀狋犲狉犆的设计及形式证明 华保健 陈意云 李兆鹏 王志芳 葛 琳 （中国科学技术大学计算机科学技术系 合肥 ２３００２６） （中国科学技术大学苏州研究院软件安全实验室 江苏 苏州 ２１５１２３） 摘 要 程序设计语言本身的安全性在高安全需求软件的设计和实现中起着基础作用．该文在用于系统级编程的 安全语言的设计和性质证明方面，做了有益的尝试．作者设计了一个类 Ｃ的命令式语言 ＰｏｉｎｔｅｒＣ，其主要特点在于 其类型系统中包含显式的副条件（ｓｉｄｅｃｏｎｄｉｔｉｏｎｓ），这些副条件本质上是约束程序语法表达式值的逻辑公式．该文 证明了 ＰｏｉｎｔｅｒＣ语言的安全性定理，即满足这些副条件的程序，在执行时不会违反语言的安全策略．为静态推理副 条件中涉及指针的命题，作者已经提出了一种指针逻辑（ｐｏｉｎｔｅｒｌｏｇｉｃ），文中证明了指针逻辑对操作语义是可靠的． 关键词 软件安全；语言设计；类型系统；Ｈｏａｒｅ逻辑；指针逻辑 中图法分类号 ＴＰ３０１ 犇犲狊犻犵狀犪狀犱犘狉狅狅犳狅犳犪犛犪犳犲犘狉狅犵狉犪犿犿犻狀犵犔犪狀犵狌犪犵犲犘狅犻狀狋犲狉犆 ＨＵＡＢａｏＪｉａｎ ＣＨＥＮ ＹｉＹｕｎ ＬＩＺｈａｏＰｅｎｇ ＷＡＮＧＺｈｉＦａｎｇ ＧＥＬｉｎ （犇犲狆犪狉狋犿犲狀狋狅犳犆狅犿狆狌狋犲狉犛犮犻犲狀犮犲犪狀犱犜犲犮犺狀狅犾狅犵狔，犝狀犻狏犲狉狊犻狋狔狅犳犛犮犻犲狀犮犲犪狀犱犜犲犮犺狀狅犾狅犵狔狅犳犆犺犻狀犪，犎犲犳犲犻 ２３００２６） （犛狅犳狋狑犪狉犲犛犲犮狌狉犻狋狔犔犪犫狅狉犪狋狅狉狔，犛狌狕犺狅狌犐狀狊狋犻狋狌狋犲犳狅狉犃犱狏犪狀犮犲犱犛狋狌犱狔， 犝狀犻狏犲狉狊犻狋狔狅犳犛犮犻犲狀犮犲犪狀犱犜犲犮犺狀狅犾狅犵狔狅犳犆犺犻狀犪，犛狌狕犺狅狌，犑犻犪狀犵狊狌 ２１５１２３） 犃犫狊狋狉犪犮狋 Ｔｈｅｓａｆｅｔｙｐｒｏｐｅｒｔｙｏｆｐｒｏｇｒａｍｍｉｎｇｌａｎｇｕａｇｅｓｐｌａｙｓａｆｕｎｄａｍｅｎｔａｌｒｏｌｅｉｎｔｈｅｄｅｓｉｇｎ ａｎｄｉｍｐｌｅｍｅｎｔａｔｉｏｎｏｆｓａｆｅｔｙｃｒｉｔｉｃａｌｓｏｆｔｗａｒｅｓｙｓｔｅｍｓ．Ａｎｄｔｈｅａｕｔｈｏｒｓｈａｖｅｍａｄｅｉｎｖｅｓｔｉｇａｔｉｏｎ ｔｏｗａｒｄｓｔｈｅｄｅｓｉｇｎａｎｄｐｒｏｏｆｏｆｓａｆｅｌａｎｇｕａｇｅｓｓｕｉｔａｂｌｅｆｏｒｓｙｓｔｅｍ ｐｒｏｇｒａｍｍｉｎｇ．Ｔｈｉｓｐａｐｅｒ ｐｒｅｓｅｎｔｓｔｈｅｄｅｓｉｇｎｏｆａＣｌｉｋｅｉｍｐｅｒａｔｉｖｅｐｒｏｇｒａｍｍｉｎｇｌａｎｇｕａｇｅＰｏｉｎｔｅｒＣ．ＯｎｅｎｏｖｅｌｔｙｏｆＰｏｉｎｔ ｅｒＣｉｓｔｈａｔｔｙｐｉｎｇｒｕｌｅｓｉｎｉｔｓｔｙｐｅｓｙｓｔｅｍａｒｅａｃｃｏｍｐａｎｉｅｄｂｙｌｏｇｉｃｐｒｏｐｏｓｉｔｉｏｎｓｗｈｉｃｈａｒｅｃａｌｌｅｄ ｓｉｄｅｃｏｎｄｉｔｉｏｎｓ．ＡｎｄｔｈｉｓｐａｐｅｒｐｒｏｖｅｓＰｏｉｎｔｅｒＣｉｓｓａｆｅ—Ｔｈｅｅｘｅｃｕｔｉｏｎｓｏｆｐｒｏｇｒａｍｓｗｉｌｌｎｏｔｖｉｏ ｌａｔｅｔｈｅｓａｆｅｔｙｐｏｌｉｃｙｏｆｔｈｅｌａｎｇｕａｇｅ，ｉｆｔｈｅｓｅｓｉｄｅｃｏｎｄｉｔｉｏｎｓｈｏｌｄ．Ａｐｏｉｎｔｅｒｌｏｇｉｃ，ａｓａｎｅｘｔｅｎ ｓｉｏｎｏｆＨｏａｒｅｌｏｇｉｃ，ｈａｓｂｅｅｎｄｅｓｉｇｎｅｄｆｏｒｔｈｅｐｕｒｐｏｓｅｏｆｐｒｏｖｉｎｇｐｏｉｎｔｅｒｒｅｌａｔｅｄｓｉｄｅｃｏｎｄｉｔｉｏｎｓ ｓｔａｔｉｃａｌｌｙ．Ｔｈｉｓｐａｐｅｒｐｒｅｓｅｎｔｓｔｈｅｓｏｕｎｄｎｅｓｓｐｒｏｏｆｆｏｒｔｈｅｐｏｉｎｔｅｒｌｏｇｉｃ． 犓犲狔狑狅狉犱狊 ｓｏｆｔｗａｒｅｓａｆｅｔｙ；ｌａｎｇｕａｇｅｄｅｓｉｇｎ；ｔｙｐｅｓｙｓｔｅｍｓ；Ｈｏａｒｅｌｏｇｉｃ；ｐｏｉｎｔｅｒｌｏｇｉｃ １ 引 言 现代社会的正常运转越来越多依赖计算机软件 系统，软件系统所引发的安全问题也日益突出．国家 计算机病毒应急处理中心（ＣＮＣＥＲＴ／ＣＣ）最近的一 份统计 报 告［１］显 示，仅 在 ２００６ 年，我 国 就 有 超 过 ７４％的计算机受到计算机病毒的感染和破坏，直接 经济损失数亿元；并且，近四年国内报告的安全事件 数量（不包括扫描攻击），年平均增长超过２００％，去
4期 华保健等：安全语言PointerC的设计及形式证明 557 年已超过26000件. 合保证语言安全性的静态机制，为此，我们设计了一 安全问题如此严峻，最基本的原因是计算机系 个保留C指针特性的类C语言PointerC.和C语言 统存在可被渗透(exploit)的脆弱性(vulnerability) 的类型系统相比，PointerC的新颖之处在于它的定 或者称为安全漏洞(security hole).由于操作系统内 型规则(typing rules)中除了包括普通的定型断言 核等系统软件的实现语言是C或C+十等不安全的 外，还包括作为副条件的逻辑命题，这些副条件给出 编程语言，因此，编程语言本身的不安全特性，导致 了对程序语法表达式值的约束.我们形式定义了语 这些系统软件很容易出现安全漏洞.很多入侵者就 言所要满足的安全策略，并且，基于这些安全策略， 是利用这些语言的下标越界、栈溢出、字符串攻击等 证明了PointerC语言是安全的. 不安全特性，对系统进行攻击或实现非授权控制. 为了静态检查这些副条件，我们在前期工作中 在为应对软件安全挑战而进行的研究工作中， 已经为PointerC语言设计了一种指针逻辑ao-),它 基于程序设计语言的软件安全(language--base soft- 是Hoare逻辑的一种拓展，本质上是一种精确的指 ware security)研究引人注目，其中典型的工作包括 针分析工具.指针逻辑可用来从前向后收集各指针是 程序分析、类型安全的语言、高级类型系统、程序验 空指针、悬空指针还是有效指针(effective pointer, 证研究等. 有指向对象的指针)的信息，收集各有效指针之间相 基于程序分析理论和方法，很多代码查错工具 等与否的信息，所收集信息用来证明指针程序是否 被开发出来，如LC-Lint、PREFix和Purify等，它 满足定型规则的附加条件，以支持对指针程序的安 们可以用于查找和定位程序中的安全漏洞.但这类 全性验证和其它性质的验证.我们证明了指针逻辑 工具查错的不完备性导致其分析结果不是精确的， 对PointerC语言的操作语义是可靠性的. 因此，难以单独依赖这些工具构造无安全漏洞的软 和已有研究工作相比，本文工作的主要特色和 件系统。 贡献在于： 类型安全的语言，如ML、Java或C共等，提供 (1)探索了一种类型系统和逻辑系统相结合保 类型安全保证；并且依赖自动垃圾收集技术，他们保 证语言安全性的静态机制，从程序设计角度看，和依 证存储安全(memory safety).虽然用这些语言实现 赖类型等方式相比，使用副条件更有利于程序员的 系统软件的尝试仍在继续)，但和C、C++相比，这 理解. 些语言运行效率的低下使得这些尝试目前仍面临难 (2)本文证明了PointerC语言是安全的，该证 以克服的困难.细化的类型系统[]着眼于为语言设 明基于一组形式定义的安全策略.基于安全策略进 计更高级的类型，以表达更精细的安全属性，近年 行证明可以保证语言的安全属性，例如，我们证明了 来典型的研究包括依赖类型(dependent type)-)、 合法的PointerC程序不会出现内存泄露(memory 应用类型(applied type)、单元素类型(singleton leak). type)[]等.尽管这些系统扩展了传统类型系统的表 (3)我们证明了指针逻辑对PointerC语言的操 达能力，但它们都受到共同问题的困扰一静态类 作语义是可靠的.和Hoare逻辑的可靠性证明相 型系统有限的表达能力，因此，这些研究都仅在整数 比，指针逻辑的可靠性证明具有明显的区别 域等几个简单论域上取得了部分结果 本文第2节介绍所设计的源语言PointerC,包 程序验证和公理语义[8]通过从程序中抽取逻 括它的语法、类型系统、操作语义，在形式定义安全 辑命题来进行程序性质证明，其中程序性质包括安 策略后，本节证明PointerC语言是安全的；第3节 全属性和部分正确性(partial correctness)等.但程 概要介绍指针逻辑，重点介绍指针逻辑的可靠性证 序验证一般需要把写程序规范和写代码本身结合起 明；第4节与相关工作进行比较：最后给出结论和进 来，这增大了程序设计的难度；而且，由于不存在证 一步的工作. 明逻辑命题的通用算法，很多程序的证明无法自动 完成. 2 源语言PointerC的设计及其 针对软件安全研究面临的挑战和现有研究工作 安全性证明 的不足，我们在适用于系统级编程的安全语言设计 和实现以及性质证明方面，做了有益的尝试.本文工 本文所讨论的带有副条件的类型系统以及为证 作的主要目的是探索一种类型系统和逻辑系统相结 明这些副条件而设计逻辑系统来保证语言安全性的
年已超过２６０００件． 安全问题如此严峻，最基本的原因是计算机系 统存在可被渗透（ｅｘｐｌｏｉｔ）的脆弱性（ｖｕｌｎｅｒａｂｉｌｉｔｙ） 或者称为安全漏洞（ｓｅｃｕｒｉｔｙｈｏｌｅ）．由于操作系统内 核等系统软件的实现语言是 Ｃ或 Ｃ＋＋等不安全的 编程语言，因此，编程语言本身的不安全特性，导致 这些系统软件很容易出现安全漏洞．很多入侵者就 是利用这些语言的下标越界、栈溢出、字符串攻击等 不安全特性，对系统进行攻击或实现非授权控制． 在为应对软件安全挑战而进行的研究工作中， 基于程序设计语言的软件安全（ｌａｎｇｕａｇｅｂａｓｅｓｏｆｔ ｗａｒｅｓｅｃｕｒｉｔｙ）研究引人注目，其中典型的工作包括 程序分析、类型安全的语言、高级类型系统、程序验 证研究等． 基于程序分析理论和方法，很多代码查错工具 被开发出来，如 ＬＣＬｉｎｔ、ＰＲＥＦｉｘ和 Ｐｕｒｉｆｙ等，它 们可以用于查找和定位程序中的安全漏洞．但这类 工具查错的不完备性导致其分析结果不是精确的， 因此，难以单独依赖这些工具构造无安全漏洞的软 件系统． 类型安全的语言，如 ＭＬ、Ｊａｖａ或 Ｃ＃等，提供 类型安全保证；并且依赖自动垃圾收集技术，他们保 证存储安全（ｍｅｍｏｒｙｓａｆｅｔｙ）．虽然用这些语言实现 系统软件的尝试仍在继续［２］，但和 Ｃ、Ｃ＋＋相比，这 些语言运行效率的低下使得这些尝试目前仍面临难 以克服的困难．细化的类型系统［３］着眼于为语言设 计更高级的类型，以表达更精细的安全属性．近年 来典型的研究包括依赖类型（ｄｅｐｅｎｄｅｎｔｔｙｐｅ）［４５］、 应用类型（ａｐｐｌｉｅｄｔｙｐｅ）［６］、单元素类型 （ｓｉｎｇｌｅｔｏｎ ｔｙｐｅ）［７］等．尽管这些系统扩展了传统类型系统的表 达能力，但它们都受到共同问题的困扰———静态类 型系统有限的表达能力，因此，这些研究都仅在整数 域等几个简单论域上取得了部分结果． 程序验证和公理语义［８９］通过从程序中抽取逻 辑命题来进行程序性质证明，其中程序性质包括安 全属性和部分正确性（ｐａｒｔｉａｌｃｏｒｒｅｃｔｎｅｓｓ）等．但程 序验证一般需要把写程序规范和写代码本身结合起 来，这增大了程序设计的难度；而且，由于不存在证 明逻辑命题的通用算法，很多程序的证明无法自动 完成． 针对软件安全研究面临的挑战和现有研究工作 的不足，我们在适用于系统级编程的安全语言设计 和实现以及性质证明方面，做了有益的尝试．本文工 作的主要目的是探索一种类型系统和逻辑系统相结 合保证语言安全性的静态机制，为此，我们设计了一 个保留 Ｃ指针特性的类 Ｃ语言 ＰｏｉｎｔｅｒＣ．和 Ｃ语言 的类型系统相比，ＰｏｉｎｔｅｒＣ 的新颖之处在于它的定 型规则（ｔｙｐｉｎｇｒｕｌｅｓ）中除了包括普通的定型断言 外，还包括作为副条件的逻辑命题，这些副条件给出 了对程序语法表达式值的约束．我们形式定义了语 言所要满足的安全策略，并且，基于这些安全策略， 证明了 ＰｏｉｎｔｅｒＣ语言是安全的． 为了静态检查这些副条件，我们在前期工作中 已经为 ＰｏｉｎｔｅｒＣ语言设计了一种指针逻辑［１０１１］，它 是 Ｈｏａｒｅ逻辑的一种拓展，本质上是一种精确的指 针分析工具．指针逻辑可用来从前向后收集各指针是 空指针、悬空指针还是有效指针（ｅｆｆｅｃｔｉｖｅｐｏｉｎｔｅｒ， 有指向对象的指针）的信息，收集各有效指针之间相 等与否的信息．所收集信息用来证明指针程序是否 满足定型规则的附加条件，以支持对指针程序的安 全性验证和其它性质的验证．我们证明了指针逻辑 对 ＰｏｉｎｔｅｒＣ语言的操作语义是可靠性的． 和已有研究工作相比，本文工作的主要特色和 贡献在于： （１）探索了一种类型系统和逻辑系统相结合保 证语言安全性的静态机制．从程序设计角度看，和依 赖类型等方式相比，使用副条件更有利于程序员的 理解． （２）本文证明了 ＰｏｉｎｔｅｒＣ 语言是安全的，该证 明基于一组形式定义的安全策略．基于安全策略进 行证明可以保证语言的安全属性，例如，我们证明了 合法的 ＰｏｉｎｔｅｒＣ 程序不会出现内存泄露（ｍｅｍｏｒｙ ｌｅａｋ）． （３）我们证明了指针逻辑对 ＰｏｉｎｔｅｒＣ语言的操 作语义是 可 靠 的．和 Ｈｏａｒｅ逻 辑 的 可 靠 性 证 明 相 比，指针逻辑的可靠性证明具有明显的区别． 本文第２节介绍所设计的源语言 ＰｏｉｎｔｅｒＣ，包 括它的语法、类型系统、操作语义，在形式定义安全 策略后，本节证明 ＰｏｉｎｔｅｒＣ 语言是安全的；第３节 概要介绍指针逻辑，重点介绍指针逻辑的可靠性证 明；第４节与相关工作进行比较；最后给出结论和进 一步的工作． ２ 源语言犘狅犻狀狋犲狉犆的设计及其 安全性证明 本文所讨论的带有副条件的类型系统以及为证 明这些副条件而设计逻辑系统来保证语言安全性的 ４ 期 华保健等：安全语言 ＰｏｉｎｔｅｒＣ的设计及形式证明 ５５７
558 计算 机 学 报 2008年 静态机制，并不只限于适用某种特定的语言，但为考 合类型也被禁止.这些限制不影响PointerC的表达 察这种静态机制在系统级编程语言上的有效性，我 能力和实际程序设计的可用性，例如，借鉴C十十和 们设计了一个类C的命令式语言，其主要出发点 Java,PointerC引入了布尔类型，代替C对整型进行 是：首先，C语言不是类型安全的，在高安全需求的 类型强制来模拟布尔类型的做法.部分C类型被忽 应用中，为它提供更强的安全保障机制非常必要：其 略了，如浮点类型、字符类型等，因为它们和本文内 次，C作为最重要的系统程序设计语言之一，其代码 容关系不大 运行效率非常关键，因此尝试以类型系统和逻辑系 PointerC类型系统[)的定型规则除了包括通 统相结合的静态机制来保证语言的安全，而不是依 常的定型断言外，还包括称为副条件的逻辑命题，这 赖动态检查，可以不牺牲代码的运行效率；最后，本 些逻辑命题用于表达对值的约束(constraints).和 文工作的主要目标是研究保证指针操作安全性的静 已有的研究相比，PointerC采用的这种结合副条件 态机制一这也是程序分析和程序验证的难点，而 的方式有显著的优点：首先，类型系统简单明了，避 C灵活的指针特性为此提供了平台. 免了使用依赖类型等带来的复杂性；其次，对这些命 本节首先概要介绍我们所设计的类C源语言 题的证明可以使用指针逻辑系统（将第3节讨论）和 PointerC,包括它的语法、类型系统、操作语义；然后 自动定理证明工具 给出PointerC语言的安全性证明.篇幅所限，无法 图1列出了PointerC类型系统部分代表性定 列出的细节包括在相应技术报告[1)中. 型规则，其它规则可参考技术报告「.其中，T是定 2.1 PointerC的语法 型环境(typing context),由变量和类型的二元组列 PointerCL是我们设计的一个类C的命令式 表组成.位于横线上下的是通常的定型断言T卜e:t, 语言，它保留了C语言核心语法特征：结构体声明、 即表达式e在定型环境T下的类型为τ，为和通常 全局变量声明、函数定义、控制流语句、表达式等.因 的定型断言区别，副条件被写在一对大花括号内，并 PointerC的语法和C接近，这里不再赘述.Point- 置于定型规则右侧. erC类型系统的语法特征将在2.2节讨论， 和其它保证系统级编程语言安全性的工作3-1的 e:effective) (Deref) TH'e:t 不同，PointerC支持动态存储的手工管理，保留了C rhl:r[NTte:im{o≤e<N 高效存储管理的特征，但这对安全性的静态检查提 TH/Le]:t (ArrayField) 出了挑战.因此，除静态类型系统外，我们还使用 THlval:r· -lol=NULL::(leak(lol)) (AsnNull) 指针逻辑系统和定理证明的方法，它们将在第3节 讨论 图1 PointerC的代表性定型规则 2.2 PointerC的类型系统 图1的3条规则说明了副条件的3种典型使 类型系统是一种静态检查程序的语法方法，它 用.其中，对数组下标越界检查的规则ArrayField 一般根据程序短语的值的类别来对程序短语进行分 比较简单，只需检查相应的下标表达式e在合法的 类，排除程序中上下文有关的错误.尽管类型系统已 取值区间内；规则Deref给指针引用定型，除了要求 经成为现代程序设计语言最流行的静态机制之一， e在定型环境T下具有指针类型x'外，还规定表达 但现有语言的类型系统并不令人满意.C和C++ 式e的值必须是有效指针（即有具体的指向对象，见 的类型系统不是可靠的，其类型系统不能对程序行 第3节)，由于这个条件涉及e的值，因此它由副条 为提供安全保证；ML、Java、C#等语言的类型系统 件e∈effective给出；规则AsnNull给指针赋值语句 虽然是可靠的，但对于表达式值或程序资源有关的 定型，它说明了另外一类重要的副条件：当赋 部分，要依赖低效的运行时动态检查（尽管某些编译 NULL值给某个左值lal时，必须确保不产生内存 器能够静态移除部分检查)· 泄漏（即确保lal原来指向的内存块在赋值后不会 PointerC包括C语言大部分的类型，如整型、 访问不到)，这个副条件用逻辑命题一leak(lval)表 指针、数组、结构等.类型强制很容易导致难以排 示，显然内存分配语句也会使用到这个副条件四. 除的程序漏洞，如把整型数据用作指针等，因此 需要指出，定型规则规定了该语句需满足的定 PointerC禁止进行类型强制；同样，通常难以静态保 型条件以及副条件；但没有规定检查或证明这些副 证多次对同一联合(union)数据的读取是一致的，联 条件的方式.在已有的研究中，传统类型系统的表达
静态机制，并不只限于适用某种特定的语言，但为考 察这种静态机制在系统级编程语言上的有效性，我 们设计了一个类 Ｃ 的 命 令 式 语 言，其 主 要 出 发 点 是：首先，Ｃ语言不是类型安全的，在高安全需求的 应用中，为它提供更强的安全保障机制非常必要；其 次，Ｃ作为最重要的系统程序设计语言之一，其代码 运行效率非常关键，因此尝试以类型系统和逻辑系 统相结合的静态机制来保证语言的安全，而不是依 赖动态检查，可以不牺牲代码的运行效率；最后，本 文工作的主要目标是研究保证指针操作安全性的静 态机制———这也是程序分析和程序验证的难点，而 Ｃ灵活的指针特性为此提供了平台． 本节首先概要介绍我们所设计的类 Ｃ 源语言 ＰｏｉｎｔｅｒＣ，包括它的语法、类型系统、操作语义；然后 给出 ＰｏｉｎｔｅｒＣ语言的安全性证明．篇幅所限，无法 列出的细节包括在相应技术报告［１２］中． ２．１ 犘狅犻狀狋犲狉犆的语法 ＰｏｉｎｔｅｒＣ［１２］是我们设计的一个类 Ｃ 的命令式 语言，它保留了 Ｃ语言核心语法特征：结构体声明、 全局变量声明、函数定义、控制流语句、表达式等．因 ＰｏｉｎｔｅｒＣ的语法和 Ｃ 接近，这里不再赘述．Ｐｏｉｎｔ ｅｒＣ类型系统的语法特征将在２．２节讨论． 和其它保证系统级编程语言安全性的工作［１３１４］ 不同，ＰｏｉｎｔｅｒＣ支持动态存储的手工管理，保留了 Ｃ 高效存储管理的特征，但这对安全性的静态检查提 出了 挑 战．因 此，除 静 态 类 型 系 统 外，我 们 还 使 用 指针逻辑系统和定理证明的方法，它们将在第３节 讨论． ２．２ 犘狅犻狀狋犲狉犆的类型系统 类型系统是一种静态检查程序的语法方法，它 一般根据程序短语的值的类别来对程序短语进行分 类，排除程序中上下文有关的错误．尽管类型系统已 经成为现代程序设计语言最流行的静态机制之一， 但现有语言的类型系统并不令人满意．Ｃ 和 Ｃ＋＋ 的类型系统不是可靠的，其类型系统不能对程序行 为提供安全保证；ＭＬ、Ｊａｖａ、Ｃ＃等语言的类型系统 虽然是可靠的，但对于表达式值或程序资源有关的 部分，要依赖低效的运行时动态检查（尽管某些编译 器能够静态移除部分检查）． ＰｏｉｎｔｅｒＣ包括 Ｃ语言大部分的类型，如整型、 指针、数组、结 构 等．类 型 强 制 很 容 易 导 致 难 以 排 除的程 序 漏 洞，如 把 整 型 数 据 用 作 指 针 等，因 此 ＰｏｉｎｔｅｒＣ禁止进行类型强制；同样，通常难以静态保 证多次对同一联合（ｕｎｉｏｎ）数据的读取是一致的，联 合类型也被禁止．这些限制不影响 ＰｏｉｎｔｅｒＣ的表达 能力和实际程序设计的可用性，例如，借鉴 Ｃ＋＋和 Ｊａｖａ，ＰｏｉｎｔｅｒＣ引入了布尔类型，代替 Ｃ对整型进行 类型强制来模拟布尔类型的做法．部分 Ｃ 类型被忽 略了，如浮点类型、字符类型等，因为它们和本文内 容关系不大． ＰｏｉｎｔｅｒＣ类型系统［１２］的定型规则除了包括通 常的定型断言外，还包括称为副条件的逻辑命题，这 些逻辑命题用于表达对值的约束（ｃｏｎｓｔｒａｉｎｔｓ）．和 已有的研究相比，ＰｏｉｎｔｅｒＣ 采用的这种结合副条件 的方式有显著的优点：首先，类型系统简单明了，避 免了使用依赖类型等带来的复杂性；其次，对这些命 题的证明可以使用指针逻辑系统（将第３节讨论）和 自动定理证明工具． 图１列出了 ＰｏｉｎｔｅｒＣ 类型系统部分代表性定 型规则，其它规则可参考技术报告［１２］ ．其中，Γ 是定 型环境（ｔｙｐｉｎｇｃｏｎｔｅｘｔ），由变量和类型的二元组列 表组成．位于横线上下的是通常的定型断言Γ !犲：τ， 即表达式犲在定型环境Γ 下的类型为τ．为和通常 的定型断言区别，副条件被写在一对大花括号内，并 置于定型规则右侧． Γ!犲：τ Γ!犲：τ ｛犲∈犲犳犳犲犮狋犻狏犲｝ （Ｄｅｒｅｆ） Γ!犾：τ［犖］ Γ!犲：ｉｎｔ Γ!犾［犲］：τ ｛０犲＜犖｝ （ＡｒｒａｙＦｉｅｌｄ） Γ!犾狏犪犾：τ Γ!犾狏犪犾＝ＮＵＬＬ；：狌狀犻狋｛!ｌｅａｋ（犾狏犪犾）｝ （ＡｓｎＮｕｌｌ） 图 １ ＰｏｉｎｔｅｒＣ的代表性定型规则 图１的３条规则说明了副条件的３种典型使 用．其中，对数 组 下 标 越 界 检 查 的 规 则 ＡｒｒａｙＦｉｅｌｄ 比较简单，只需检查相应的下标表达式犲在合法的 取值区间内；规则 Ｄｅｒｅｆ给指针引用定型，除了要求 犲在定型环境Γ 下具有指针类型τ 外，还规定表达 式犲的值必须是有效指针（即有具体的指向对象，见 第３节），由于这个条件涉及犲的值，因此它由副条 件犲∈犲犳犳犲犮狋犻狏犲给出；规则 ＡｓｎＮｕｌｌ给指针赋值语句 定 型，它 说 明 了 另 外 一 类 重 要 的 副 条 件：当 赋 ＮＵＬＬ值给某个左值犾狏犪犾时，必须确保不产生内存 泄漏（即确保犾狏犪犾原来指向的内存块在赋值后不会 访问不到），这个副条件用逻辑命题 !ｌｅａｋ（犾狏犪犾）表 示，显然内存分配语句也会使用到这个副条件［１２］ ． 需要指出，定型规则规定了该语句需满足的定 型条件以及副条件；但没有规定检查或证明这些副 条件的方式．在已有的研究中，传统类型系统的表达 ５５８ 计 算 机 学 报 ２００８年
4期 华保健等：安全语言PointerC的设计及形式证明 559 能力不足以推导或证明关于值（特别是指针类型变 部分.需要指出，实际的证明1)使用的都是完整的 量的值)的属性，这是我们设计指针逻辑并以逻辑系 机器状态定义， 统来证明这些副条件的部分原因. 2.4 PointerC的安全性定理 2.3 PointerC的操作语义 给出PointerC的类型系统和操作语义后，本节 PointerC操作语义的定义基于一个为PointerC 证明PointerC语言是安全性的.在给出形式证明之 设计的抽象机器模型M).PointerC包括声明变 前，首先讨论语言安全性的概念，这个概念基于对程 量、动态分配的指针类型变量、函数定义、函数调用 序运行时错误的区分 等语言特性，因此，它的抽象机器状态M由五元组 程序运行时错误可分为两类.一类程序运行时 构成：M=(S:H;G;R;K).其中，存储器(Store)S: 错误称为会被捕获的错误(trapped error),如除数 Var→Value把程序中的声明变量映射到值；堆H: 为零错误等；在许多计算机系统结构上，这样的错误 Addr→Value(Heap),把抽象的堆地址映射到值； 使得计算立即停止.然而，还有一些难以捉摸的错 G是全局数据区，对程序所有的代码可见：归约栈 误，它们引起数据遭破坏而不立即出现征兆，典型的 (evaluation stack)K规定语句和表达式的归约顺 例子是C中的数组越界访问.这类错误当时未引起 序；R是调用栈(call stack),规定函数调用和返回的 注意，而后引发难以预见的行为，因此，这类错误叫 控制转移（负责保存调用者的归约控制栈K和存储 做不会被捕获的错误(untrapped error).一个程序 器S). 段是安全的，如果它不可能引起不会被捕获错误的 PointerC的操作语义用抽象机器模型M上的 出现.所有程序段都是安全的语言叫做安全语言 状态转移规则来描述.程序的执行总是从一个初始 (safe language). 机器状态M开始，根据当前语句，使用状态转移规 PointerC的安全性定理的主要目的是证明：经 则到达后状态M'.在每个程序点，都至多有一条状 过类型检查且满足副条件的代码，在执行过程中，不 态转移规则可以使用：如果没有任何归约规则可以 会出现不会被捕获的错误.为此，我们把不会被捕获 使用，则产生错误， 的错误形式化为特定的安全策略(safety policy),然 在PointerC的操作语义的规则中，每个归约状 后基于这些安全策略证明PointerC的安全性， 态的形式是 具体讲，该定理的描述和定理的证明分成如下 (S;H;G;R;K)Da, 两个步骤： 其中(S;H;G;R;K)是当前抽象机状态，a是当前正 (1)在PointerC的机器模型和操作语义上形式 在被归约但还未完成的某个语法对象（如表达式、语 描述安全策略SP;安全策略SP实际上是定义在抽 句等).(S;H;G;R;K)Da称为在当前机器状态上 象机器模型M=(S:H)上的逻辑谓词，记作 的一个“结构”(configuration).PointerC操作语义 ESP(M), 的归约规则是结构间的二元关系“→”： 需要指出，我们使用符号仁来强调安全策略是在机 (S;H;G;R;K)Da(S';H';G;R';K')Da', 器模型上定义的语义性质. 即在抽象机状态(S;H;G;R;K)上归约语法对象a (2)证明形式描述的安全策略SP对于程序的 后，得到新的抽象机器状态(S:H';G;R';K'),并 操作语义→是一个不变式(invariant):即对于机器 在这个新状态下继续归约剩余的a'.典型的情况是 状态M=(S;H)和满足定型规则及所有副条件的 a是语句序列，而a'是该语句序列的尾；特别的，当 语句s,有 a是单条语句时，a'是空语句，此时我们用特殊符号 (=SP(M)∧(MDs→M'Ds')D卡SP(M'). e来表示a'.抽象机从初状态和完整程序开始执行， 非形式地说，第二点表明如果安全策略SP在 要么最终把所有的程序执行完，停在某个终状态；要 某个前抽象机器状态M上成立，并且满足相应定型 么陷入死循环，执行不终止，篇幅所限，此处略去 规则（包括副条件）的程序s在M上执行后得到新 PointerC操作语义的完整规则，细节可参考技术报 的机器状态M',则安全策略SP在M'上仍然成立 告[12 这样，不难得到结论：只要安全策略SP在抽象机初 在本文接下来的讨论中，存储器S和堆H的性 始状态M。上成立，它将在程序执行中的所有机器 质最重要，为陈述简单清晰起见，下面将使用只包括 状态M上成立. 存储器和堆的简化机器状态M=(S;H),省略其它 第一点中，PointerC的基本安全策略包括三个
能力不足以推导或证明关于值（特别是指针类型变 量的值）的属性，这是我们设计指针逻辑并以逻辑系 统来证明这些副条件的部分原因． ２．３ 犘狅犻狀狋犲狉犆的操作语义 ＰｏｉｎｔｅｒＣ操作语义的定义基于一个为ＰｏｉｎｔｅｒＣ 设计的抽象机器模型"［１２］ ．ＰｏｉｎｔｅｒＣ 包括声明变 量、动态分配的指针类型变量、函数定义、函数调用 等语言特性，因此，它的抽象机器状态"由五元组 构成："＝（犛；犎；犌；犚；犓）．其中，存储器（Ｓｔｏｒｅ）犛： 犞犪狉→犞犪犾狌犲把程序中的声明变量映射到值；堆 犎： 犃犱犱狉→犞犪犾狌犲（Ｈｅａｐ），把抽象的堆地址映射到值； 犌 是全局数据区，对程序所有的代码可见；归约栈 （ｅｖａｌｕａｔｉｏｎｓｔａｃｋ）犓 规定语句和表达式的归约顺 序；犚 是调用栈（ｃａｌｌｓｔａｃｋ），规定函数调用和返回的 控制转移（负责保存调用者的归约控制栈 犓 和存储 器犛）． ＰｏｉｎｔｅｒＣ的操作语义用抽象机器模型"上的 状态转移规则来描述．程序的执行总是从一个初始 机器状态"开始，根据当前语句，使用状态转移规 则到达后状态"′．在每个程序点，都至多有一条状 态转移规则可以使用；如果没有任何归约规则可以 使用，则产生错误． 在 ＰｏｉｎｔｅｒＣ的操作语义的规则中，每个归约状 态的形式是 （犛；犎；犌；犚；犓）犪， 其中（犛；犎；犌；犚；犓）是当前抽象机状态，犪是当前正 在被归约但还未完成的某个语法对象（如表达式、语 句等）．（犛；犎；犌；犚；犓）犪称为在当前机器状态上 的一个“结构”（ｃｏｎｆｉｇｕｒａｔｉｏｎ）．ＰｏｉｎｔｅｒＣ 操作语义 的归约规则是结构间的二元关系“ ”： （犛；犎；犌；犚；犓）犪 （犛′；犎′；犌′；犚′；犓′）犪′， 即在抽象机状态（犛；犎；犌；犚；犓）上归约语法对象犪 后，得到新的抽象机器状态（犛′；犎′；犌′；犚′；犓′），并 在这个新状态下继续归约剩余的犪′．典型的情况是 犪是语句序列，而犪′是该语句序列的尾；特别的，当 犪是单条语句时，犪′是空语句，此时我们用特殊符号 ε来表示犪′．抽象机从初状态和完整程序开始执行， 要么最终把所有的程序执行完，停在某个终状态；要 么陷 入 死 循 环，执 行 不 终 止．篇 幅 所 限，此 处 略 去 ＰｏｉｎｔｅｒＣ操作语义的完整规则，细节可参考技术报 告［１２］ ． 在本文接下来的讨论中，存储器犛和堆犎 的性 质最重要，为陈述简单清晰起见，下面将使用只包括 存储器和堆的简化机器状态"＝（犛；犎），省略其它 部分．需要指出，实际的证明［１５］使用的都是完整的 机器状态定义． ２．４ 犘狅犻狀狋犲狉犆的安全性定理 给出 ＰｏｉｎｔｅｒＣ的类型系统和操作语义后，本节 证明 ＰｏｉｎｔｅｒＣ语言是安全性的．在给出形式证明之 前，首先讨论语言安全性的概念，这个概念基于对程 序运行时错误的区分． 程序运行时错误可分为两类．一类程序运行时 错误称为会被捕获的错误（ｔｒａｐｐｅｄｅｒｒｏｒ），如除数 为零错误等；在许多计算机系统结构上，这样的错误 使得计算立即停止．然而，还有一些难以捉摸的错 误，它们引起数据遭破坏而不立即出现征兆，典型的 例子是 Ｃ中的数组越界访问．这类错误当时未引起 注意，而后引发难以预见的行为，因此，这类错误叫 做不会被捕获的错误（ｕｎｔｒａｐｐｅｄｅｒｒｏｒ）．一个程序 段是安全的，如果它不可能引起不会被捕获错误的 出现．所有 程 序 段 都 是 安 全 的 语 言 叫 做 安 全 语 言 （ｓａｆｅｌａｎｇｕａｇｅ）． ＰｏｉｎｔｅｒＣ的安全性定理的主要目的是证明：经 过类型检查且满足副条件的代码，在执行过程中，不 会出现不会被捕获的错误．为此，我们把不会被捕获 的错误形式化为特定的安全策略（ｓａｆｅｔｙｐｏｌｉｃｙ），然 后基于这些安全策略证明 ＰｏｉｎｔｅｒＣ的安全性． 具体讲，该定理的描述和定理的证明分成如下 两个步骤： （１）在 ＰｏｉｎｔｅｒＣ的机器模型和操作语义上形式 描述安全策略 #$；安全策略 # $ 实际上是定义在抽 象机器模型"＝（犛；犎）上的逻辑谓词，记作 #$（"）， 需要指出，我们使用符号 来强调安全策略是在机 器模型上定义的语义性质． （２）证明形式描述的安全策略 # $ 对于程序的 操作语义 是一个不变式（ｉｎｖａｒｉａｎｔ）：即对于机器 状态"＝（犛；犎）和满足定型规则及所有副条件的 语句狊，有 （ #$（"）∧（"狊 "′狊′）） #$（"′）． 非形式地说，第二点表明如果安全策略 # $ 在 某个前抽象机器状态"上成立，并且满足相应定型 规则（包括副条件）的程序狊在"上执行后得到新 的机器状态"′，则安全策略 # $ 在"′上仍然成立． 这样，不难得到结论：只要安全策略 # $在抽象机初 始状态"０上成立，它将在程序执行中的所有机器 状态"上成立． 第一点中，ＰｏｉｎｔｅｒＣ 的基本安全策略包括三个 ４ 期 华保健等：安全语言 ＰｏｉｎｔｅｒＣ的设计及形式证明 ５５９
560 计算 乡 学报 2008年 方面：无空指针或悬空指针引用（也禁止把它们用作 YIE Dom(H).(3q.V(q)=1), free函数的参数)、无数组下标越界、无内存泄漏.前 此即=NoLeak(S;H').对其它情况的证明类似， 两个比较简单，可参考技术报告和Coq实现].最 对其它定型使用了副条件的语句同样可以证明. 复杂的是最后一个，为此，我们引入机器状态M= 证毕 (S;H)上的NoLeak谓词 不同于通常的手工证明方法，为严格起见，该定 NoLeak(S;H)△Vl∈Dom(H).(3p.V(p)=l), 理的完整描述和形式证明都已在证明辅助工具Coq 该谓词表达当前抽象机状态无内存泄漏的性质，即 中完成，细节可参考技术报告和Coq实现] 对抽象机状态M=(S;H),若对堆H上的任意地 对一般C程序而言，完全静态推理其无内存泄 址1，都存在一个从存储器S出发的指针p指向，则 漏的性质是困难的，在PointerC中加入的一些限制 该机器状态M无内存泄漏.其中，对于给定的M= (如禁止取地址操作&等)使得静态推理这类性质 (S;H),函数V 成为可能。 V(S,H,p)= S(p), 若p是声明变量 3 指针逻辑及其可靠性证明 H(V(S,H,q)(n),若p=q→n 基于对p的语法形式归纳返回指针p的值.注意， 2.2节介绍了定型规则中的副条件，这些副条 在NoLeak谓词的定义中，为了简单，我们略去了V 件表达了对程序语法表达式值的约束.对这些副条 的机器状态参数(S;H). 件的检查可以使用在Java等语言中流行的动态检 和V的定义类似，在PointerC的安全性定理证 查方法，由编译器在需要检查副条件的程序点插人 明中要用到求一个指针初始声明变量的Root操作： 额外指令；也可以使用静态检查的方法，在编译期间 Root(p)= p. 若p是声明变量 证明副条件.我们设计了一种指针逻辑[10-)，它以 Root(q),若p=q→n 静态方式检查和保证这些副条件.和动态方法比较， 对无内存泄漏的安全策略，我们证明了它对语 使用指针逻辑这种静态机制的优点是：首先，程序漏 句的执行是一个不变式：如果在无内存泄漏的状态 洞可在开发阶段被捕获：其次，可以提高目标代码的 下执行所有副条件都成立的程序，执行后得到的状 运行效率，这在许多应用中至关重要，当然，指针逻 态也一定无内存泄漏.即证明了以下定理， 辑的使用给静态证明提出了挑战，因此，我们使用自 定理1（无内存泄漏）.对任意机器状态M= 动定理证明工具，而不是只依赖类型检查器 (S:H)及语句s,其中s是良类型的且满足定型规则中 本节简要介绍指针逻辑的设计思想，然后给出 所用到的所有副条件，若仁NoLeak(S;H)且存在归 指针逻辑的可靠性证明。 约(S;H)>s→(S;H')Ds',则=NoLeak(S';H'). 3.1指针逻辑的设计 证明.基于对语句s的结构归纳.可按对语句 指针逻辑本质上是对Hoare逻辑的一种扩展， s的定型是否使用了副条件把语句分为两类.如果s 它的设计主要基于以下考虑： 的定型规则中没有用到副条件，则证明是简单的.复 (l)若在程序点能区分有效指针(effective 杂的是s的定型规则中使用了副条件的情况.我们 pointers)、空指针、悬空指针(dangling pointers),并 以语句s是指针赋值语句p=NULL为例说明证明 且知道有效指针之间是否相等，则不但能判断有关 思路.图1中的规则AsnNull给语句p=NULL定 指针的操作是否安全，还可得出经过这步操作后指 型，它包括的副条件一leak(p)说明 针信息的变化 3p'.(Root(p)≠Root(p'))∧(V(p)=V(p')). (2)用Hoare逻辑风格的推理规则来表达指针 对p的语法形式进行归纳：如果p是声明变量，则 信息的变化，就可以把这些信息用于证明程序的其 由条件=NoLeak(S;H)可知 它性质，同时把程序分析、类型系统和程序验证联系 YIE Dom(H).(3q.V(q)=l), 起来，有更好的表达能力. 因此，在赋值前有 指针逻辑的设计难点在于指针类型和动态变 3IE Dom(H).(V(p)=V(p')=1), 量，并且有关指针性质的推导同程序其它性质的推 赋值后，显然有3l∈Dom(H).(V(p')=l),并且新 导有很大的区别.例如，在free(p)语句执行后，为防 的状态S'=S[p一NULL]且H'=H,则可得到 止悬空指针引用，在p被重新赋值指向别的对象之
方面：无空指针或悬空指针引用（也禁止把它们用作 ｆｒｅｅ函数的参数）、无数组下标越界、无内存泄漏．前 两个比较简单，可参考技术报告和 Ｃｏｑ实现［１５］ ．最 复杂的是最后一个，为此，我们引入机器状态"＝ （犛；犎）上的 犖狅犔犲犪犽谓词 犖狅犔犲犪犽（犛；犎）犾∈犇狅犿（犎）．（狆．犞（狆）＝犾）， 该谓词表达当前抽象机状态无内存泄漏的性质，即 对抽象机状态"＝（犛；犎），若对堆 犎 上的任意地 址犾，都存在一个从存储器犛出发的指针狆 指向，则 该机器状态"无内存泄漏．其中，对于给定的"＝ （犛；犎），函数犞 犞（犛，犎，狆）＝ 犛（狆）， 若狆是声明变量 ｛犎（犞（犛，犎，狇））（狀）， 若狆＝狇→狀 ， 基于对狆的语法形式归纳返回指针狆 的值．注意， 在 犖狅犔犲犪犽谓词的定义中，为了简单，我们略去了犞 的机器状态参数（犛；犎）． 和犞 的定义类似，在 ＰｏｉｎｔｅｒＣ的安全性定理证 明中要用到求一个指针初始声明变量的犚狅狅狋操作： 犚狅狅狋（狆）＝ 狆， 若狆是声明变量 ｛犚狅狅狋（狇）， 若狆＝狇→狀 ． 对无内存泄漏的安全策略，我们证明了它对语 句的执行是一个不变式：如果在无内存泄漏的状态 下执行所有副条件都成立的程序，执行后得到的状 态也一定无内存泄漏．即证明了以下定理． 定理１（无内存泄漏）． 对任意机器状态"＝ （犛；犎）及语句狊，其中狊是良类型的且满足定型规则中 所用到的所有副条件，若 犖狅犔犲犪犽（犛；犎）且存在归 约（犛；犎）狊（犛′；犎′）狊′，则 犖狅犔犲犪犽（犛′；犎′）． 证明． 基于对语句狊的结构归纳．可按对语句 狊的定型是否使用了副条件把语句分为两类．如果狊 的定型规则中没有用到副条件，则证明是简单的．复 杂的是狊的定型规则中使用了副条件的情况．我们 以语句狊是指针赋值语句狆＝ＮＵＬＬ为例说明证明 思路．图１中的规则 ＡｓｎＮｕｌｌ给语句狆＝ＮＵＬＬ 定 型，它包括的副条件 !ｌｅａｋ（狆）说明 狆′．（犚狅狅狋（狆）≠犚狅狅狋（狆′））∧（犞（狆）＝犞（狆′））． 对狆的语法形式进行归纳：如果狆 是声明变量，则 由条件 犖狅犔犲犪犽（犛；犎）可知 犾∈犇狅犿（犎）．（狇．犞（狇）＝犾）， 因此，在赋值前有 犾∈犇狅犿（犎）．（犞（狆）＝犞（狆′）＝犾）， 赋值后，显然有犾∈犇狅犿（犎）．（犞（狆′）＝犾），并且新 的状态犛′＝犛［狆!ＮＵＬＬ］且 犎′＝犎，则可得到 犾∈犇狅犿（犎′）．（狇．犞（狇）＝犾）， 此即 犖狅犔犲犪犽（犛′；犎′）．对其它情况的证明类似． 对其它定型使用了副条件的语句同样可以证明． 证毕． 不同于通常的手工证明方法，为严格起见，该定 理的完整描述和形式证明都已在证明辅助工具 Ｃｏｑ 中完成，细节可参考技术报告和 Ｃｏｑ实现［１５］ ． 对一般 Ｃ程序而言，完全静态推理其无内存泄 漏的性质是困难的，在 ＰｏｉｎｔｅｒＣ中加入的一些限制 （如禁止取地址操作 牔 等）使得静态推理这类性质 成为可能． ３ 指针逻辑及其可靠性证明 ２．２节介绍了定型规则中的副条件，这些副条 件表达了对程序语法表达式值的约束．对这些副条 件的检查可以使用在Ｊａｖａ等语言中流行的动态检 查方法，由编译器在需要检查副条件的程序点插入 额外指令；也可以使用静态检查的方法，在编译期间 证明副条件．我们设计了一种指针逻辑［１０１１］，它以 静态方式检查和保证这些副条件．和动态方法比较， 使用指针逻辑这种静态机制的优点是：首先，程序漏 洞可在开发阶段被捕获；其次，可以提高目标代码的 运行效率，这在许多应用中至关重要．当然，指针逻 辑的使用给静态证明提出了挑战，因此，我们使用自 动定理证明工具，而不是只依赖类型检查器． 本节简要介绍指针逻辑的设计思想，然后给出 指针逻辑的可靠性证明． ３．１ 指针逻辑的设计 指针逻辑本质上是对 Ｈｏａｒｅ逻辑的一种扩展， 它的设计主要基于以下考虑： （１）若 在 程 序 点 能 区 分 有 效 指 针 （ｅｆｆｅｃｔｉｖｅ ｐｏｉｎｔｅｒｓ）、空指针、悬空指针（ｄａｎｇｌｉｎｇｐｏｉｎｔｅｒｓ），并 且知道有效指针之间是否相等，则不但能判断有关 指针的操作是否安全，还可得出经过这步操作后指 针信息的变化． （２）用 Ｈｏａｒｅ逻辑风格的推理规则来表达指针 信息的变化，就可以把这些信息用于证明程序的其 它性质，同时把程序分析、类型系统和程序验证联系 起来，有更好的表达能力． 指针逻辑的设计难点在于指针类型和动态变 量，并且有关指针性质的推导同程序其它性质的推 导有很大的区别．例如，在ｆｒｅｅ（狆）语句执行后，为防 止悬空指针引用，在狆 被重新赋值指向别的对象之 ５６０ 计 算 机 学 报 ２００８年
4期 华保健等：安全语言PointerC的设计及形式证明 561 前，不能用p或与p相等的指针去访问p原来所指 作为单元素的有效指针集合（因为只有p一个指针 向的内存；再如，在对有效指针q赋值时，为防止出 指向刚分配的单元)，而且要把该单元的所有指针域 现内存泄漏，需要知道是否存在有与q相等的指针， 都加入悬空指针集合中（都是悬空的），最后把p从 为解决这些难点，以使静态推理成为可能，指针 空指针集合中删除.其它规则的含义类似，只是加入 逻辑在每个程序点区分三类指针：有效指针、空指 了更多的基本函数和谓词来处理较复杂的情 针、悬空指针，分别用指针集合Ⅱ，W,D来表示它 况[o-1叮.其次，这种从前向后的推理形式，使得对验 们，这些集合实质上只是相应逻辑命题的一种语法 证条件(verification condition)的计算也可使用最强 美化(syntactic sugar).例如，对有效指针集合Ⅱ= 后条件演算的方式：最后，规则形式的一致性，方 {s,t}八{p,q},Ⅱ实际上等价于逻辑命题(s=t)八 便我们借鉴传统Hoare逻辑可靠性证明的方式，证 (s∈effective)∧(p=q)∧(s∈effective)∧(s！=p). 明指针逻辑的可靠性。 可以看出，使用指针集合这样的语法美化，大大简化 Pn..>))) struct List nert: 图3指针逻辑的代表性规则 (p)Alp->next)Aip->next-next,glN 3.2指针逻辑的可靠性证明 q=alloc(struct List): Ap}A(p->>next)Aip->>next->next)NAiq)Alq->>nexi)D 我们证明了指针逻辑相对PointerC操作语义 q->nexi=p->next: 是可靠性的，所用方法同Hoare逻辑可靠性证明没 Ap}Aip->next.q-next)Aip-next-next)NAdgh p->next=NULL: 有本质区别，也是先在机器模型和操作语义上给出断 Ap)Aig->next)Aiq->next>nert.p->next}NAigh 言的语义解释，然后证明每条公理和推理规则对操作 p->>next=q: Ap)Aiq->next)A(q->>next->>next)NA(q.p->next} 语义都是可靠的).即要证明，若断言{P}s{Q}在指 针逻辑中可以证明，则在任何满足前断言P的状态 图2用指针逻辑推理单链表插入代码 M下执行程序段s后，得到的新状态M'一定满足 图2的第1行断言给出指针在当前程序点的状 后断言Q.我们证明了如下的定理. 态：p和p->next是有效指针，并且指向不同的单 定理2（指针逻辑可靠性定理）.若(S;H)仁 元；而p->next>ext和q都是空指针.第2行分 P,且(S;H)Ds→(S';H')De,则有(S:H')=Q. 配一个新的链表节点，并把它赋值给q:这个操作所 证明，首先用定理证明工具Coq表示Point- 引起的指针变化反映在第3行的断言中，即q被加 erC语法、类型系统、操作语义等；然后在Coq中形 入到一个单元素的有效集合，而q>next被加入到 式化指针逻辑的断言和定理；最后在Coq中基于对 悬空指针集合D中.按这种方式，可以推理图2中剩 语句s的结构归纳完成该证明.需要注意，在操作语 余的代码. 义的规则中得到的结构的形式是(S;H')>e,即整 图3列出了图2例子中使用到的部分指针逻辑 个语句归约到了空语句e. 证毕 推理规则10-1门.这些规则体现了指针逻辑的三个主 限于篇幅，这里无法给出语义函数仁的完整定 要特点：首先是规则形式和Hoare逻辑规则的一致 义，细节可参考技术报告[町.和对PointerC语言的 性.以Malloc规则为例，它描述了进行内存分配并 安全性证明相同，为更严格，证明过程在辅助工具 给变量p赋值的演算过程：如果前面的指针集合是 Cog]中机械化完成，而非手工进行.下面给出该证 Ⅱ∧W八D,并且p属于W集合（即p的值为NULL. 明的一些细节步骤和定理，对该证明的更详细的讨 这里使用符号<：表示集合的属于关系，而没有使用 论（包括PointerC语法、类型系统和操作语义相应 集合符号∈，是因为<：比∈表达了一种更广意义上 的Coq表示，定理在Coq中的表达等)可参考技术 的属于关系，细节参见文献[10])，则赋值后，应把p 报告]
前，不能用狆或与狆 相等的指针去访问狆 原来所指 向的内存；再如，在对有效指针狇赋值时，为防止出 现内存泄漏，需要知道是否存在有与狇相等的指针． 为解决这些难点，以使静态推理成为可能，指针 逻辑在每个程序点区分三类指针：有效指针、空指 针、悬空指 针，分 别 用 指 针 集 合 Π，%，& 来 表 示 它 们，这些集合实质上只是相应逻辑命题的一种语法 美化（ｓｙｎｔａｃｔｉｃｓｕｇａｒ）．例如，对有效指针集合 Π＝ ｛狊，狋｝∧｛狆，狇｝，Π 实际上等价于逻辑命题（狊＝狋）∧ （狊∈犲犳犳犲犮狋犻狏犲）∧（狆＝狇）∧（狊∈犲犳犳犲犮狋犻狏犲）∧（狊！＝狆）． 可以看出，使用指针集合这样的语法美化，大大简化 了记号．下面用 Ψ 表示Π∧%∧&． 基于这些记号，图２给出了用指针逻辑推理单链 表插入代码片段的例程（为了和断言区别，代码进行 了缩进）．其中，狆，狇是具有如下单链表类型的指针： ｓｔｒｕｃｔＬｉｓｔ｛ ｉｎｔ犱犪狋犪； ｓｔｒｕｃｔＬｉｓｔ狀犲狓狋； ｝ ｛狆｝∧｛狆－＞狀犲狓狋｝∧｛狆－＞狀犲狓狋－＞狀犲狓狋，狇｝% 狇＝犪犾犾狅犮（ｓｔｒｕｃｔＬｉｓｔ）； ｛狆｝∧｛狆－＞狀犲狓狋｝∧｛狆－＞狀犲狓狋－＞狀犲狓狋｝%∧｛狇｝∧｛狇－＞狀犲狓狋｝& 狇－＞狀犲狓狋＝狆－＞狀犲狓狋； ｛狆｝∧｛狆－＞狀犲狓狋，狇－＞狀犲狓狋｝∧｛狆－＞狀犲狓狋－＞狀犲狓狋｝%∧｛狇｝ 狆－＞狀犲狓狋＝ＮＵＬＬ； ｛狆｝∧｛狇－＞狀犲狓狋｝∧｛狇－＞狀犲狓狋－＞狀犲狓狋，狆－＞狀犲狓狋｝%∧｛狇｝ 狆－＞狀犲狓狋＝狇； ｛狆｝∧｛狇－＞狀犲狓狋｝∧｛狇－＞狀犲狓狋－＞狀犲狓狋｝%∧｛狇，狆－＞狀犲狓狋｝ 图 ２ 用指针逻辑推理单链表插入代码 图２的第１行断言给出指针在当前程序点的状 态：狆和狆－＞狀犲狓狋是有效指针，并且指向不同的单 元；而狆－＞狀犲狓狋－＞狀犲狓狋和狇 都是空指针．第２行分 配一个新的链表节点，并把它赋值给狇；这个操作所 引起的指针变化反映在第３行的断言中，即狇被加 入到一个单元素的有效集合，而狇－＞狀犲狓狋被加入到 悬空指针集合&中．按这种方式，可以推理图２中剩 余的代码． 图３列出了图２例子中使用到的部分指针逻辑 推理规则［１０１１］ ．这些规则体现了指针逻辑的三个主 要特点：首先是规则形式和 Ｈｏａｒｅ逻辑规则的一致 性．以 Ｍａｌｌｏｃ规则为例，它描述了进行内存分配并 给变量狆赋值的演算过程：如果前面的指针集合是 Π∧%∧&，并且狆属于%集合（即狆 的值为 ＮＵＬＬ． 这里使用符号＜：表示集合的属于关系，而没有使用 集合符号∈，是因为＜：比∈表达了一种更广意义上 的属于关系，细节参见文献［１０］），则赋值后，应把狆 作为单元素的有效指针集合（因为只有狆 一个指针 指向刚分配的单元），而且要把该单元的所有指针域 都加入悬空指针集合中（都是悬空的），最后把狆 从 空指针集合中删除．其它规则的含义类似，只是加入 了 更 多 的 基 本 函 数 和 谓 词 来 处 理 较 复 杂 的 情 况［１０１１］ ．其次，这种从前向后的推理形式，使得对验 证条件（ｖｅｒｉｆｉｃａｔｉｏｎｃｏｎｄｉｔｉｏｎ）的计算也可使用最强 后条件演算的方式［１０］；最后，规则形式的一致性，方 便我们借鉴传统 Ｈｏａｒｅ逻辑可靠性证明的方式，证 明指针逻辑的可靠性． 狆＜：& 狇＜：Π ｛Π∧%∧&｝狆＝狇｛（Πａｄｄ狆ｔｏ狇）∧%∧&／狆｝ （Ａｓｎ＿ＤＥ） 狆＜：Π狇＜：% !ｌｅａｋ（狆） ｛Π∧%∧&｝狆＝狇｛Π／狆∧（%＼狆∪｛狆｝）∧&＼狆｝ （Ａｓｎ＿ＥＮ） 狆＜：% 狇＜：Π ｛Π∧%∧&｝狆＝狇｛（Πａｄｄ狆ｔｏ狇）∧%／狆∧&｝ （Ａｓｎ＿ＮＥ） 狆＜：% ｛Π∧%∧&｝狆＝犪犾犾狅犮（犜） ｛（Π＋狆）∧%／狆∧（&∪｛狆－＞狉１，…，狆－＞狉狀｝）｝ （Ｍａｌｌｏｃ） 图 ３ 指针逻辑的代表性规则 ３．２ 指针逻辑的可靠性证明 我们证明了指针逻辑相对 ＰｏｉｎｔｅｒＣ 操作语义 是可靠性的，所用方法同 Ｈｏａｒｅ逻辑可靠性证明没 有本质区别，也是先在机器模型和操作语义上给出断 言的语义解释，然后证明每条公理和推理规则对操作 语义都是可靠的［１５］ ．即要证明，若断言｛犘｝狊｛犙｝在指 针逻辑中可以证明，则在任何满足前断言 犘 的状态 "下执行程序段狊 后，得到的新状态"′一定满足 后断言犙．我们证明了如下的定理． 定理２（指针逻辑可靠性定理）． 若（犛；犎） 犘，且（犛；犎）狊 （犛′；犎′）ε，则有（犛′；犎′）犙． 证明． 首先用定理证明工具 Ｃｏｑ表示 Ｐｏｉｎｔ ｅｒＣ语法、类型系统、操作语义等；然后在 Ｃｏｑ中形 式化指针逻辑的断言和定理；最后在 Ｃｏｑ中基于对 语句狊的结构归纳完成该证明．需要注意，在操作语 义的规则中得到的结构的形式是（犛′；犎′）ε，即整 个语句归约到了空语句ε． 证毕． 限于篇幅，这里无法给出语义函数 的完整定 义，细节可参考技术报告［１５］ ．和对 ＰｏｉｎｔｅｒＣ 语言的 安全性证明相同，为更严格，证明过程在辅助工具 Ｃｏｑ［１６］中机械化完成，而非手工进行．下面给出该证 明的一些细节步骤和定理，对该证明的更详细的讨 论（包括 ＰｏｉｎｔｅｒＣ 语法、类型系统和操作语义相应 的 Ｃｏｑ表示，定理在 Ｃｏｑ中的表达等）可参考技术 报告［１５］ ． ４ 期 华保健等：安全语言 ＰｏｉｎｔｅｒＣ的设计及形式证明 ５６１
562 计 算 机学 报 2008年 指针类型赋值语句的推理规则和Hoare逻辑 系统是不可靠的，所以为保证语言的安全性，仍需依 赋值公理完全不一样，另外还有新增的malloc和 赖动态检查机制，这在很多情况下降低了系统效率。 free语句的规则，所以，指针逻辑可靠性的证明实际 而PointerC的安全性保证了通过静态验证的程 上分成如下3个步骤： 序不需要进行动态检查.另外，与本文工作不同， (1)证明基本语句s(指针赋值、调用、malloc、 CCured使用垃圾收集器，回避了指针推理的难点； free等)的推理规则 而PointerC支持C的动态存储管理的机制，并且能 P(Ψ亚) 够用指针逻辑推理其安全性， {Ψ}s{Ψ Cyclonel为C设计新的类型系统，重点是加 是可靠的，其中P(平)是指该规则中以平为参数的 入更多高级语言特性和类型.本文工作和Cyclone 前提.若对s语句定型时所用各定型规则的附加条 的主要区别在于Cyclone使用基于区域的存储管理 件是C1,…,Cm,则要证明（其中卜是通常的语法可 (region-based memory management),基于区域的 证符号)如下引理， 存储管理除了自身有较大局限性外，还要求程序员 引理1（指针逻辑可靠性定理，指针部分）.若 在代码中加入对这些机制的支持代码，因此，难以改 上平∧P(平)→C1∧…∧C。, 写现有的C遗留代码以适应Cyclone的要求.而 则对任何满足(S:H)仁平∧P(平)的状态(S:H), PointerC的副条件生成由编译器自动完成， 有 Xi等人的ATS(Applied Type System)项目] (S:H)=C1∧…∧Cm 和本文工作类似，也把Hoare逻辑形式的断言引入 且若(S;H)Da→(S;H')Db,则(S;H')=平 类型系统，从而在类型系统上模拟Hoare逻辑的部 证明.基于对语句s的结构归纳可证， 分推理.但本文工作和ATS的重要区别在于ATS (2)证明整型赋值语句a的推理规则 的类型系统需要程序员显式标注，加大了理解和使 {Ψ∧(Q[y1x]…[ymx][x←-e])}x=e{平AQ》 用难度；而且，由于类型检查的表达能力有限，ATS (y1,…,yn构成closure(x)的所有成员[町) 仅能推理整数等较简单论域的性质.而本文工作使 是可靠的.若对语句x=e定型时所用各定型规则的 用单独的指针逻辑系统对副条件进行推理，从而能 附加条件是C1,…,Cm,则要证明如下引理， 够证明更强的程序安全属性。 引理2（指针逻辑可靠性定理，整型部分）.如果 ESC(Extended Static Checking)[us和Spec#[i町 上Ψ∧P(Ψ)→C1∧…∧Cm, 等将Hoare逻辑推理方法用于检查Modular-3、 则对任何满足(S:H)=平的状态(S:H),有 Java、C#等程序.本文工作与这些研究的本质区别 (S;H)=CA…∧Ca 在于：ESC等只是程序查错工具，而不是程序设计 且若(S;H)Ds→(S:H')Ds',则(S;H')=Ψ 或验证工具，它们没有给出可靠性证明.而本文工作 证明.基于对语句s的结构归纳可证 使用指针逻辑来推理和证明验证条件，并证明了该 (3)复合、条件和循环语句的规则以及推论规 指针逻辑的可靠性；另外，本文证明了PointerC语 则等的可靠性的证明.它们完全与Hoare逻辑可靠 言是安全性的 性中相应规则的证明方式相同. Caduceus「2o]是一个C程序验证框架，它支持多 个定理证明器作为后端.本文工作和Caduceus的重 4 相关工作 要区别在于：Caduceus的可靠性没有经过严格证 明；并且Caduceus仅支持C很简单的一个小子集， C语言安全性问题主要是出于效率和编程灵活 对被验证程序提出了很多限制，例如，Caduceus禁 性的考虑.随着类型系统理论的发展和程序分析技术 止程序中出现别名 的成熟，最近几年，一些项目尝试改造C,或设计它 Clighta)是Xavier Leroy等人为在Coq中验证 的安全变种.CCuredt13]是对C程序进行分析和变 编译器的前端而设计的一个小类C的语言.和本文 换的框架，它使用静态程序分析排除程序漏洞.为了 工作类似，Clight的语义也被形式在Cog中.但和本 保证分析的可行性，CCured提出了两种方案：(1)允 文工作不同，Clight仅包含了C的核心语法结构，完 许程序员在C代码上加入额外标注作为给静态分 全去掉了动态存储特性，这限制了Clight的表达能 析器的提示；(2)插入动态检查代码.CCured的类型 力.而PointerC语言保留了C的动态存储管理机
指针类型赋值语句的推理规则和 Ｈｏａｒｅ逻辑 赋值公理 完 全 不 一 样，另 外 还 有 新 增 的 ｍａｌｌｏｃ和 ｆｒｅｅ语句的规则，所以，指针逻辑可靠性的证明实际 上分成如下３个步骤： （１）证明基本语句狊（指针赋值、调用、ｍａｌｌｏｃ、 ｆｒｅｅ等）的推理规则 犘（Ψ） ｛Ψ｝狊｛Ψ′｝ 是可靠的，其中 犘（Ψ）是指该规则中以 Ψ 为参数的 前提．若对狊语句定型时所用各定型规则的附加条 件是犆１，…，犆狀，则要证明（其中 ! 是通常的语法可 证符号）如下引理． 引理１（指针逻辑可靠性定理，指针部分）． 若 !Ψ∧犘（Ψ）犆１∧…∧犆狀， 则对任何满足（犛；犎）Ψ∧犘（Ψ）的状态（犛；犎）， 有 （犛；犎）犆１∧…∧犆狀． 且若（犛；犎）犪 （犛′；犎′）犫，则（犛′；犎′）Ψ′． 证明． 基于对语句狊的结构归纳可证． （２）证明整型赋值语句犪的推理规则 ｛Ψ∧（犙［狔１←狓］…［狔狀←狓］［狓←犲］）｝狓＝犲｛Ψ∧犙｝ （狔１，…，狔狀构成犮犾狅狊狌狉犲（狓）的所有成员［９］） 是可靠的．若对语句狓＝犲定型时所用各定型规则的 附加条件是犆１，…，犆狀，则要证明如下引理． 引理２（指针逻辑可靠性定理，整型部分）． 如果 !Ψ∧犘（Ψ）犆１∧…∧犆狀， 则对任何满足（犛；犎）Ψ 的状态（犛；犎），有 （犛；犎）犆１∧…∧犆狀． 且若（犛；犎）狊 （犛′；犎′）狊′，则（犛′；犎′）Ψ′． 证明． 基于对语句狊的结构归纳可证． （３）复合、条件和循环语句的规则以及推论规 则等的可靠性的证明．它们完全与 Ｈｏａｒｅ逻辑可靠 性中相应规则的证明方式相同． ４ 相关工作 Ｃ语言安全性问题主要是出于效率和编程灵活 性的考虑．随着类型系统理论的发展和程序分析技术 的成熟，最近几年，一些项目尝试改造 Ｃ，或设计它 的安全变种．ＣＣｕｒｅｄ［１３］是对 Ｃ 程序进行分析和变 换的框架，它使用静态程序分析排除程序漏洞．为了 保证分析的可行性，ＣＣｕｒｅｄ提出了两种方案：（１）允 许程序员在 Ｃ 代码上加入额外标注作为给静态分 析器的提示；（２）插入动态检查代码．ＣＣｕｒｅｄ的类型 系统是不可靠的，所以为保证语言的安全性，仍需依 赖动态检查机制，这在很多情况下降低了系统效率． 而 ＰｏｉｎｔｅｒＣ 的 安 全 性 保 证 了 通 过 静 态 验 证 的 程 序不需要 进 行 动 态 检 查．另 外，与 本 文 工 作 不 同， ＣＣｕｒｅｄ使用垃圾收集器，回避了指针推理的难点； 而ＰｏｉｎｔｅｒＣ支持 Ｃ的动态存储管理的机制，并且能 够用指针逻辑推理其安全性． Ｃｙｃｌｏｎｅ［１４］为 Ｃ设计新的类型系统，重点是加 入更多高级语言特性和类型．本文工作和 Ｃｙｃｌｏｎｅ 的主要区别在于 Ｃｙｃｌｏｎｅ使用基于区域的存储管理 （ｒｅｇｉｏｎｂａｓｅｄｍｅｍｏｒｙｍａｎａｇｅｍｅｎｔ），基于区域的 存储管理除了自身有较大局限性外，还要求程序员 在代码中加入对这些机制的支持代码，因此，难以改 写现 有 的 Ｃ 遗 留 代 码 以 适 应 Ｃｙｃｌｏｎｅ的 要 求．而 ＰｏｉｎｔｅｒＣ的副条件生成由编译器自动完成． Ｘｉ等人的 ＡＴＳ（ＡｐｐｌｉｅｄＴｙｐｅＳｙｓｔｅｍ）项目［６］ 和本文工作类似，也把 Ｈｏａｒｅ逻辑形式的断言引入 类型系统，从而在类型系统上模拟 Ｈｏａｒｅ逻辑的部 分推理．但本文工作和 ＡＴＳ的重要区别在于 ＡＴＳ 的类型系统需要程序员显式标注，加大了理解和使 用难度；而且，由于类型检查的表达能力有限，ＡＴＳ 仅能推理整数等较简单论域的性质．而本文工作使 用单独的指针逻辑系统对副条件进行推理，从而能 够证明更强的程序安全属性． ＥＳＣ（ＥｘｔｅｎｄｅｄＳｔａｔｉｃＣｈｅｃｋｉｎｇ）［１８］和Ｓｐｅｃ＃ ［１９］ 等将 Ｈｏａｒｅ 逻 辑 推 理 方 法 用 于 检 查 Ｍｏｄｕｌａｒ３、 Ｊａｖａ、Ｃ＃等程序．本文工作与这些研究的本质区别 在于：ＥＳＣ等只是程序查错工具，而不是程序设计 或验证工具，它们没有给出可靠性证明．而本文工作 使用指针逻辑来推理和证明验证条件，并证明了该 指针逻辑的可靠性；另外，本文证明了 ＰｏｉｎｔｅｒＣ 语 言是安全性的． Ｃａｄｕｃｅｕｓ［２０］是一个 Ｃ程序验证框架，它支持多 个定理证明器作为后端．本文工作和 Ｃａｄｕｃｅｕｓ的重 要区别在 于：Ｃａｄｕｃｅｕｓ的 可 靠 性 没 有 经 过 严 格 证 明；并且 Ｃａｄｕｃｅｕｓ仅支持 Ｃ很简单的一个小子集， 对被验证程序提出了很多限制，例如，Ｃａｄｕｃｅｕｓ禁 止程序中出现别名． Ｃｌｉｇｈｔ［２１］是ＸａｖｉｅｒＬｅｒｏｙ等人为在Ｃｏｑ中验证 编译器的前端而设计的一个小类 Ｃ 的语言．和本文 工作类似，Ｃｌｉｇｈｔ的语义也被形式在Ｃｏｑ中．但和本 文工作不同，Ｃｌｉｇｈｔ仅包含了Ｃ的核心语法结构，完 全去掉了动态存储特性，这限制了 Ｃｌｉｇｈｔ的表达能 力．而 ＰｏｉｎｔｅｒＣ 语言保留了 Ｃ 的动态存储管理机 ５６２ 计 算 机 学 报 ２００８年
4期 华保健等：安全语言PointerC的设计及形式证明 563 制，适合验证更实际的指针程序 1782.London:Springer-Verlag,2000:366-381 [8]Hoare C A R.An axiomatic basis for computer program- 5结论和进一步的工作 ming.Communications of the ACM.1969,12(10):576-580 [9]Necula G C.Proof-carrying code//Proceedings of the 24th ACM SIGPLAN-SIGACT Symposium on Principles of Pro- 本文在系统级安全语言设计和实现以及性质证 gramming Languages.Paris.France.1997:106-119 明方面做了有益尝试.我们采用一种类型系统和逻 [10] Chen YY.Ge L.Hua BJ,Li Z P.Liu C.Wang Z F.A 辑系统相结合的静态机制保证语言的安全性.为了 pointer logic and certifying compiler.Frontiers of Computer Science in China.2007.1(3):297-312 考察这种机制的实际可行性，我们设计了一个类C [11] Chen Yi-Yun.Hua Bao-Jian.Ge Lin,Wang Zhi-Fang.A 的命令式语言PointerC,它的新颖之处在于定型规 pointer logic for safety verification of pointer programs.Chi- 则中包括副条件断言.基于形式定义的安全策略，本 nese Journal of Computers.2008,31(3):372-380(in Chi- 文证明定理PointerC的安全性.为了静态推理指针 nese) 类型的断言，我们在前期工作中提出了指针逻辑，以 (陈意云，华保健，葛琳，王志芳.一种用于指针程序安全性证 解决Hoare逻辑处理别名问题所面临的困难.本文 明的指针逻辑.计算机学报，2008,31(3)：372-380) [12]Hua BJ,Chen YY,Ge L.Wang Z F.The PointerC pro- 证明了指针逻辑相对PointerC的操作语义是可 gramming language specification.University of Science and 靠的. Technology of China:Technical Report TR-1001-06.2006 我们正在研究放宽对PointerC指针运算的限 [13]Necula G C.MePeak S,Weimer W.CCured:Type-safe ret- 制，有限制地允许指针算术，以适应编程中经常使用 rofitting of legacy code//Proceedings of the 29th Annual 的calloc存储分配等.加上面向对象的语言构造，使 ACM Symposium on Principles of Programming Languages. New York.NY:ACM Press.2002:128-139 程序性质证明具有更好的模块性将是进一步研究的 [14]Jim T.Morrisett JG.Grossman D.Hicks M W,Cheney J. 内容. Wang Y.Cyclone:A safe dialect of C//Proceedings of the General Track:2002 USENIX Annual Technical Conference. 参考文献 Berkeley:USENIX Association.2002:275-288 [15]Hua B J.Chen YY.Li Z P.The pointer logic soundness proof and PointerC safety proof.University of Science and [1]CNCERT/CC.2006 Annual report.Available at http:// Technology of China:Technical Report TR-1101-07.2007 www.cert.org.cn/articles/docs/common/2007042923284. [16]The Cog development team.The Cog proof assistant refer- shtml ence manual Version8.0.Paris.France.2004 [2]Galen Hunt.James Larus.Singularity:Rethinking the soft- [17]Ge Lin.Chen Yi-Yun.Hua Bao-Jian.Li Zhao-Peng,Liu ware stack.Operating Systems Review,2007.41(2):37-49 Cheng.Automatic generation of formal specifications in as- [3]Mandelbaum Y.Walker D.Harper R.An effective theory of sembly code certification.Mini-Macro Systems,to appear(in type refinements//Proceedings of the 8th ACM SIGPLAN Chinese) International Conference on Functional Programming.Upp- (葛琳，陈意云，华保健，李兆翦，刘诚.汇编代码验证中的形 sala,Sweden,2003:213-225 式规范自动生成.小型微型计算机系统，已录用) [4]Xi H.Imperative programming with dependent types//Pro- [18]Flanagan C.Leino K R M.Lillibridge M.Nelson G.Saxe J ceedings of the 15th IEEE Symposium on Logic in Computer B.Stata R.Extended static checking for java//Proceedings Science.Washington.DC:IEEE Computer Society.2000: of the ACM SIGPLAN 2002 Conference on Programming 375-387 Language Design and Implementation (PLDI'2002).New [5]Xi H.Pfenning F.Dependent types in practical program- York:ACM Press,2002:234-245 ming//Proceedings of the 26th ACM SIGPLAN-SIGACT [19]Barnett M.Leino K R M,Schulte W.The Spec#program- Symposium on Principles of Programming Languages.San ming system:An overview//Proceedings of the CASSIS'04. Antonio.Texas,USA.1999:214-227 LNCS 3362.Marseille,France.2005:49-69 [6]Xi H W.Applied type system (extended abstract)//Post- [20]Filliatre J-C.Marche C.Multi-prover verification of C pro- Workshop Proceedings of the TYPES 2003.Lecture Notes in grams//Proceedings of the ICFEM.LNCS 3308.Seattle. Computer Science 3085.Berlin:Springer-Verlag.2004: USA,2004:15-29 394-408 [21]Sandrine Blazy.Zaynah Dargaye.Xavier Leroy.Formal veri- [7]Smith F.Walker D.Morrisett J G.Alias types//Proceed- fication of a C compiler front-end//Proceedings of the Sympo- ings of the 9th European Symposium on Programming Lan- sium on Formal Methods (FM'06).LNCS 4805.Hamilton. guages and Systems.Lecture Notes in Computer Science Canada,2006:460-475
制，适合验证更实际的指针程序． ５ 结论和进一步的工作 本文在系统级安全语言设计和实现以及性质证 明方面做了有益尝试．我们采用一种类型系统和逻 辑系统相结合的静态机制保证语言的安全性．为了 考察这种机制的实际可行性，我们设计了一个类 Ｃ 的命令式语言 ＰｏｉｎｔｅｒＣ，它的新颖之处在于定型规 则中包括副条件断言．基于形式定义的安全策略，本 文证明定理 ＰｏｉｎｔｅｒＣ的安全性．为了静态推理指针 类型的断言，我们在前期工作中提出了指针逻辑，以 解决 Ｈｏａｒｅ逻辑处理别名问题所面临的困难．本文 证明了 指 针 逻 辑 相 对 ＰｏｉｎｔｅｒＣ 的 操 作 语 义 是 可 靠的． 我们正在研究放宽对 ＰｏｉｎｔｅｒＣ 指针运算的限 制，有限制地允许指针算术，以适应编程中经常使用 的ｃａｌｌｏｃ存储分配等．加上面向对象的语言构造，使 程序性质证明具有更好的模块性将是进一步研究的 内容． 参 考 文 献 ［１］ ＣＮＣＥＲＴ／ＣＣ．２００６ Ａｎｎｕａｌｒｅｐｏｒｔ．Ａｖａｉｌａｂｌｅａｔｈｔｔｐ：／／ ｗｗｗ．ｃｅｒｔ．ｏｒｇ．ｃｎ／ａｒｔｉｃｌｅｓ／ｄｏｃｓ／ｃｏｍｍｏｎ／２００７０４２９２３２８４． ｓｈｔｍｌ ［２］ ＧａｌｅｎＨｕｎｔ，ＪａｍｅｓＬａｒｕｓ．Ｓｉｎｇｕｌａｒｉｔｙ：Ｒｅｔｈｉｎｋｉｎｇｔｈｅｓｏｆｔ ｗａｒｅｓｔａｃｋ．ＯｐｅｒａｔｉｎｇＳｙｓｔｅｍｓＲｅｖｉｅｗ，２００７，４１（２）：３７４９ ［３］ Ｍａｎｄｅｌｂａｕｍ Ｙ，ＷａｌｋｅｒＤ，ＨａｒｐｅｒＲ．Ａｎｅｆｆｅｃｔｉｖｅｔｈｅｏｒｙｏｆ ｔｙｐｅｒｅｆｉｎｅｍｅｎｔｓ／／Ｐｒｏｃｅｅｄｉｎｇｓｏｆｔｈｅ８ｔｈ ＡＣＭ ＳＩＧＰＬＡＮ ＩｎｔｅｒｎａｔｉｏｎａｌＣｏｎｆｅｒｅｎｃｅｏｎＦｕｎｃｔｉｏｎａｌＰｒｏｇｒａｍｍｉｎｇ．Ｕｐｐ ｓａｌａ，Ｓｗｅｄｅｎ，２００３：２１３２２５ ［４］ ＸｉＨ．Ｉｍｐｅｒａｔｉｖｅｐｒｏｇｒａｍｍｉｎｇｗｉｔｈｄｅｐｅｎｄｅｎｔｔｙｐｅｓ／／Ｐｒｏ ｃｅｅｄｉｎｇｓｏｆｔｈｅ１５ｔｈＩＥＥＥＳｙｍｐｏｓｉｕｍｏｎＬｏｇｉｃｉｎＣｏｍｐｕｔｅｒ Ｓｃｉｅｎｃｅ．Ｗａｓｈｉｎｇｔｏｎ，ＤＣ：ＩＥＥＥ ＣｏｍｐｕｔｅｒＳｏｃｉｅｔｙ，２０００： ３７５３８７ ［５］ ＸｉＨ，ＰｆｅｎｎｉｎｇＦ．Ｄｅｐｅｎｄｅｎｔｔｙｐｅｓｉｎｐｒａｃｔｉｃａｌｐｒｏｇｒａｍ ｍｉｎｇ／／Ｐｒｏｃｅｅｄｉｎｇｓｏｆｔｈｅ ２６ｔｈ ＡＣＭ ＳＩＧＰＬＡＮＳＩＧＡＣＴ Ｓｙｍｐｏｓｉｕｍ ｏｎ ＰｒｉｎｃｉｐｌｅｓｏｆＰｒｏｇｒａｍｍｉｎｇ Ｌａｎｇｕａｇｅｓ．Ｓａｎ Ａｎｔｏｎｉｏ，Ｔｅｘａｓ，ＵＳＡ，１９９９：２１４２２７ ［６］ ＸｉＨ Ｗ．Ａｐｐｌｉｅｄｔｙｐｅｓｙｓｔｅｍ （ｅｘｔｅｎｄｅｄａｂｓｔｒａｃｔ）／／Ｐｏｓｔ ＷｏｒｋｓｈｏｐＰｒｏｃｅｅｄｉｎｇｓｏｆｔｈｅＴＹＰＥＳ２００３．ＬｅｃｔｕｒｅＮｏｔｅｓｉｎ Ｃｏｍｐｕｔｅｒ Ｓｃｉｅｎｃｅ ３０８５．Ｂｅｒｌｉｎ：ＳｐｒｉｎｇｅｒＶｅｒｌａｇ，２００４： ３９４４０８ ［７］ ＳｍｉｔｈＦ，ＷａｌｋｅｒＤ，ＭｏｒｒｉｓｅｔｔＪＧ．Ａｌｉａｓｔｙｐｅｓ／／Ｐｒｏｃｅｅｄ ｉｎｇｓｏｆｔｈｅ９ｔｈＥｕｒｏｐｅａｎＳｙｍｐｏｓｉｕｍｏｎＰｒｏｇｒａｍｍｉｎｇＬａｎ ｇｕａｇｅｓａｎｄ Ｓｙｓｔｅｍｓ．Ｌｅｃｔｕｒｅ Ｎｏｔｅｓｉｎ ＣｏｍｐｕｔｅｒＳｃｉｅｎｃｅ １７８２．Ｌｏｎｄｏｎ：ＳｐｒｉｎｇｅｒＶｅｒｌａｇ，２０００：３６６３８１ ［８］ ＨｏａｒｅＣ Ａ Ｒ．Ａｎａｘｉｏｍａｔｉｃｂａｓｉｓｆｏｒｃｏｍｐｕｔｅｒｐｒｏｇｒａｍ ｍｉｎｇ．ＣｏｍｍｕｎｉｃａｔｉｏｎｓｏｆｔｈｅＡＣＭ，１９６９，１２（１０）：５７６５８０ ［９］ ＮｅｃｕｌａＧ Ｃ．Ｐｒｏｏｆｃａｒｒｙｉｎｇｃｏｄｅ／／Ｐｒｏｃｅｅｄｉｎｇｓｏｆｔｈｅ２４ｔｈ ＡＣＭ ＳＩＧＰＬＡＮＳＩＧＡＣＴＳｙｍｐｏｓｉｕｍ ｏｎＰｒｉｎｃｉｐｌｅｓｏｆＰｒｏ ｇｒａｍｍｉｎｇＬａｎｇｕａｇｅｓ．Ｐａｒｉｓ，Ｆｒａｎｃｅ，１９９７：１０６１１９ ［１０］ ＣｈｅｎＹＹ，ＧｅＬ，ＨｕａＢＪ，ＬｉＺＰ，ＬｉｕＣ，ＷａｎｇＺＦ．Ａ ｐｏｉｎｔｅｒｌｏｇｉｃａｎｄｃｅｒｔｉｆｙｉｎｇｃｏｍｐｉｌｅｒ．ＦｒｏｎｔｉｅｒｓｏｆＣｏｍｐｕｔｅｒ ＳｃｉｅｎｃｅｉｎＣｈｉｎａ，２００７，１（３）：２９７３１２ ［１１］ ＣｈｅｎＹｉＹｕｎ，ＨｕａＢａｏＪｉａｎ，ＧｅＬｉｎ，ＷａｎｇＺｈｉＦａｎｇ．Ａ ｐｏｉｎｔｅｒｌｏｇｉｃｆｏｒｓａｆｅｔｙｖｅｒｉｆｉｃａｔｉｏｎｏｆｐｏｉｎｔｅｒｐｒｏｇｒａｍｓ．Ｃｈｉ ｎｅｓｅＪｏｕｒｎａｌｏｆＣｏｍｐｕｔｅｒｓ，２００８，３１（３）：３７２３８０（ｉｎＣｈｉ ｎｅｓｅ） （陈意云，华保健，葛琳，王志芳．一种用于指针程序安全性证 明的指针逻辑．计算机学报，２００８，３１（３）：３７２３８０） ［１２］ ＨｕａＢＪ，ＣｈｅｎＹ Ｙ，ＧｅＬ，ＷａｎｇＺＦ．ＴｈｅＰｏｉｎｔｅｒＣｐｒｏ ｇｒａｍｍｉｎｇｌａｎｇｕａｇｅｓｐｅｃｉｆｉｃａｔｉｏｎ．ＵｎｉｖｅｒｓｉｔｙｏｆＳｃｉｅｎｃｅａｎｄ ＴｅｃｈｎｏｌｏｇｙｏｆＣｈｉｎａ：ＴｅｃｈｎｉｃａｌＲｅｐｏｒｔＴＲ１００１０６，２００６ ［１３］ ＮｅｃｕｌａＧＣ，ＭｃＰｅａｋＳ，ＷｅｉｍｅｒＷ．ＣＣｕｒｅｄ：Ｔｙｐｅｓａｆｅｒｅｔ ｒｏｆｉｔｔｉｎｇｏｆｌｅｇａｃｙｃｏｄｅ／／Ｐｒｏｃｅｅｄｉｎｇｓｏｆｔｈｅ２９ｔｈ Ａｎｎｕａｌ ＡＣＭＳｙｍｐｏｓｉｕｍｏｎＰｒｉｎｃｉｐｌｅｓｏｆＰｒｏｇｒａｍｍｉｎｇＬａｎｇｕａｇｅｓ． ＮｅｗＹｏｒｋ，ＮＹ：ＡＣＭ Ｐｒｅｓｓ，２００２：１２８１３９ ［１４］ Ｊｉｍ Ｔ，ＭｏｒｒｉｓｅｔｔＪＧ，ＧｒｏｓｓｍａｎＤ，ＨｉｃｋｓＭ Ｗ，ＣｈｅｎｅｙＪ， ＷａｎｇＹ．Ｃｙｃｌｏｎｅ：ＡｓａｆｅｄｉａｌｅｃｔｏｆＣ／／Ｐｒｏｃｅｅｄｉｎｇｓｏｆｔｈｅ ＧｅｎｅｒａｌＴｒａｃｋ：２００２ＵＳＥＮＩＸＡｎｎｕａｌＴｅｃｈｎｉｃａｌＣｏｎｆｅｒｅｎｃｅ． Ｂｅｒｋｅｌｅｙ：ＵＳＥＮＩＸＡｓｓｏｃｉａｔｉｏｎ，２００２：２７５２８８ ［１５］ ＨｕａＢＪ，ＣｈｅｎＹ Ｙ，ＬｉＺＰ．Ｔｈｅｐｏｉｎｔｅｒｌｏｇｉｃｓｏｕｎｄｎｅｓｓ ｐｒｏｏｆａｎｄＰｏｉｎｔｅｒＣｓａｆｅｔｙｐｒｏｏｆ．ＵｎｉｖｅｒｓｉｔｙｏｆＳｃｉｅｎｃｅａｎｄ ＴｅｃｈｎｏｌｏｇｙｏｆＣｈｉｎａ：ＴｅｃｈｎｉｃａｌＲｅｐｏｒｔＴＲ１１０１０７，２００７ ［１６］ ＴｈｅＣｏｑｄｅｖｅｌｏｐｍｅｎｔｔｅａｍ．ＴｈｅＣｏｑｐｒｏｏｆａｓｓｉｓｔａｎｔｒｅｆｅｒ ｅｎｃｅｍａｎｕａｌＶｅｒｓｉｏｎ８．０．Ｐａｒｉｓ，Ｆｒａｎｃｅ，２００４ ［１７］ ＧｅＬｉｎ，Ｃｈｅｎ ＹｉＹｕｎ，ＨｕａＢａｏＪｉａｎ，ＬｉＺｈａｏＰｅｎｇ，Ｌｉｕ Ｃｈｅｎｇ．Ａｕｔｏｍａｔｉｃｇｅｎｅｒａｔｉｏｎｏｆｆｏｒｍａｌｓｐｅｃｉｆｉｃａｔｉｏｎｓｉｎａｓ ｓｅｍｂｌｙｃｏｄｅｃｅｒｔｉｆｉｃａｔｉｏｎ．ＭｉｎｉＭａｃｒｏＳｙｓｔｅｍｓ，ｔｏａｐｐｅａｒ（ｉｎ Ｃｈｉｎｅｓｅ） （葛琳，陈意云，华保健，李兆鹏，刘诚．汇编代码验证中的形 式规范自动生成．小型微型计算机系统，已录用） ［１８］ ＦｌａｎａｇａｎＣ，ＬｅｉｎｏＫＲ Ｍ，ＬｉｌｌｉｂｒｉｄｇｅＭ，ＮｅｌｓｏｎＧ，ＳａｘｅＪ Ｂ，ＳｔａｔａＲ．Ｅｘｔｅｎｄｅｄｓｔａｔｉｃｃｈｅｃｋｉｎｇｆｏｒｊａｖａ／／Ｐｒｏｃｅｅｄｉｎｇｓ ｏｆｔｈｅ ＡＣＭ ＳＩＧＰＬＡＮ ２００２ Ｃｏｎｆｅｒｅｎｃｅｏｎ Ｐｒｏｇｒａｍｍｉｎｇ ＬａｎｇｕａｇｅＤｅｓｉｇｎａｎｄＩｍｐｌｅｍｅｎｔａｔｉｏｎ（ＰＬＤＩ′２００２）．Ｎｅｗ Ｙｏｒｋ：ＡＣＭ Ｐｒｅｓｓ，２００２：２３４２４５ ［１９］ ＢａｒｎｅｔｔＭ，ＬｅｉｎｏＫＲ Ｍ，ＳｃｈｕｌｔｅＷ．ＴｈｅＳｐｅｃ＃ ｐｒｏｇｒａｍ ｍｉｎｇｓｙｓｔｅｍ：Ａｎｏｖｅｒｖｉｅｗ／／ＰｒｏｃｅｅｄｉｎｇｓｏｆｔｈｅＣＡＳＳＩＳ′０４． ＬＮＣＳ３３６２，Ｍａｒｓｅｉｌｌｅ，Ｆｒａｎｃｅ，２００５：４９６９ ［２０］ ＦｉｌｌｉｔｒｅＪＣ，ＭａｒｃｈéＣ．ＭｕｌｔｉｐｒｏｖｅｒｖｅｒｉｆｉｃａｔｉｏｎｏｆＣｐｒｏ ｇｒａｍｓ／／ＰｒｏｃｅｅｄｉｎｇｓｏｆｔｈｅＩＣＦＥＭ．ＬＮＣＳ３３０８．Ｓｅａｔｔｌｅ， ＵＳＡ，２００４：１５２９ ［２１］ ＳａｎｄｒｉｎｅＢｌａｚｙ，ＺａｙｎａｈＤａｒｇａｙｅ，ＸａｖｉｅｒＬｅｒｏｙ．Ｆｏｒｍａｌｖｅｒｉ ｆｉｃａｔｉｏｎｏｆａＣｃｏｍｐｉｌｅｒｆｒｏｎｔｅｎｄ／／ＰｒｏｃｅｅｄｉｎｇｓｏｆｔｈｅＳｙｍｐｏ ｓｉｕｍｏｎＦｏｒｍａｌＭｅｔｈｏｄｓ（ＦＭ′０６）．ＬＮＣＳ４８０５．Ｈａｍｉｌｔｏｎ， Ｃａｎａｄａ，２００６：４６０４７５ ４ 期 华保健等：安全语言 ＰｏｉｎｔｅｒＣ的设计及形式证明 ５６３
564 计 算机 学 报 2008年 HUA Bao-Jian,born in 1979,Ph.D. gies,and software safety and security. candidate.His research interests include LI Zhao-Peng.born in 1978,Ph.D.candidate.His re- program verification,program logic. search interests include program verification,software safety and software safety and security. and security,type system and theory. WANG Zhi-Fang,born in 1982.Ph.D.candidate.His research interests include software safety and security.pro- gram logic.and program verification. CHEN Yi-Yun,born in 1946,professor,Ph.D.super- GE Lin.born in 1979,Ph.D.candidate.Her research visor.His research interests include theory and implementa- interests include program verification.software safety and tion of programming languages.formal description technolo- security,and type theory and system. Background This research is supported by the National Natural Sci- research of scaling the technology of PCC to the verification ence Foundation of China Verification and Compilation of and compilation of more realistic programming languages and Software Safety.grant No.60673126),and the Intel China more practical safety policies. Research Center.These projects study the theory and meth- This paper presents their research progress on the de- od of program verification and compilation of software safety. sign and safety proof of the PointerC programming language. Program verification is an important method to improve More specifically,they have designed a C-like imperative software reliability.And axiomatic semantics and certifying language PointerC which retains explicit memory allocation compilation are also wellpopulated research fields with dec-and deallocation features.By introducing side conditions. ades of history.In the past decade.the success of Proof-Car-PointerC's type system is kept expressive yet simple.The rying Code (PCC)renews researchers'interests in program safety proof for PointerC is presented,which is based on the verification.One important reason for PCC's success is that technique of invariants.To reason PointerC programs stati- by concentrating on safety properties,instead of partial cor- cally.a pointer logic,as an extension of Hoare logic,has rectness,the safety proofs could be generated automatically been proposed in their previous work,and this paper pres- by a certifying compiler.Their research group has focused on ents the soundness proof of the pointer logic
犎犝犃犅犪狅犑犻犪狀，ｂｏｒｎｉｎ１９７９，Ｐｈ．Ｄ． ｃａｎｄｉｄａｔｅ．Ｈｉｓｒｅｓｅａｒｃｈｉｎｔｅｒｅｓｔｓｉｎｃｌｕｄｅ ｐｒｏｇｒａｍ ｖｅｒｉｆｉｃａｔｉｏｎ， ｐｒｏｇｒａｍ ｌｏｇｉｃ， ａｎｄｓｏｆｔｗａｒｅｓａｆｅｔｙａｎｄｓｅｃｕｒｉｔｙ． 犆犎犈犖犢犻犢狌狀，ｂｏｒｎｉｎ１９４６，ｐｒｏｆｅｓｓｏｒ，Ｐｈ．Ｄ．ｓｕｐｅｒ ｖｉｓｏｒ．Ｈｉｓｒｅｓｅａｒｃｈｉｎｔｅｒｅｓｔｓｉｎｃｌｕｄｅｔｈｅｏｒｙａｎｄｉｍｐｌｅｍｅｎｔａ ｔｉｏｎｏｆｐｒｏｇｒａｍｍｉｎｇｌａｎｇｕａｇｅｓ，ｆｏｒｍａｌｄｅｓｃｒｉｐｔｉｏｎｔｅｃｈｎｏｌｏ ｇｉｅｓ，ａｎｄｓｏｆｔｗａｒｅｓａｆｅｔｙａｎｄｓｅｃｕｒｉｔｙ． 犔犐犣犺犪狅犘犲狀犵，ｂｏｒｎｉｎ１９７８，Ｐｈ．Ｄ．ｃａｎｄｉｄａｔｅ．Ｈｉｓｒｅ ｓｅａｒｃｈｉｎｔｅｒｅｓｔｓｉｎｃｌｕｄｅｐｒｏｇｒａｍｖｅｒｉｆｉｃａｔｉｏｎ，ｓｏｆｔｗａｒｅｓａｆｅｔｙ ａｎｄｓｅｃｕｒｉｔｙ，ｔｙｐｅｓｙｓｔｅｍａｎｄｔｈｅｏｒｙ． 犠犃犖犌犣犺犻犉犪狀犵，ｂｏｒｎｉｎ１９８２，Ｐｈ．Ｄ．ｃａｎｄｉｄａｔｅ．Ｈｉｓ ｒｅｓｅａｒｃｈｉｎｔｅｒｅｓｔｓｉｎｃｌｕｄｅｓｏｆｔｗａｒｅｓａｆｅｔｙａｎｄｓｅｃｕｒｉｔｙ，ｐｒｏ ｇｒａｍｌｏｇｉｃ，ａｎｄｐｒｏｇｒａｍｖｅｒｉｆｉｃａｔｉｏｎ． 犌犈犔犻狀，ｂｏｒｎｉｎ１９７９，Ｐｈ．Ｄ．ｃａｎｄｉｄａｔｅ．Ｈｅｒｒｅｓｅａｒｃｈ ｉｎｔｅｒｅｓｔｓｉｎｃｌｕｄｅｐｒｏｇｒａｍ ｖｅｒｉｆｉｃａｔｉｏｎ，ｓｏｆｔｗａｒｅｓａｆｅｔｙａｎｄ ｓｅｃｕｒｉｔｙ，ａｎｄｔｙｐｅｔｈｅｏｒｙａｎｄｓｙｓｔｅｍ． 犅犪犮犽犵狉狅狌狀犱 ＴｈｉｓｒｅｓｅａｒｃｈｉｓｓｕｐｐｏｒｔｅｄｂｙｔｈｅＮａｔｉｏｎａｌＮａｔｕｒａｌＳｃｉ ｅｎｃｅＦｏｕｎｄａｔｉｏｎｏｆＣｈｉｎａ（Ｖｅｒｉｆｉｃａｔｉｏｎａｎｄ Ｃｏｍｐｉｌａｔｉｏｎｏｆ ＳｏｆｔｗａｒｅＳａｆｅｔｙ，ｇｒａｎｔＮｏ．６０６７３１２６），ａｎｄｔｈｅＩｎｔｅｌＣｈｉｎａ ＲｅｓｅａｒｃｈＣｅｎｔｅｒ．Ｔｈｅｓｅｐｒｏｊｅｃｔｓｓｔｕｄｙｔｈｅｔｈｅｏｒｙａｎｄｍｅｔｈ ｏｄｏｆｐｒｏｇｒａｍｖｅｒｉｆｉｃａｔｉｏｎａｎｄｃｏｍｐｉｌａｔｉｏｎｏｆｓｏｆｔｗａｒｅｓａｆｅｔｙ． Ｐｒｏｇｒａｍｖｅｒｉｆｉｃａｔｉｏｎｉｓａｎｉｍｐｏｒｔａｎｔｍｅｔｈｏｄｔｏｉｍｐｒｏｖｅ ｓｏｆｔｗａｒｅｒｅｌｉａｂｉｌｉｔｙ．Ａｎｄａｘｉｏｍａｔｉｃｓｅｍａｎｔｉｃｓａｎｄｃｅｒｔｉｆｙｉｎｇ ｃｏｍｐｉｌａｔｉｏｎａｒｅａｌｓｏｗｅｌｌｐｏｐｕｌａｔｅｄｒｅｓｅａｒｃｈｆｉｅｌｄｓｗｉｔｈｄｅｃ ａｄｅｓｏｆｈｉｓｔｏｒｙ．Ｉｎｔｈｅｐａｓｔｄｅｃａｄｅ，ｔｈｅｓｕｃｃｅｓｓｏｆＰｒｏｏｆＣａｒ ｒｙｉｎｇＣｏｄｅ（ＰＣＣ）ｒｅｎｅｗｓｒｅｓｅａｒｃｈｅｒｓ′ｉｎｔｅｒｅｓｔｓｉｎｐｒｏｇｒａｍ ｖｅｒｉｆｉｃａｔｉｏｎ．ＯｎｅｉｍｐｏｒｔａｎｔｒｅａｓｏｎｆｏｒＰＣＣ′ｓｓｕｃｃｅｓｓｉｓｔｈａｔ ｂｙｃｏｎｃｅｎｔｒａｔｉｎｇｏｎｓａｆｅｔｙｐｒｏｐｅｒｔｉｅｓ，ｉｎｓｔｅａｄｏｆｐａｒｔｉａｌｃｏｒ ｒｅｃｔｎｅｓｓ，ｔｈｅｓａｆｅｔｙｐｒｏｏｆｓｃｏｕｌｄｂｅｇｅｎｅｒａｔｅｄａｕｔｏｍａｔｉｃａｌｌｙ ｂｙａｃｅｒｔｉｆｙｉｎｇｃｏｍｐｉｌｅｒ．Ｔｈｅｉｒｒｅｓｅａｒｃｈｇｒｏｕｐｈａｓｆｏｃｕｓｅｄｏｎ ｒｅｓｅａｒｃｈｏｆｓｃａｌｉｎｇｔｈｅｔｅｃｈｎｏｌｏｇｙｏｆＰＣＣｔｏｔｈｅｖｅｒｉｆｉｃａｔｉｏｎ ａｎｄｃｏｍｐｉｌａｔｉｏｎｏｆｍｏｒｅｒｅａｌｉｓｔｉｃｐｒｏｇｒａｍｍｉｎｇｌａｎｇｕａｇｅｓａｎｄ ｍｏｒｅｐｒａｃｔｉｃａｌｓａｆｅｔｙｐｏｌｉｃｉｅｓ． Ｔｈｉｓｐａｐｅｒｐｒｅｓｅｎｔｓｔｈｅｉｒｒｅｓｅａｒｃｈｐｒｏｇｒｅｓｓｏｎｔｈｅｄｅ ｓｉｇｎａｎｄｓａｆｅｔｙｐｒｏｏｆｏｆｔｈｅＰｏｉｎｔｅｒＣｐｒｏｇｒａｍｍｉｎｇｌａｎｇｕａｇｅ． Ｍｏｒｅｓｐｅｃｉｆｉｃａｌｌｙ，ｔｈｅｙｈａｖｅｄｅｓｉｇｎｅｄａ Ｃｌｉｋｅｉｍｐｅｒａｔｉｖｅ ｌａｎｇｕａｇｅＰｏｉｎｔｅｒＣ ｗｈｉｃｈｒｅｔａｉｎｓｅｘｐｌｉｃｉｔｍｅｍｏｒｙａｌｌｏｃａｔｉｏｎ ａｎｄｄｅａｌｌｏｃａｔｉｏｎｆｅａｔｕｒｅｓ．Ｂｙｉｎｔｒｏｄｕｃｉｎｇｓｉｄｅｃｏｎｄｉｔｉｏｎｓ， ＰｏｉｎｔｅｒＣ′ｓｔｙｐｅｓｙｓｔｅｍｉｓｋｅｐｔｅｘｐｒｅｓｓｉｖｅｙｅｔｓｉｍｐｌｅ．Ｔｈｅ ｓａｆｅｔｙｐｒｏｏｆｆｏｒＰｏｉｎｔｅｒＣｉｓｐｒｅｓｅｎｔｅｄ，ｗｈｉｃｈｉｓｂａｓｅｄｏｎｔｈｅ ｔｅｃｈｎｉｑｕｅｏｆｉｎｖａｒｉａｎｔｓ．ＴｏｒｅａｓｏｎＰｏｉｎｔｅｒＣｐｒｏｇｒａｍｓｓｔａｔｉ ｃａｌｌｙ，ａｐｏｉｎｔｅｒｌｏｇｉｃ，ａｓａｎｅｘｔｅｎｓｉｏｎｏｆＨｏａｒｅｌｏｇｉｃ，ｈａｓ ｂｅｅｎｐｒｏｐｏｓｅｄｉｎｔｈｅｉｒｐｒｅｖｉｏｕｓｗｏｒｋ，ａｎｄｔｈｉｓｐａｐｅｒｐｒｅｓ ｅｎｔｓｔｈｅｓｏｕｎｄｎｅｓｓｐｒｏｏｆｏｆｔｈｅｐｏｉｎｔｅｒｌｏｇｉｃ． ５６４ 计 算 机 学 报 ２００８年