一种出具证明编译器中汇编级断言和证明的生成方法

《一种出具证明编译器中汇编级断言和证明的生成方法》由会员上传分享，免费在线阅读，更多相关内容在行业资料-天天文库。

1、摘要摘要随着计算机科学的迅速发展，软件规模日益庞大。现在人们在考虑软件执行效率的I司时，也越来越关注其安全性(Safety)。高可信软件的研究致力于使用前沿的技术和工具来提高计算机软件的安伞性。程序验证是一种构建高可信软件的方法，它的原理是使用数学方法来严格证明程序行为符合其预定规范，从而保证程序的安全性。程序验证可以对源代码进行，也可以对汇编代码进行。源代码级别的验证更易于程序员的理解和参与，但是由于普通编译器的低可靠性，编译器不能保证由经过验证的源代码(CertifiedSourceCode)生成的汇编代码仍然满足预定的安全规范。汇编级别的验证虽然能保证生成的汇编代码的安全性，但

2、是如果是手工编写汇编代码、书写断言、交互式完成证明，则代价过高，开发效率低。因此一种比较理想的方法是在源代码级别进行验证，然后通过出具证明编译器(CertifyingCompiler)自动生成经过验证的汇编代码。本文首先介绍了国内外基于程序性质证明的软件安全的相关研究以及出具证明编译的研究，然后介绍笔者所参与的项目CComp的整体框架模型：CComp是一个类C语言的出具证明编译器原型，它在将带有规范标注的源代码编译成汇编代码的同时，还能产生汇编代码满足相应规范的Coq可检查证明，从而保证汇编代码的安伞性。该出具证明编泽器包括：编译器前端、源级验证条件生成器、源级自动定理证明器、汇编代

3、码生成器、汇编级断言生成器、汇编级证明生成器以及汇编级验证框架。本文的主要上作集中在后面三个部分，主要研究如何自动生成汇编代码满足规范的证明，其中包括：如何复用源级自动定理证明器产生的证明以及如何生成汇编级所特有的性质的证明。本文在已有的验证框架的荩础上提出了一种Hoare风格的汇编级验证框架，并在此框架下定义了断言语言，提出一种新的汇编级断言和证明的生成方法，实现了汇编级断言生成器和汇编级证明生成器，从而保证在同一个汇编级验证框架下，实现证明的自动生成。关键词：程序验证携带证明代码出具证明编译器汇编级验证AbstractABSTRACTAsthedevelopingofcomput

4、erscience，thescaleofsoftwareislargerandlarger．Peoplepaymoreandmoreattentiononthesafetyofsoftware．High—confidencesoftwareisworkingonnewedge-cuttingtoolsandmethodtoimprovethesafetyofcomputersoftware．Programverificationworksonhowtoprovethebehaviorofprogramsatisfiespredeterminedspecificationbyusing

5、mathematicalknowledge．Programverificationcanbedonebothonsourcecodeandassemblycode．Verifysourcecodeismucheasiertounderstand，butbecauseofthelowreliabilityofnormalcompiler,wecan’tguaranteethatassemblycodewhichiscompiledbynormalcompilerusingcertifiedsourcecodestillsatisfiesthespecification．Verifyas

6、semblycodecanensurethesafetyofassemblycode，butitisnoteasytowriteassertionandproofaboutassemblycodemanually．Sothereisaperfectmethodisthatwecanverifysourcecode，andcompilethesecodeusingcertifyingcompiler,thenwecangetcertifiedassemblycodewhichincludesbothcodeandproofofsafety．inthistheism，Iintroduce

7、somepreviousworkonProgramverificationintheareaofsoftwaresafetyandcertifyingcompiler．TheniwillintroducetheframeworkofourprogramCComp：weimplementaprototypeofcertifyingcompilerwhosesourcelanguageisClike．Thiscertifyingcompilernotonlyt