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

Assertion and Proof Generation for Assembly Code in Certifying Compiler

携带证明代码允许代码消费方通过检查代码生产方提供的证明,来判断代码是否满足相应的安全规范.本文实现了一个类C语言的出具证明编译器原型,它在将带有规范标注的源代码编译成汇编代码的同时,还能产生汇编代码满足相应规范的Coq可检查证明,从而保证汇编代码的安全性.本文设计了一种Hoare风格的汇编级验证框架,并在此框架下提出并实现一种新的自动生成汇编级断言和证明的方法.

Proof-carrying code（PCC） is a technique that allows the code consumer to check whether the code is safe to execute via a formal safety proof provided by the code producer.A certifying compiler implements the technology of PCC by compiling annotated source code into low-level code and proof which can be checked by Coq.In this paper,we present a low-level verification framework following Hoare-style certification methods.Based on the framework,we give a definition of assertion language for assembly code and a feasible method to automatically generate assertions and proof for assembly code.