随着计算机科学的迅速发展,软件规模日益庞大。现在人们在考虑软件执行效率的同时,也越来越关注其安全性(Safety)。高可信软件的研究致力于使用前沿的技术和工具来提高计算机软件的安全性。程序验证是一种构建高可信软件的方法,它的原理是使用数学方法来严格证明程序行为符合其预定规范,从而保证程序的安全性。程序验证可以对源代码进行,也可以对汇编代码进行。源代码级别的验证更易于程序员的理解和参与,但是由于普通编译器的低可靠性,编译器不能保证由经过验证的源代码(Certified Source Code)生成的汇编代码仍然满足预定的安全规范。汇编级别的验证虽然能保证生成的汇编代码的安全性,但是如果是手工编写汇编代码、书写断言、交互式完成证明,则代价过高,开发效率低。因此一种比较理想的方法是在源代码级别进行验证,然后通过集成在出具证明编译器(Certifying Compiler)中一些工具自动生成经过验证的汇编代码。本文首先介绍了国内外基于程序性质证明的软件安全的相关研究以及出具证明编译的研究,然后介绍我们的项目CComp的框架模型:我们实现了一个类C语言的出具证明编译器原型,它在将带有规范标注的源代码编译成汇编代码的同时,还能产生汇编代码满足相应规范的Coq可检查证明,从而保证汇编代码的安全性。该出具证明编译器包括:编译器前端、汇编代码生成器、源级验证条件生成器、自动定理证明器、汇编级断言生成器、汇编级证明生成器以及汇编级验证框架。本文的主要工作集中在后面三个部分,在已有的验证框架的基础上设计了一种Hoare风格的汇编级验证框架,并在此框架下定义了断言语言,并提出了一种新的汇编级断言和证明的生成方法,实现了汇编级断言生成器和汇编级证明生成器。