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

论文摘要

在社会逐渐走入信息时代的今天,社会的各个层面,包括工业界、政府机关、学校、商业部门等,都和计算机软件等信息系统结合越来越紧密。信息系统中的任何一个环节工作失败或是遭受攻击都会带来难以预料的灾难性后果,因而软件安全的重要性与日俱增。用形式化的方法对软件进行严格推理是提高软件质量的根本途径。在众多的形式化方法中,近十年来基于程序设计语言理论和实现技术的软件安全研究引起了广泛的关注。基于语言理论的研究从程序基础出发考虑软件安全,有利于减小运算系统的受信任计算基础(TrustedComputing Base,简称TCB)。未来高安全软件设计和开发的一种行之有效的方式将是基于程序性质证明的开发框架。在这个框架中,程序设计者将软件的安全策略等描述成程序应满足的规范,连同程序一起提交给编译器:编译器生成为证明程序满足规范所需的验证条件,并且利用内嵌的定理证明器自动地或交互地证明这些验证条件;编译器在把源程序翻译成目标代码的同时,将源程序满足规范的证明翻译成目标代码满足等效规范的证明,这样的编译器称为出具证明的编译器(certifyingcompiler);在目标代码一级由证明检验器利用代码所携带的证明自动进行代码满足规范的检验。该框架的主要优点是,它向程序设计者提供源级而不是目标级的程序性质证明方法,以提高安全程序的开发效率,同时它将编译器、证明器等排除出受信任的计算基础,以尽量缩小系统的TCB。作为上述基于程序性质证明的软件安全长期研究工作的一个环节和组成部分,本文在指针逻辑以及基于指针逻辑的源代码性质描述和性质证明方面做了有益探索。本文首先研究了一个强调指针类型的类C的命令式语言源语言PointerC的设计并给出了它的安全性证明。PointerC语言设计的主要出发点是:已有软件安全和出具证明编译的研究大多集中在类型安全等简单安全策略上;而本文研究的高安全程序设计框架关注更实际、更丰富的安全策略,如内存安全等,因此,PointerC保留了C语言指针特性。本文给出了一种易于程序员理解的安全语言描述方式,并尝试以类型系统和逻辑系统相结合的静态机制来推理程序的安全性。本文利用辅助定理证明工具Coq,机械证明了PointerC语言的安全性定理。本文研究了一种指针逻辑系统。指针逻辑扩展了传统Hoare逻辑,并加入了新的推理规则以支持对指针操作的推理,因此指针逻辑为证明指针程序的安全性提供了可行的途径。本文给出了针逻辑系统在一个出具证明编译器原型系统中的实现,该原型证明系统包括一个验证条件生成器和定理证明器,能够根据指针逻辑的公理和推理规则,自动完成断言的生成和证明;并且,这些代码、断言和证明可以被出具证明的编译器继续翻译到目标语言级。本文利用辅助定理证明工具Coq,机械证明了指针逻辑对于操作语义的可靠性定理。本文研究了指针逻辑在面向对象语言上的应用。本文设计了一个小的面向对象语言Cool并定义了它的形式语义;Cool保留了Java语言核心的的语法元素,如类、对象、继承等。本文扩展了指针逻辑以增加对这些新语言特性的支持。除了作为通用的程序逻辑外,本文还研究了指针逻辑在静态垃圾判断方面的应用。具体的,本文研究了指针逻辑判断静态垃圾的两种典型应用:栈分配和静态垃圾判断。栈分配可以通过把对象分配到栈而不是堆上,有效的减少垃圾的产生;而静态垃圾判断可以静态判断堆上的垃圾。本文的研究工作是对基于程序性质证明的安全软件开发框架的初步探索,但本文所研究的以指针逻辑为基础的程序性质证明方法为更大规模和更实际的软件系统安全性证明提供了一条可行的途径。

论文目录

• 摘要
• Abstract
• 第1章 绪论
• 1.1 研究背景
• 1.2 基于语言理论的软件安全研究
• 1.2.1 类型系统
• 1.2.2 Hoare逻辑和程序验证
• 1.2.3 类型系统和逻辑系统相结合的方法
• 1.3 存在的问题和发展方向
• 1.4 本文概述
• 1.4.1 研究内容和主要贡献
• 1.4.2 章节安排
• 第2章 基于程序性质证明的高安全软件设计框架
• 2.1 基于程序性质证明的软件设计框架
• 2.2 源语言设计与性质证明
• 2.3 出具证明编译器与证明翻译
• 2.4 目标语言级验证框架
• 2.5 本章小节
• 第3章 源语言PointerC
• 3.1 语法
• 3.2 操作语义
• 3.2.1 抽象机器模型
• 3.2.2 操作语义规则
• 3.3 类型系统
• 3.3.1 定型规则
• 3.3.2 副条件
• 3.4 安全性定理及其证明
• 3.5 本章小结
• 3.5.1 相关工作
• 3.5.2 小结
• 第4章 指针逻辑
• 4.1 引言
• 4.2 断言语言
• 4.3 推理规则
• 4.3.1 基本运算和谓词
• 4.3.2 指针逻辑的推理规则
• 4.4 证明实例
• 4.5 指针逻辑在出具证明编译器中的实现
• 4.6 可靠性证明
• 4.7 本章小节
• 4.7.1 和相关工作的比较
• 4.7.2 小节
• 第5章 指针逻辑在面向对象语言上的应用
• 5.1 Cool:Java的一个命令式子集
• 5.2 指针逻辑
• 5.2.1 断言语言
• 5.2.2 设计动机
• 5.2.3 公理和推理规则
• 5.3 指针逻辑用于静态垃圾收集
• 5.3.1 栈分配
• 5.3.2 静态垃圾判断
• 5.4 源级指针逻辑验证系统的设计和实现
• 5.5 本章小节
• 5.5.1 与相关工作的比较
• 5.5.2 本章小节
• 第6章 结束语
• 6.1 论文工作总结
• 6.2 进一步的工作
• 参考文献
• 致谢
• 在读期间发表的学术论文与取得的研究成果