摘要: 随着计算机在各个领域中的广泛应用，计算机软件安全问题也越来越引起人们的关注。在包括金融、电力、国防等一些核心的应用领域中，由于诸如内存访问错误之类的软件安全问题而导致的损失也时有发生。基于程序设计语言的软件安全研究试图通过使用安全的程序设计语言来避免软件中可能存在的诸多隐患。使用这类安全的程序设计语言，例如Java和C#等，程序员通常能够避免在使用传统程序设计语言时经常出现的一些安全漏洞，如数组越界、悬空指针访问、内存泄漏等。然而这类安全语言的实现大都相当复杂，通常包括一个庞大的编译器，以及诸多实现各种功能的运行库和虚拟机。因此这类语言编写的程序能否安全运行就完全建立在语言实现的正确性之上。从上个世纪90年代开始，大量研究开始关注如何减小安全语言的信任基础。携带证明的代码（proof-carrying code，简称PCC）是其中最有代表性的工作，它采用形式化方法来证明程序的安全性质，并通过直接在汇编语言级别上对程序进行运行前的证明检查来排除编译器中潜在的错误对程序安全性的影响。然而，即使是这类汇编语言级的安全程序设计系统还是需要由被信任的运行库，特别是被信任的垃圾收集器，来提供诸如存储管理之类的基本支持。为了进一步提高安全语言系统的可信度，向汇编语言级的安全系统提供经过验证的垃圾收集器也就成了当前国际软件安全研究领域的热点。本文介绍了在PCC程序验证框架下验证一个保守式标记—清除垃圾收集器的正确性的过程。我们证明了垃圾收集器不破坏用户程序的数据，并且回收所有的空闲内存单元。同时，我们严格形式地描述了垃圾收集器的内部数据结构以及它与用户程序之间的接口规范；列举了垃圾收集器的汇编语言实现以及它在执行的各个阶段中需要满足的安全性质。在验证工作中，我们也对现有的PCC验证框架进行了有益的改进和扩展。我们的验证工作通过使用Coq定理证明辅助工具来完成，所有的证明都严格地使用可以由计算机检查的形式来给出。从实践过程中的经验出发，我们也发现了很多能够有效提高计算机辅助证明效率的方法。本文工作的创新和贡献在于：严格形式地描述并证明了一个实际垃圾收集器的汇编语言实现和它的运行时规范；使用计算机辅助证明工具得到了携带机器可检查的安全证明的垃圾收集器软件包；以及对现有的PCC验证框架和程序证明技术的有益改进等。通过对垃圾收集器的安全性，以至对安全程序设计框架的研究，可以提高计算机软件在包括核心领域的诸多应用中的可靠性，减少、进而避免由于计算机软件安全问题导致的各种损失，使得计算机能够更好的为社会主义现代化建设和人民生产、生活服务。