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

Assertion and Proof Generation for Assembly Code in Certifying Compiler

作　　者：张臻婷[1,2] 李兆鹏[1,2] 陈意云[1,2] 杨思敏[1,2] 庄重[1,2] 

机构地区：[1]中国科学技术大学计算机科学与技术学院,合肥230027 [2]中国科学技术大学苏州研究院,江苏苏州215123

出　　处：《小型微型计算机系统》2011年第6期1164-1169,共6页Journal of Chinese Computer Systems

基　　金：国家自然科学基金项目(90718026)资助;江苏省自然科学基金项目(BK2008181)资助

摘　　要：携带证明代码允许代码消费方通过检查代码生产方提供的证明,来判断代码是否满足相应的安全规范.本文实现了一个类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.

关 键 词：程序验证 携带证明代码 出具证明编译器 汇编级验证 

分 类 号：TP311[自动化与计算机技术—计算机软件与理论]