| 一种出具证明编译器中的汇编级断言和证明生成的方法 |
| |
| 引用本文： | 张臻婷,李兆鹏,陈意云,杨思敏,庄重.一种出具证明编译器中的汇编级断言和证明生成的方法[J].小型微型计算机系统,2011,32(6). |
| |
| 作者姓名： | 张臻婷 李兆鹏 陈意云 杨思敏 庄重 |
| |
| 作者单位： | 中国科学技术大学计算机科学与技术学院,合肥,230027;中国科学技术大学苏州研究院,江苏苏州,215123 |
| |
| 基金项目： | 国家自然科学基金项目(90718026)资助; 江苏省自然科学基金项目(BK2008181)资助 |
| |
| 摘 要： | 携带证明代码允许代码消费方通过检查代码生产方提供的证明,来判断代码是否满足相应的安全规范.本文实现了一个类C语言的出具证明编译器原型,它在将带有规范标注的源代码编译成汇编代码的同时,还能产生汇编代码满足相应规范的Coq可检查证明,从而保证汇编代码的安全性.本文设计了一种Hoare风格的汇编级验证框架,并在此框架下提出并实现一种新的自动生成汇编级断言和证明的方法.
|
| 关 键 词： | 程序验证 携带证明代码 出具证明编译器 汇编级验证 |
Assertion and Proof Generation for Assembly Code in Certifying Compiler |
| |
| ZHANG Zhen-ting,LI Zhao-peng,CHEN Yi-yun,YANG Si-min,ZHUANG Zhong.Assertion and Proof Generation for Assembly Code in Certifying Compiler[J].Mini-micro Systems,2011,32(6). |
| |
| Authors: | ZHANG Zhen-ting LI Zhao-peng CHEN Yi-yun YANG Si-min ZHUANG Zhong |
| |
| Affiliation: | ZHANG Zhen-ting1,2,LI Zhao-peng1,CHEN Yi-yun1,YANG Si-min1,ZHUANG Zhong1,2 1(Department of Computer Science and Technology,University of Science and Technology of China,Hefei 230027,China) 2(Suzhou Institute for Advanced Study,Suzhou 215123,China) |
| |
| Abstract: | 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... |
| |
| Keywords: | program verification proof-carrying code certifying compiler verification on assembly code |
| 本文献已被 CNKI 万方数据 等数据库收录！ |
|
