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

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

A Method for Code Safety Proof Construction

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.