###
DOI:
Journal of Software:2008.19(10):2720-2727

一种构造代码安全性证明的方法
郭宇,陈意云,林春晓
(中国科学技术大学 计算机科学技术系,安徽 合肥 230027; 中国科学技术大学 苏州研究院 软件安全实验室,江苏 苏州 215123)
A Method for Code Safety Proof Construction
GUO Yu,CHEN Yi-Yun,LIN Chun-Xiao
()
Abstract
Chart / table
Reference
Similar Articles
Article :Browse 3637   Download 2956
Received:July 30, 2007    Revised:February 25, 2008
> 中文摘要: 提出一种构造代码安全性证明的新方法.这种方法的基本思想是,在基础逻辑中定义辅助递归函数来帮助构造证明.这种构造方法在不增加系统信任计算基础的情况下可以极大地减轻构造证明的工作量,并且减小安全性证明的规模.同时介绍了该方法在一个FPCC系统中的应用.在这个系统中使用该方法使得代码的安全性证明可以自动产生.全部工作的细节已在证明辅助工具Coq中得以实现.
Abstract:This paper proposes a new method to achieve proof construction, the basic idea of which is to construct proof with auxiliary recursive functions in the foundational logic. In this way, the workload of proof construction and the size of constructed proof can be reduced while maintaining the same trusted computing base. This paper also illustrates how to adapt this method to a type-based FPCC system, where the safety proof can be constructed automatically. All this work is implemented in the proof assistant Coq.
文章编号:     中图分类号:    文献标志码:
基金项目:Supported by the National Natural Science Foundation of China under Grant No.60673126 (国家自然科学基金) Supported by the National Natural Science Foundation of China under Grant No.60673126 (国家自然科学基金)
Foundation items:
Reference text:

郭 宇,陈意云,林春晓.一种构造代码安全性证明的方法.软件学报,2008,19(10):2720-2727

GUO Yu,CHEN Yi-Yun,LIN Chun-Xiao.A Method for Code Safety Proof Construction.Journal of Software,2008,19(10):2720-2727