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

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