【作者】 林春晓；

【导师】 陈意云；

【作者基本信息】 中国科学技术大学 ， 计算机软件与理论， 2008， 博士

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

【Abstract】 Safe programming languages such as Java and C# is capable of producing software systems that are free from some pitfalls often seen in software developed with traditional programming languages. However, all the existing safe languages rely on garbage collection mechanism for dynamic memory management. And some of their safety-related features, including the prevention of dangling pointer dereference and memory leak, are provided by garbage collection. Thus, the correctness of the underlying garbage collection is the key to the safety of these languages. Unfortunately, garbage collectors are extremely hard to implement correctly, and their interactions with mutators are often complex and error-prone. For increasing the safety of languages such as Java and C#, it is necessary to rigorously reason about the safety and correctness of garbage collection.This paper presents the Proof-Carrying Code style formal verification of two garbage collectors against their safety and correctness specifications, as well as the safe interaction between garbage collectors and various mutators, including codes constructed with Typed Assembly Language. The verification work presented is implemented as COQ proofs, and is thus machine-checkable and ready to be distributed in the form of Proof-Carrying Code.The work presented in this paper includes three major parts. The first part of work verifies two garbage collectors, namely stop-the-world mark-sweep and Yuasa incremental, against their safety and correctness specifications. The specifications, including some intricate invariants like the Weak Tri-color Invariant, are constructed using Separation-Logic style specification language. And the proof is constructed in a Hoare-style program logic.The second part of work introduces a new uniform approach to verify the safety of the interaction between mutator and garbage collector in Hoare-style program logic. Based on techniques like Abstract Data Type, this approach specifies garbage collector interfaces in an abstract way. Thus the verification of mutator is freed from reason- ing about the details of garbage collector. And the linking of the mutator verification against the verification of garbage collector is easier and more flexible.The final part of work studies the issue of type-safe garbage collection. It offers an approach of combining Typed Assembly Language with verified garbage collection. Using an open Proof-Carrying Code framework and the ideas in the second part of work, this approach successfully links the code constructed in a Typed Assembly Language with a proved conservative garbage collector, which includes showing that the collector’s interface specifications are compatible with the typing rules of the Typed Assembly Language.Besides, this paper also discusses the COQ implementation issues of the work above, and introduces some ideas and techniques for improving productivity in proof construction.The work presented in this paper may effectively reduced the Trusted Computing Base of languages like Java and C#, as well as other safe programming systems using garbage collection. And the successful verification of complex garbage collector algorithms is also a valuable experience for Proof-Carrying Code style verification.更多还原