首页 | 本学科首页   官方微博 | 高级检索  
     

一种构造代码安全性证明的方法
引用本文:郭 宇,陈意云,林春晓. 一种构造代码安全性证明的方法[J]. 软件学报, 2008, 19(10): 2720-2727
作者姓名:郭 宇  陈意云  林春晓
作者单位:中国科学技术大学,计算机科学技术系,安徽,合肥,230027;中国科学技术大学,苏州研究院,软件安全实验室,江苏,苏州,215123
摘    要:提出一种构造代码安全性证明的新方法.这种方法的基本思想是,在基础逻辑中定义辅助递归函数来帮助构造证明.这种构造方法在不增加系统信任计算基础的情况下可以极大地减轻构造证明的工作量,并且减小安全性证明的规模同时介绍了该方法在一个FPCC系统中的应用.在这个系统中使用该方法使得代码的安全性证明可以自动产生.全部工作的细节已在证明辅助工具Coq中得以实现.

关 键 词:类型理论  软件安全  携带证明的代码  程序验证  类型化汇编语言
收稿时间:2007-07-30
修稿时间:2008-02-25

A Method for Code Safety Proof Construction
GUO Yu,CHEN Yi-Yun and LIN Chun-Xiao. A Method for Code Safety Proof Construction[J]. Journal of Software, 2008, 19(10): 2720-2727
Authors:GUO Yu  CHEN Yi-Yun  LIN Chun-Xiao
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.
Keywords:type theory  software security  proof-carrying code  program verification  typed assembly language
本文献已被 CNKI 维普 万方数据 等数据库收录!
点击此处可从《软件学报》浏览原始摘要信息
点击此处可从《软件学报》下载全文
设为首页 | 免责声明 | 关于勤云 | 加入收藏

Copyright©北京勤云科技发展有限公司  京ICP备09084417号