ISSN 1000-9825,CODEN RUXUEW E-mail:jos@iscas.ac.cn Journal of Sofrware,Vol.19,No.10,October 2008,pp.2720-2727 http://www.jos.org.cn D01:10.3724/SP.J.1001.2008.02720 Tel/Fax:+86-10-62562563 2008 by Journal of Software.All rights reserved. 一种构造代码安全性证明的方法 郭字2，陈意云只，林春晓口 '(中国科学技术大学计算机科学技术系，安徽合肥230027) 中因科学技术大学苏州研究院软件安全实验室，江苏苏州215123) A Method for Code Safety Proof Construction GUO Yu'2,CHEN Yi-Yun2,LIN Chun-Xiao2 "(Department of Computer Science and Technology,University of Science and Technology of China,Hefei 230027,China) (Software Security Laboratory,Suzhou Institute for Advanced Study,University of Science and Technology of China,Suzhou 215123, China) Corresponding author:E-mail:guoyu@mail.ustc.edu.cn Guo Y,Chen YY,Lin CX.A method for code safety proof construction.Journal of Software,2008, 19(10:2720-2727.http:www.jos.org.cn/1000-9825/19/2720.htm 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 摘要：提出一种构造代码安全性证明的新方法这种方法的基本思想是，在基础逻辑中定义辅助递归函数来帮 助构造证明这种构造方法在不增加系统信任计算基础的情况下可以极大地减轻构造证明的工作量，并且减小安全 性证明的规模同时介绍了该方法在一个PCC系统中的应用.在这个系统中使用该方法使得代码的安全性证明可 以自动产生.全部工作的细节已在证明辅助工具C0q中得以实现. 关键词：类型理论：软件安全，携带证明的代码：程序验证：类型化汇编语言 中图法分类号：TP309 文献标识码：A 1背景 携带证明的代码(proof-carrying code,.简称PCC)最早由Necula提出，其定义是可执行代码携带上关于自 身安全性的形式证明代码消费方不需要信任PCC代码的生产方，即可执行代码与安全性证明不再属于整个系 统安全性的信任计算基础((trusted computing base,简称TCB).随后，Appel与Felty提出了基础性携带证明的代码 (foundational proof-.carrying code,简称FPCC)的概念.FPCC的基本思想是将PCC代码与复杂的推理系统都形 ·Supported by the National Natural Science Foundation of China under Grant No.60673l26(国家自然科学基金) Received 2007-07-30;Accepted 2008-02-25ISSN 1000-9825, CODEN RUXUEW E-mail: jos@iscas.ac.cn Journal of Software, Vol.19, No.10, October 2008, pp.2720−2727 http://www.jos.org.cn DOI: 10.3724/SP.J.1001.2008.02720 Tel/Fax: +86-10-62562563 © 2008 by Journal of Software. All rights reserved. 一种构造代码安全性证明的方法∗ 郭 宇 1,2+, 陈意云 1,2, 林春晓 1,2 1 (中国科学技术大学 计算机科学技术系,安徽 合肥 230027) 2 (中国科学技术大学 苏州研究院 软件安全实验室,江苏 苏州 215123) A Method for Code Safety Proof Construction GUO Yu1,2+, CHEN Yi-Yun1,2, LIN Chun-Xiao1,2 1 (Department of Computer Science and Technology, University of Science and Technology of China, Hefei 230027, China) 2 (Software Security Laboratory, Suzhou Institute for Advanced Study, University of Science and Technology of China, Suzhou 215123, China) + Corresponding author: E-mail: guoyu@mail.ustc.edu.cn Guo Y, Chen YY, Lin CX. A method for code safety proof construction. Journal of Software, 2008, 19(10):2720−2727. http://www.jos.org.cn/1000-9825/19/2720.htm 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 摘 要: 提出一种构造代码安全性证明的新方法.这种方法的基本思想是,在基础逻辑中定义辅助递归函数来帮 助构造证明.这种构造方法在不增加系统信任计算基础的情况下可以极大地减轻构造证明的工作量,并且减小安全 性证明的规模.同时介绍了该方法在一个 FPCC 系统中的应用.在这个系统中使用该方法使得代码的安全性证明可 以自动产生.全部工作的细节已在证明辅助工具 Coq 中得以实现. 关键词: 类型理论;软件安全;携带证明的代码;程序验证;类型化汇编语言 中图法分类号: TP309 文献标识码: A 1 背 景 携带证明的代码(proof-carrying code,简称 PCC)[1]最早由 Necula 提出,其定义是可执行代码携带上关于自 身安全性的形式证明.代码消费方不需要信任 PCC 代码的生产方,即可执行代码与安全性证明不再属于整个系 统安全性的信任计算基础(trusted computing base,简称 TCB).随后,Appel 与 Felty 提出了基础性携带证明的代码 (foundational proof-carrying code,简称 FPCC)[2]的概念.FPCC 的基本思想是将 PCC 代码与复杂的推理系统都形 ∗ Supported by the National Natural Science Foundation of China under Grant No.60673126 (国家自然科学基金) Received 2007-07-30; Accepted 2008-02-25