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

摘要：

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

关键词：类型理论、软件安全、携带证明的代码、程序验证、类型化汇编语言

所属期刊栏目：19

分类号：TP309(计算技术、计算机技术)

资助基金：the National Natural Science Foundation of China under Grant No.60673126

在线出版日期：2008-12-15（万方平台首次上网日期，不代表论文的发表时间）

页数：共8页

页码：2720-2727