一个出具证明编译器后端的设计与实现  

Design and Implementation of Certifying Compiler Back End

作　　者：田波[1,2] 陈意云[1,2] 王伟[1,2] 李兆鹏[1,2] 王志芳[1,2] 

机构地区：[1]中国科学技术大学计算机科学技术系,合肥230027 [2]中国科学技术大学苏州研究院软件安全实验室,苏州215123

出　　处：《计算机工程》2009年第7期132-135,共4页Computer Engineering

基　　金：国家自然科学基金资助项目(60673126;90718026);Intel中国研究中心基金资助项目

摘　　要：设计并实现一个类C语言PointerC的出具证明编译器后端。该后端采用最强后条件演算同步处理整型断言和指针断言实现整型验证条件和指针验证条件的证明,能够完全自动地产生目标级程序的指针安全性证明,处理常见递归数据结构中的非一致性别名问题。后端包括独立的定理检查器,能够检验携证明代码的完整性。This paper introduces the design and implementation of a certifying complier back end for a C-like language. PointerC. The back end adopts the strongest post-conditions calculation for both integer assertion and pointer assertion synchronously, and proofs the verification conditions involving integers and pointers. It generates the proofs of pointer safety at the assembly level full-automatically, and solves the problem of the non-uniform alias analysis in commonly used data structures. The proof checker, which checks the integrity of proof-carrying code, is included in the back end.

关 键 词：高可信软件 出具证明编译器 指针安全 汇编代码 

分 类 号：N945[自然科学总论—系统科学]