论文摘要
使用Java和C#等安全的程序设计语言编写的程序能够完全避免一些在传统程序设计语言编写的程序中经常出现的安全漏洞,从而提高软件的可靠性。然而,这类安全语言的众多安全特性都依赖于其运行环境,特别是垃圾收集机制的正确性和安全性。不幸的是,垃圾收集算法通常难于设计和正确地实现。同时,垃圾收集器和用户程序的交互过程也往往相当复杂而易出错。因此,为了提高使用垃圾收集机制的程序设计语言的安全性和可靠性,势必需要对垃圾收集过程的安全性和正确性进行严格的研究。本文工作使用基于Hoare逻辑的汇编语言级形式程序验证框架,对垃圾收集器的安全性和正确性,以及垃圾收集器与多种用户程序,特别是类型化汇编语言的交互过程的安全性进行了严格的形式验证。本文工作基于携带证明的代码技术,所有的验证都在计算机辅助定理证明工具COQ中实现为计算机可检查的证明。这样,垃圾收集器和用户程序就能够被构造为一个完整的携带安全性证明的软件包,方便地通过互联网和其他渠道进行发布。本文的第一部分工作验证了两种典型垃圾收集器的汇编语言实现。该工作使用分离逻辑风格的代码规范语言给出了停止式标记—清扫垃圾收集器和基于初始快照的Yuasa渐进式垃圾收集器的安全规范,并使用Hoare风格的程序逻辑和推理方法证明了垃圾收集器满足其安全规范。第二部分工作从单独验证垃圾收集器工作存在的不足出发,提出并实现了一种通用的验证垃圾收集器和用户程序交互过程的方法。其核心思想是使用类似抽象数据类型的技术将垃圾收集器对用户程序的接口及其验证抽象起来,使得用户程序的验证无需再关心垃圾收集器的具体实现,并方便用户程序验证和垃圾收集器验证的链接。最后一部分工作研究了类型安全的垃圾收集过程。给出了一种为基础的类型化汇编语言提供验证的垃圾收集过程的方法,它基于一个开放式的汇编语言级程序逻辑,并使用了第二部分工作的主要思想,将垃圾收集器的细节从类型化汇编语言的类型系统中抽象出去,简化了类型化汇编语言的设计。同时,本文还讨论了这些工作在计算机辅助定理证明工具COQ中的实现,以及在这些实现中设计和发展的一些提高证明效率的方法和技术。本文工作的主要贡献和创新包括:1)基于汇编语言层次的一个携带证明程序的验证框架,首次成功地验证了多种垃圾收集算法的汇编级实现代码,以及它们和用户程序的交互过程;2)提出了一种基于抽象数据类型技术的通用方法,能够对垃圾收集器、用户程序以及它们的交互过程进行简洁且严格的验证;3)首次成功地解决了在最小被信任计算基础的前提下为类型化汇编语言提供类型安全的垃圾收集过程这一热点研究问题;4)基于分离逻辑技术,首次成功地从单个内存单元开始构造了标记—清扫式垃圾收集器的具体内存规范。这些研究工作对减小安全程序设计语言的被信任计算基础进行了有益的尝试——使用形式程序验证技术,携带基础证明的垃圾收集过程就可以被排除出安全程序设计语言的被信任计算基础。同时,它们也为汇编语言级程序的形式验证,特别是为携带证明的代码的技术的应用积累了重要的理论和实践经验。而随着这类技术的进步,更多被信任的软件就可以经过验证而被排除出系统的被信任计算基础。