随着国家和社会对软件的依赖程度日益增长，软件的安全性越来越受到关注，软件的安全性主要包括saflety和security两个方面。Safety是指软件运行时不引起危险、灾难的能力，而security是指软件系统对数据和信息提供保密性、完整性、可用性、真实性保障的能力。本文的研究主要关注软件的saflety，但是软件的safety和security是有联系的，黑客通常就是利用缓冲区溢出、数组访问越界、悬空指针访问等低级的safety错误，来破坏系统和获得未经授权的控制等。因此提高salfety有助于保证security。提高safety的目标是：所有的程序错误在程序运行前被发现或者在程序运行时被温和地捕获，以保证程序不会导致不可预测的系统行为。软件安全性研究主要是探索建立一个管理安全性的健全的科学和技术基础，其中软件满足安全策略的证明方法(即程序性质证明)是研究的热点之一。程序性质证明既可以采用基于类型的方法也可以采用基于逻辑的方法，近年来还有人提出了逻辑和类型相结合的方法。然而在程序性质证明方面，现有的研究不是集中于高级语言层次就是集中于低级语言层次，而很少同时考虑高级语言和低级语言的。基于高级语言的研究易于程序员使用、且可以更早发现程序的安全问题，但是被信任计算基础(TCB)比较大，而基于低级语言的研究虽然TCB比较小但是形式大多比较复杂，难以被程序员使用从而也难以应用到实际当中。一些出具证明的编译器虽然能根据源程序信息产生其汇编代码的证明，但可证明的程序性质大都是一些源级类型系统可以表达的性质，一些复杂的性质例如值相关的性质并没有在考虑的范围内。基于上述考虑，本文设计了一种可信软件开发框架，该框架的特点是同时包含了源级和目标级的程序性质证明，并且使用出具证明编译器根据源级规范和证明自动生成目标级证明。该框架可以表达的程序性质不仅局限于类型，还可以是更复杂的程序性质，比如值相关的部分正确性。本文在该框架下主要探讨了出具证明编译的相关技术，即编译器在翻译源代码到汇编代码的同时，根据源级安全规范和证明附带生成汇编代码满足等效规范的证明，并同汇编代码一同输出。这些证明可以被底层证明检查器所检查，以证明生成的汇编代码满足安全规范。本文的工作主要基于类型化汇编语言(Typed Assembly Language)、验证汇编编程(Certified Assembly Programming)和携带证明代码(Proof-Carrying Code)等研究，采用的是类型和逻辑相结合的研究方法。本文首先介绍了国内外基于程序性质证明的软件安全的相关研究和出具证明编译的研究，然后提出了一个可信软件开发框架，随后本文着重介绍了在这个框架下的出具证明编译技术，以及一个相应的出具证明编译器的设计和实现。这些技术包括验证条件生成技术，底层代码规范(断言)的翻译和生成技术，以及底层证明的生成技术。本文还讨论了出具证明的编译特性对传统编译技术的影响。本文的主要特色和贡献为：·提出了一个可信软件开发框架。它向程序员提供源级程序性质证明接口，允许程序员提供源级规范和源程序满足规范的证明，并通过出具证明编译器产生目标程序满足等效规范的证明。对目标级证明的检查可以将代码编译器排除出系统TCB，从而提高程序可信性；而目标级证明的自动生成则减轻了程序员的负担。·改进设计了源级验证条件生成算法。该算法将证明源程序满足安全规范的问题转化为证明验证条件正确性的问题。该算法还合并了源语言定型规则中的附加条件收集，同时也考虑了生成的验证条件的化简问题。源级验证条件的证明可以使程序的安全问题尽早暴露。·设计并实现了一个出具证明编译器的原型系统，该编译器首次尝试根据源级规范和证明生成目标级规范和证明，且产生的证明包含了验证条件生成过程的证明，从而将验证条件产生器排除出系统TCB，避免了现有出具证明编译器的TCB中存在复杂的验证条件产生器的尴尬局面。而且，相比已有的出具证明编译器，该编译器可以处理更加复杂的程序性质，例如值相关的部分正确性。本文由中国国家自然科学基金资助(编号60673126)。