| 摘要: |
| 提出一种构造代码安全性证明的新方法.这种方法的基本思想是,在基础逻辑中定义辅助递归函数来帮助构造证明.这种构造方法在不增加系统信任计算基础的情况下可以极大地减轻构造证明的工作量,并且减小安全性证明的规模.同时介绍了该方法在一个FPCC系统中的应用.在这个系统中使用该方法使得代码的安全性证明可以自动产生.全部工作的细节已在证明辅助工具Coq中得以实现. |
| 关键词: 类型理论 软件安全 携带证明的代码 程序验证 类型化汇编语言 |
| DOI： |
| 分类号: |
| 基金项目:Supported by the National Natural Science Foundation of China under Grant No.60673126 (国家自然科学基金) |
|
| A Method for Code Safety Proof Construction |
|
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. |
| Key words: type theory, software security, proof-carrying code, program verification, typed assembly language |
