随着软件逐渐被应用到国家、社会的更广、更深的领域中，随之而来的软件安全性问题也不容忽视。重要领域、行业的关键软件的安全性问题尤为迫切，关键软件的安全漏洞让国家和社会蒙受了巨大的损失。现有的保证软件安全的方法主要依靠软件测试，这种方法只能保证经测试的特定情状不出错，未经测试的或者无法测试的情况下的行为往往不可知。通过形式化程序的性质，并给出形式化证明的方法，被称之为形式化程序验证，这种方法是提高软件安全性的一个有效途径，且前人已经取得了丰硕的成果。 程序验证方法能够从理论上保证软件不发生程序中禁止的错误，而出具证明编译器技术结合了编译器技术和程序验证方法，它作为验证编译器的一个重要分支，在生成目标代码同时，给出目标代码对应的安全证明。出具证明编译器的出现降低了形式化程序验证的开销，它能够(半)自动地给出形式化的证明。 本实验室前期也完成了一个出具证明编译器的原型系统，但它不能够自动产生证明，这个缺陷极大的制约了其功用性和实用性，因此我们在吸取前期原型系统的经验后，重新设计的一个出具证明的编译器。新的编译器处理一个类C的PointerC语言，它保留了C语言的动态存储管理的特性，便于我们研究存储安全方面的隐患：同时我们设计了一种断言语言方便程序员书写安全规范。出具证明的编译器除了完成传统的代码编译和代码发射外，还将源级的安全规范翻译到目标级。在目标级包含一个验证系统，该验证系统中的验证条件产生器根据翻译得到的安全规范，生成程序对应的验证条件，验证条件包括整型断言和指针断言两类：其中整型断言是机器模型上变量值的约束关系谓词，指针断言是关于指针表示信息是否等价的谓词，且指针断言中的指针变量可以用整型断言中的变量来精确地描述其在堆中的偏移，能够描述更复杂的性质。目标级验证系统中还包括一个定理证明器，它能够自动地产生两种验证条件的证明：整型断言的自动证明主要借助于一个整数谓词自动证明算法和一个将目标机器模型上的寄存器变量、栈变量和堆变量范化成一种符号化变元的算法；指针断言的自动证明通过计算满足同种性质的指针的闭包集合是否等价来证明指针蕴含断言的前后件是否等价，从而得到指针断言的证明。此外我们还设计实现了一个定理检查器，它从文件中读取我们产生的携证明代码，经词法、语法分析无误的程序，进一步较验其证明和代码的合法性。这样我们不但提供了一种对产生的携证明代码机器自动检查的方法，还将编译器模块排除出信任基础，增强了系统的可信性。同时我们通过代表性的示例程序对系统可用性进行了实验评测，实验结果也在本文末尾给出。本文介绍的系统实现了一个可信计算框架，这是对程序验证的一个新的试验，其中的经验教训可作为今后完善出具证明编译器系统的借鉴。 本文由中国国家自然科学基金项目(60673126，90718026)，Intel中国研究中心资助。