一种构造代码安全性证明的方法

• 作者: 林春晓 郭宇 陈意云
• 来源期刊: 软件学报
• 学科: 工学
• 关键词: 类型理论 软件安全 携带证明的代码 程序验证 类型化汇编语言
• 年，卷（期）: 2008,（10）
• 所属期刊栏目: 2007年中国计算机大会推荐优秀论文
• 页码范围: 2720-2727
• 页数: 8页
• 分类号: TP309
• 字数: 6561字
• 语种: 中文

摘要

提出一种构造代码安全性证明的新方法.这种方法的基本思想是,在基础逻辑中定义辅助递归函数来帮助构造证明.这种构造方法在不增加系统信任计算基础的情况下可以极大地减轻构造证明的工作量,并且减小安全性证明的规模.同时介绍了该方法在一个FPCC系统中的应用.在这个系统中使用该方法使得代码的安全性证明可以自动产生.全部工作的细节已在证明辅助工具Coq中得以实现.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	陈意云	中国科学技术大学计算机科学技术系	83	854	16.0	26.0
5	郭宇	中国科学技术大学计算机科学技术系	12	38	3.0	6.0
9	林春晓	中国科学技术大学计算机科学技术系	5	20	2.0	4.0