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

2011 6 6 小 型 微 型 计 算 机 系 统 年 月 第 期 Journal of Chinese Computer Systems Vol. 32 No． 6 2011 一种出具证明编译器中的汇编级断言和证明生成的方法 1，2 1，2 1，2 1，2 1，2 ， ， ， ， 张臻婷 李兆鹏 陈意云 杨思敏 庄 重 1 ( ， 230027 ) 中国科学技术大学计算机科学与技术学院 合肥 2 ( ， 215123) 中国科学技术大学苏州研究院 江苏苏州 E-mail :zztya@ mail． ustc． edu． cn : ， ． 摘 要 携带证明代码允许代码消费方通过检查代码生产方提供的证明 来判断代码是否满足相应的安全规范 本文实现了一 C ， ， 个类 语言的出具证明编译器原型 它在将带有规范标注的源代码编译成汇编代码的同时 还能产生汇编代码满足相应规范 Coq ， ． Hoare ， 的 可检查证明 从而保证汇编代码的安全性 本文设计了一种 风格的汇编级验证框架 并在此框架下提出并实现一 种新的自动生成汇编级断言和证明的方法． : ; ; ; 关键词 程序验证 携带证明代码 出具证明编译器 汇编级验证 中图分类号:TP311 文献标识码:A 文章编号:1000-1220 (2011)06-1164-06 Assertion and Proof Generation for Assembly Code in Certifying Compiler ZHANG Zhen-ting 1，2 ，LI Zhao -peng 1，2 ，CHEN Yi-yun1，2 ，YANG Si-min1，2 ，ZHUANG Zhong 1，2 1 (Dep artment of Comp uter Science and Technology ，Univers ity of Science and Technology of China ，Hef ei 230027 ，China) 2 (Suz hou Institute f or A dvanced Study ，Univers ity of Science and Technology of China ，Suz hou 215123 ，China) Abstract :Proof -carrying code (PCC)is a technique that allow s the code consumer to check w hether 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 w hich can be checked by Coq． In this paper ，w e present a low -level verification framew ork follow ing Hoare-style certific