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-25
ISSN 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
郭宇等：一种构造代码安全性证明的方法 2721 式化地在一个底层的基础逻辑(foundational logic)中，于是推理系统的可靠性就可以用基础逻辑保证，复杂的推 理系统可以被排除出TCB.其TCB仅包括安全策略、机器模型、基础逻辑以及基础逻辑的证明检查器 随后的各种FPCC实现采用了不同的推理系统来构造代码的安全性证明例如某些实现采用类型系统，如 LTAL(low-level typed assembly language)),TALT(yped assembly language two),还有一些实现采用逻辑系统， 如CAP(certified assembly programming)s,等；此外，还有一些FPCC系统同时采用了类型与逻辑的混合系统作 为推理系统，比如OCAP(open CAP)] 1.1已有的证明构造方法 构造基础的安全性证明是PCC的关键步骤理论上，代码生产方可以产生完整的安全性证明并将其附加在 可执行代码上发送给代码消费方，代码消费方利用证明检查器来检查这个证明的正确性对于代码生产方而言， 传统的证明产生过程较为复杂与繁琐.另一方面，传统的安全性证明往往过于庞大，证明的规模远超代码，并且 证明的规模有可能会随着可执行代码长度的增长以更大的幅度增长庞大的证明将导致携带证明的代码难以 在低速的网络上传输，并且会极大地增加证明检查的开销 针对上面的问题，以往的一些FPCC的实现采取了一定的对策.例如，在一部分基于类型系统的FPCC系统 实现中，使用与安全性证明有关的类型标注(annotation)来代替完整的证明，如图I(a)所示例如LTAL系统与 TALT系统将代码的类型信息与类型推理规则附加在代码上，代码消费方接收到代码之后，使用一个Prolog风格 的解释器8，检查代码是否满足类型推理规则这种方法虽然有效地减小了代码携带的信息的规模，并降低了代 码生产方的负担，但是额外的解释器却增加了系统安全性的TCB Code Code Tactics interpreter Type info Prolog interpreter Tactics (Foundational logic) Type system (Foundational logic) Logic rules Proof checker soundness Proof checker &soundness (a)LTAL and TALT (b)CAP Fig.I Traditional FPCC 图I传统的FPCC 此外，在一些基于逻辑系统的FPCC系统实现中，使用证明策略(tactic)来编码证明.证明策略是定理证明器 中由程序员输入的面向证明目标(goa)的证明脚本语言.如图1(b)所示，CAP系统将证明策略脚本附加在代码 上，代码消费方接收到代码之后，使用证明策略解释器来重新遍历检查证明过程，然后产生完整证明并交给基础 逻辑的证明检查器来检查证明的正确与否使用证明策略来编码并构造证明，可以在一定程度上达到降低证明 复杂度的目的，且不需要信任证明策略解释器.但是这种方法无法避免产生规模庞大的证明 1.2本文的证明构造方法 在目前的FPCC研究中，基础逻辑通常使用类型化演算来表示，例如ELFo,CiC(calculus of inductive constructions)等.根据Curry-Howard同构原理，类型化演算中的类型(ype)可以用来表示逻辑系统中的命题 (proposition),类型化演算的项(term)可以用来表示逻辑系统中的证明(proo).同时，值得注意的是，a演算也可以 表示计算(computation),类型化演算中可以定义递归函数，也具有较强的计算能力， 本文介绍一种基于辅助递归函数的证明构造方式，它利用了演算中的递归函数，在不增加系统TCB的前 提下，增强了证明构造的自动化程度并有效减小了证明的规模该方法的基本思想如图2所示，首先在基础逻辑 中定义递归函数，然后使用递归函数来代替推理规则进行证明的构造，代码生产方将这些递归函数以及由递归 函数构造的证明附加在可执行代码上交付给代码消费方，代码消费方使用基础逻辑证明检查器对这些递归函 数进行计算，完成证明正确性的检查」
郭宇 等:一种构造代码安全性证明的方法 2721 式化地在一个底层的基础逻辑(foundational logic)中,于是推理系统的可靠性就可以用基础逻辑保证,复杂的推 理系统可以被排除出 TCB.其 TCB 仅包括安全策略、机器模型、基础逻辑以及基础逻辑的证明检查器. 随后的各种 FPCC 实现采用了不同的推理系统来构造代码的安全性证明.例如某些实现采用类型系统,如 LTAL(low-level typed assembly language)[3],TALT(typed assembly language two)[4];还有一些实现采用逻辑系统, 如 CAP(certified assembly programming)[5,6]等;此外,还有一些 FPCC 系统同时采用了类型与逻辑的混合系统作 为推理系统,比如 OCAP(open CAP)[7]. 1.1 已有的证明构造方法 构造基础的安全性证明是 PCC 的关键步骤.理论上,代码生产方可以产生完整的安全性证明并将其附加在 可执行代码上发送给代码消费方,代码消费方利用证明检查器来检查这个证明的正确性.对于代码生产方而言, 传统的证明产生过程较为复杂与繁琐.另一方面,传统的安全性证明往往过于庞大,证明的规模远超代码,并且 证明的规模有可能会随着可执行代码长度的增长以更大的幅度增长.庞大的证明将导致携带证明的代码难以 在低速的网络上传输,并且会极大地增加证明检查的开销. 针对上面的问题,以往的一些 FPCC 的实现采取了一定的对策.例如,在一部分基于类型系统的 FPCC 系统 实现中,使用与安全性证明有关的类型标注(annotation)来代替完整的证明,如图 1(a)所示.例如 LTAL 系统与 TALT 系统将代码的类型信息与类型推理规则附加在代码上,代码消费方接收到代码之后,使用一个 Prolog 风格 的解释器[8,9]检查代码是否满足类型推理规则.这种方法虽然有效地减小了代码携带的信息的规模,并降低了代 码生产方的负担,但是额外的解释器却增加了系统安全性的 TCB. 此外,在一些基于逻辑系统的 FPCC 系统实现中,使用证明策略(tactic)来编码证明.证明策略是定理证明器 中由程序员输入的面向证明目标(goal)的证明脚本语言.如图 1(b)所示,CAP 系统将证明策略脚本附加在代码 上,代码消费方接收到代码之后,使用证明策略解释器来重新遍历检查证明过程,然后产生完整证明并交给基础 逻辑的证明检查器来检查证明的正确与否.使用证明策略来编码并构造证明,可以在一定程度上达到降低证明 复杂度的目的,且不需要信任证明策略解释器.但是这种方法无法避免产生规模庞大的证明. 1.2 本文的证明构造方法 在目前的 FPCC 研究中,基础逻辑通常使用类型化λ演算来表示,例如 ELF[10],CiC(calculus of inductive constructions)[11]等.根据 Curry-Howard 同构原理,类型化λ演算中的类型(type)可以用来表示逻辑系统中的命题 (proposition),类型化λ演算的项(term)可以用来表示逻辑系统中的证明(proof).同时,值得注意的是,λ演算也可以 表示计算(computation),类型化λ演算中可以定义递归函数,也具有较强的计算能力. 本文介绍一种基于辅助递归函数的证明构造方式,它利用了λ演算中的递归函数,在不增加系统 TCB 的前 提下,增强了证明构造的自动化程度并有效减小了证明的规模.该方法的基本思想如图 2 所示,首先在基础逻辑 中定义递归函数,然后使用递归函数来代替推理规则进行证明的构造,代码生产方将这些递归函数以及由递归 函数构造的证明附加在可执行代码上交付给代码消费方,代码消费方使用基础逻辑证明检查器对这些递归函 数进行计算,完成证明正确性的检查. (a) LTAL and TALT (b) CAP Fig.1 Traditional FPCC 图 1 传统的 FPCC Code Prolog interpreter (Foundational logic) Proof checker Tactics Code Type info Type system & soundness (Foundational logic) Proof checker Logic rules & soundness Tactics interpreter
2722 Journal of Software软件学报ol.19,No.10.October2008 Code Proof (Foundational logic) Type system Recursive func. Proof checker soundness soundness Fig.2 FPCC built with recursive functions 图2使用递归函数构造的FPCC 因为递归函数不是独立于基础逻辑系统之外的，而是定义在基础逻辑系统之中，所以此证明构造方法具有 如下优势：()由于使用递归函数代替了部分或全部的推理规则，则证明构造过程可以（半）自动完成，从而提高 了证明构造的自动化程度，易于代码生产方产生FPCC代码.(2)利用递归函数构造的证明不会随着可执行代码 的长度增长而大幅度增长，证明检查过程中避免了操作规模庞大的证明(3)定义在基础逻辑系统之中的递归 函数不需要被信任，即不属于系统的TCB.代码消费方在检查安全性证明时，除了基础逻辑证明检查器之外，不 再需要信任额外的检查程序(4)代码携带的安全性证明仍然是严格意义上的基础的安全性证明，不局限于某 一种特定的推理系统，因此，证明可以基于多态类型系统、一阶算术逻辑系统、或者是多种由不同形式推理系 统构成的混合系统.（⑤）此方法可以与己有的证明构造方法(TALT,CAP等系统)相结合. 本文第2节使用一个简单的例子来解释此证明构造方法的步骤和原理第3节介绍此方法在一个简化的 FPCC系统中的应用.由于篇幅所限，本文只给出涉及文中内容部分的形式定义与相关定理证明的大概思路.该 FPCC系统的全部内容都己在证明辅助工具Coq中实现，完整的实现代码可以从本文的网站 (http:∥ssg.ustcsZ.edu.cn/~guoyu/proof功上下载.该方法已被应用到了垃圾收集器2]与多线程库l]的证明中第4 节简要介绍C0q代码实现与实验结论.第5节比较相关的工作，最后一节为结束语. 2利用辅助递归函数构造证明 假设一个定理的证明基于一些推理规则（定义在基础逻辑系统内部），如果由这些推理规则构成的证明可以 找到一种算法来机械地完成构造，那么可以（在基础逻辑系统内部）定义递归函数实现这一算法，然后代替原有 的推理规则来构造证明此外，递归函数关于推理规则的可靠性必须在基础逻辑系统内部被证明利用此递归函 数与其可靠性证明，我们就可以构造与原来使用推理规则构造的证明等价的证明.下面将通过一个简单的例子 来解释如何利用辅助递归函数构造证明」 2.1基于推理系统的证明构造 下面定义一个推理系统来推理一个自然数是否是斐波纳奇(Fibonacci)数： 0b1 (fibz) 1 (fibo) mPnm+lP凸(6bp) mon (fib) m+2D2,+几， Fibn 其中，m>n表示斐波纳奇数列的第m个数是n,Fbn表示n属于斐波纳奇数列.推理规则在CiC中定义为 Fib fibz:0 1 fibo:11 1fbp:(mDn)→(m+1>nz2)→(m+2)P(+n2) 1fib:(3m.mpn)→Fibn 其中，fibz,fibo,fibp与fib是Fib谓词的构造符(constructor),fibp与fib构造符是函数项.由上面推理规则可知， 命题Fb3与命题Fb8是此推理系统中的定理，其证明用项表示如下： (3,fibp fibo (fibp fibz fibo)):Fib 3 (5,(fibp fibo (fibp fibz fibo))(fibp (fibp fibz fibo)(fibp fibo (fibp fibz fibo)))):Fib 8 这里的符号(x,a)表示依赖对，即命题x.T的证明，其中a的类型是T.命题Fib34也是此推理系统的一个定理，但 此定理的证明项的规模接近1000字节.尽管这些证明项中都存在着一定冗余，但是经过优化之后其规模仍然 难以避免地随着输入数值的增加而大幅增长
2722 Journal of Software 软件学报 Vol.19, No.10, October 2008 因为递归函数不是独立于基础逻辑系统之外的,而是定义在基础逻辑系统之中,所以此证明构造方法具有 如下优势:(1) 由于使用递归函数代替了部分或全部的推理规则,则证明构造过程可以(半)自动完成,从而提高 了证明构造的自动化程度,易于代码生产方产生 FPCC 代码.(2) 利用递归函数构造的证明不会随着可执行代码 的长度增长而大幅度增长,证明检查过程中避免了操作规模庞大的证明.(3) 定义在基础逻辑系统之中的递归 函数不需要被信任,即不属于系统的 TCB.代码消费方在检查安全性证明时,除了基础逻辑证明检查器之外,不 再需要信任额外的检查程序.(4) 代码携带的安全性证明仍然是严格意义上的基础的安全性证明,不局限于某 一种特定的推理系统,因此,证明可以基于多态类型系统、一阶算术逻辑系统、或者是多种由不同形式推理系 统构成的混合系统.(5) 此方法可以与已有的证明构造方法(TALT,CAP 等系统)相结合. 本文第 2 节使用一个简单的例子来解释此证明构造方法的步骤和原理.第 3 节介绍此方法在一个简化的 FPCC 系统中的应用.由于篇幅所限,本文只给出涉及文中内容部分的形式定义与相关定理证明的大概思路.该 FPCC 系统的全部内容都已在证明辅助工具 Coq 中实现 , 完整的实现代码可以从本文的网站 (http://ssg.ustcsz.edu.cn/~guoyu/proof/)上下载.该方法已被应用到了垃圾收集器[12]与多线程库[13]的证明中.第 4 节简要介绍 Coq 代码实现与实验结论.第 5 节比较相关的工作.最后一节为结束语. 2 利用辅助递归函数构造证明 假设一个定理的证明基于一些推理规则(定义在基础逻辑系统内部),如果由这些推理规则构成的证明可以 找到一种算法来机械地完成构造,那么可以(在基础逻辑系统内部)定义递归函数实现这一算法,然后代替原有 的推理规则来构造证明.此外,递归函数关于推理规则的可靠性必须在基础逻辑系统内部被证明.利用此递归函 数与其可靠性证明,我们就可以构造与原来使用推理规则构造的证明等价的证明.下面将通过一个简单的例子 来解释如何利用辅助递归函数构造证明. 2.1 基于推理系统的证明构造 下面定义一个推理系统来推理一个自然数是否是斐波纳奇(Fibonacci)数: 1 2 1 2 1 (fibz) (fibo) (fibp) (fib) 0 1 1 1 2 Fib mn m n mn m nn n + + + 其中,m n 表示斐波纳奇数列的第 m 个数是 n,Fib n 表示 n 属于斐波纳奇数列.推理规则在 CiC 中定义为 1 2 12 Fib fibz : 0 1| fibo :1 1 | fibp : ( ) ( 1 ) ( 2) ( ) | fib : ( . ) Fib mn m n m n n mm n n →+ →+ + ∃ → 其中,fibz,fibo,fibp 与 fib 是 Fib 谓词的构造符(constructor),fibp 与 fib 构造符是λ函数项.由上面推理规则可知, 命题 Fib 3 与命题 Fib 8 是此推理系统中的定理,其证明用λ项表示如下: 〈 〉 3,fibp fibo (fibp fibz fibo) : Fib 3 〈 〉 5,(fibp fibo (fibp fibz fibo)) (fibp (fibp fibz fibo) (fibp fibo (fibp fibz fibo))) : Fib 8 这里的符号〈x,a〉表示依赖对,即命题∃x.T 的证明,其中 a 的类型是 T.命题 Fib 34 也是此推理系统的一个定理,但 此定理的证明项的规模接近 1 000 字节.尽管这些证明项中都存在着一定冗余,但是经过优化之后其规模仍然 难以避免地随着输入数值的增加而大幅增长. Fig.2 FPCC built with recursive functions 图 2 使用递归函数构造的 FPCC Proof Recursive func. & soundness Code (Foundational logic) Proof checker Type system & soundness
郭宇等：一种构造代码安全性证明的方法 2723 2.2基于递归函数的证明构造 本节闸释如何利用递归函数代替上述推理规则来构造证明.判新一个自然数是否是斐波纳奇数的存在多 种判定过程，本节给出一种简单的判定过程，在基础逻辑CiC中定义如下： firf(n)兰case n of fix g(m,n)if f(m)=n then true 10→1 else if m=0 then false else g(m-1,n) 11→1 lotherwise→f(n-l)+fn-2)isfib(n)兰g(m,n) end n)函数是取斐波纳奇数列中的第n个数：g(m,n)函数从m到0依次测试n是否属于斐波纳奇数列；isfb(n)函数 从n开始调用g(n,n)来递归测试n是否属于斐波纳奇数列，isfib(n)返回值为布尔值true或者false.此递归函数的 定义需要证明对于上面的推理规则是可靠的，在基础逻辑CC中可以证明下面的定理： 定理1.如果自然数n输入到函数isb(n)中并返回结果tue,那么Fibn一定在推理系统中存在推导.此定 理在CiC中表示为 Vn.((isfib(n)=true)->Fib n 证明：使用数学归纳法可以证得，具体细节略. ▣ 假定符号Prf!表示定理1的证明项，那么Prf的类型是n.(ifb(nm)=true)→Fibn).根据Cury- Howard同构原理，Prfr也可以被看作是一个函数项，它接受两个参数：第1个参数是自然数n,第2个参数是命 题isb(n)=tue的证明项.函数的返回结果就是Fibn的证明项. 在CC理论中，如果一个项A的类型T可以由另一个类型T'计算归约得到，那么CiC的类型系统会认为项 A的类型既可以是T,也可以是T'例如，上一小节的证明项(3，fibp fibo(fibp fibz fibo)》的类型可以是Fib3,也可 以是Fib(1+2).又如命题isfib(3)=true的证明项也是命题true=true的证明项在CiC中，表达式(ref_equal)表 示命题A=A的证明项 下面我们就可以构造出Fibn的证明项： Prf n(refl_equal true):Fib n 观察上面的证明项，isb()函数隐含在证明项的类型中，它的计算过程也隐含在证明项的类型检查过程中. 因为PrfrH的类型是一个依赖类型(dependent type),Prfre的第2个参数的类型isfib(n)=true中含有一个变量n, 它必须等于函数PrfH的第1个参数n,所以当Prfm1接受第1个参数o后，CiC的类型检查器将要求第2个 参数的类型必须为isfib(no)=true,而此时第2个参数项为(rei_equal true),于是CiC的类型检查器会计算等式左 边的isfib(no),假设计算结果等于b,那么CiC的类型检查器接下来检查(refl_equal true)的类型是否是b=ture.如 果no确实是斐波纳奇数，使得函数isfib(no)的计算结果为true,那么Prfou n,(ren_equal true)将是Fibn的证明项； 否则Prfm(refl_equal true)不是一个良类型的CiC项.例如： Prf 8(refl_equal true):Fib 8 Prf,9(refl equal true):ill-typed. 由上式可知，仅输入数值即可构造某个数n是斐波纳奇数的证明，而且构造出证明的规模固定，即递归函数 的大小加上其可靠性证明的大小 2.3讨论 利用辅助递归函数构造证明方法的关键是：定义的辅助递归函数并不是用来产生证明的工具，而是作为证 明项的一部分这样构造出的证明项是由(1)递归函数的定义；(2)递归函数的可靠性证明；(3)参数构成，递归 函数被隐藏在可靠性证明的类型中因此递归函数的计算不是发生在证明的构造期，而是被延迟到了证明的检 查期. 即使一个推理系统不存在判定过程，其局部仍然有可能存在部分的推理规则的判定过程，即其中一部分相 理规则可以使用递归函数代替.对于这种情况，本节的方法仍然适用.例如Presburger算术与集合等价判定等推 理系统都存在判定过程，因此也可以应用本节介绍的方法
郭宇 等:一种构造代码安全性证明的方法 2723 2.2 基于递归函数的证明构造 本节阐释如何利用递归函数代替上述推理规则来构造证明.判断一个自然数是否是斐波纳奇数的存在多 种判定过程,本节给出一种简单的判定过程,在基础逻辑 CiC 中定义如下: ( ) |0 1 | 1 | otherwise ( 1) ( 2) fn n fn fn −+ − fix case of end ⇒ ⇒1 ⇒ ( , ) ( ) true 0 false ( 1, ) () (,) gmn f m n m gm n isfib n g n n = = − fix if then else if then else f(n)函数是取斐波纳奇数列中的第 n 个数;g(m,n)函数从 m 到 0 依次测试 n 是否属于斐波纳奇数列;isfib(n)函数 从 n 开始调用 g(n,n)来递归测试 n 是否属于斐波纳奇数列;isfib(n)返回值为布尔值 true 或者 false.此递归函数的 定义需要证明对于上面的推理规则是可靠的,在基础逻辑 CiC 中可以证明下面的定理: 定理 1. 如果自然数 n 输入到函数 isfib(n)中并返回结果 true,那么 Fib n 一定在推理系统中存在推导.此定 理在 CiC 中表示为 ∀ =→ n isfib n n . ( ( ( ) true) Fib ) . 证明:使用数学归纳法可以证得,具体细节略. □ 假定符号 PrfTH1 表示定理 1 的证明项,那么 PrfTH1 的类型是 ∀n isfib n n . ( ( ( ) true) Fib ) = → .根据 CurryHoward 同构原理,PrfTH1 也可以被看作是一个函数项,它接受两个参数:第 1 个参数是自然数 n,第 2 个参数是命 题 isfib(n)=true 的证明项.函数的返回结果就是 Fib n 的证明项. 在 CiC 理论中,如果一个项 A 的类型 T 可以由另一个类型 T ′计算归约得到,那么 CiC 的类型系统会认为项 A 的类型既可以是 T,也可以是 T ′.例如,上一小节的证明项 〈3,fibp fibo (fibp fibz fibo)〉 的类型可以是 Fib 3,也可 以是 Fib (1+2).又如命题 isfib(3) true = 的证明项也是命题 true=true 的证明项.在 CiC 中,表达式 (refl_equal ) A 表 示命题 A=A 的证明项. 下面我们就可以构造出 Fib n 的证明项: Prf (refl_equal true) : Fib TH1 n n . 观察上面的证明项,isfib(n)函数隐含在证明项的类型中,它的计算过程也隐含在证明项的类型检查过程中. 因为 PrfTH1 的类型是一个依赖类型(dependent type),PrfTH1 的第 2 个参数的类型 isfib(n)=true 中含有一个变量 n, 它必须等于函数 PrfTH1 的第 1 个参数 n,所以当 PrfTH1 接受第 1 个参数 n0 后,CiC 的类型检查器将要求第 2 个 参数的类型必须为 isfib(n0)=true,而此时第 2 个参数项为 (refl_equal true) ,于是 CiC 的类型检查器会计算等式左 边的 isfib(n0),假设计算结果等于 b,那么 CiC 的类型检查器接下来检查(refl_equal true)的类型是否是 b=ture.如 果 n0确实是斐波纳奇数,使得函数 isfib(n0)的计算结果为 true,那么 Prf (refl_equal true) TH1 0 n 将是 Fib n0的证明项; 否则 Prf (refl_equal true) TH1 0 n 不是一个良类型的 CiC 项.例如: Prf 8 (refl_equal true) : Fib 8 Prf 9 (refl_equal true) : 1 1 ill typed − . 由上式可知,仅输入数值即可构造某个数 n 是斐波纳奇数的证明,而且构造出证明的规模固定,即递归函数 的大小加上其可靠性证明的大小. 2.3 讨 论 利用辅助递归函数构造证明方法的关键是:定义的辅助递归函数并不是用来产生证明的工具,而是作为证 明项的一部分.这样构造出的证明项是由(1) 递归函数的定义;(2) 递归函数的可靠性证明;(3) 参数构成,递归 函数被隐藏在可靠性证明的类型中.因此递归函数的计算不是发生在证明的构造期,而是被延迟到了证明的检 查期. 即使一个推理系统不存在判定过程,其局部仍然有可能存在部分的推理规则的判定过程,即其中一部分推 理规则可以使用递归函数代替.对于这种情况,本节的方法仍然适用.例如 Presburger 算术与集合等价判定等推 理系统都存在判定过程,因此也可以应用本节介绍的方法
2724 Journal of Software软件学报ol.19,No.10 October2008 3构造代码的安全性证明 本节介绍如何把利用辅助递归函数的证明构造方法应用到一个FPCC系统中，该FPCC系统采用类型系统 TALI作为推理系统TAL推理系统的基本思想是使用类型系统为指令以及指令操作数加上静态类型，通过约 束指令的操作对象来保证指令操作的安全性.如控制流安全、访问内存安全等等. TAL类型系统通常存在可判定的类型检查算法，因此可以在基础逻辑中构造一个类型检查函数并证明此 类型检查函数的可靠性，然后利用此类型检查函数来自动地进行安全性证明的构造.为了突出构造证明方法在 FPCC系统中的应用，本节给出的是一个经过简化的FPCC系统，并略去了FPCC系统中的部分定义和证明的细 节，完整的FPCC系统细节参见Coq实现代码. 3.1可执行代码与安全性证明 一个简单的机器模型如图3所示该机器模型略去了数据堆与内存操作的指令，目标机器M仅由一个代码 堆C和一个机器状态的描述S组成；代码堆C是从地址标号∫到指令i的映射；机器状态S由寄存器文件R以及 程序计数器pc组成；寄存器文件R是从寄存器名称r到数值w的映射；程序计数器pc是指向代码地址的寄存 器.目标机器在运行内存中的代码之前的状态称为初始状态，此时，寄存器文件与程序计数器全部置0，分别用 R。与pco表示.M~"M'表示机器M向前执行n(>O)步.下面定义代码的安全性与FPCC代码. (Machine) M:=(C,S) (State) S::=(R,pc) (Code heap)C :: {f→}* (Register) r::=rilral...Irs (Registers file) R:={n→w}* (Program counter)pc ::=f (Instruction) ::addu rar,r,l move rarslli ra wlbgtz rsNM... (Execution) M"M' (n is number of instruction) Fig.3 Machine model defintion 图3机器模型定义 定义1(Safety).如果加载代码C的日标机器可以一直不出错地执行下去，那么认为代码C是安全的.这是 该FPCC系统的安全策略，在CiC中表示为 Safety(C)n>0.3M'.((C,(Ro,pco))"M'). 定义2(FPCC package).FPCC代码是一个依赖对，第1个分量是可执行代码；第2个分量是机器安全运行 的证明，它的类型是一个依赖和类型(dependent sum type),在CiC中表示为 FPCC≌(C,Proof FPCC:EC.Safety(C). 3.2TAL推理系统 本节将要介绍的推理系统是一个经过简化的TAL类型系统，它只包含整型与代码指针类型，不包含多态类 型以及数据指针类型等等TAL的类型语法定义与部分推理规则如图4所示. 在TAL类型系统中，值类型t包括整数类型it与代码指针类型code(:寄存器文件类型I是从寄存器r到 值类型的映射：代码规范是从地址标号「到寄存器文件类型的映射.具有代码指针类型cod(刀的值是指向 一段指令序列的地址，而这段指令序列的前条件为厂是某个时刻寄存器文件中所有寄存器类型的集合，可以被 看作是TAL系统中的前条件(pre-condition).代码规范y是代码中所有前条件I的集合. TAL类型系统的推理规则(safe)规定了可执行代码是否安全取决于加载指令代码后的初始机器 (C,(R。,pc。)》是否是良类型的.规则(mach)规定了一个机器的良类型性需要满足3个前提条件：(1)代码堆C的 类型为代码规范平，(2)当前寄存器文件R的类型为(3)即将执行的指令序列的类型为工规则(l©)规定了R 的类型是T,当且仅当R中的所有值的类型分别对应于中的类型.规则(cdhp)的含义是C中所有指令序列的类 型分别对应于4中的T指令序列的类型规则表示为平，C卜{「}∫：C(),这部分类型规则可参考传统的TAL系 统或者Coq实现代码，这里不再赘述.TAL可靠性的证明思路是“可靠性=前进性+保持性
2724 Journal of Software 软件学报 Vol.19, No.10, October 2008 3 构造代码的安全性证明 本节介绍如何把利用辅助递归函数的证明构造方法应用到一个 FPCC 系统中.该 FPCC 系统采用类型系统 TAL[14]作为推理系统.TAL 推理系统的基本思想是使用类型系统为指令以及指令操作数加上静态类型,通过约 束指令的操作对象来保证指令操作的安全性,如控制流安全、访问内存安全等等. TAL 类型系统通常存在可判定的类型检查算法,因此可以在基础逻辑中构造一个类型检查函数并证明此 类型检查函数的可靠性,然后利用此类型检查函数来自动地进行安全性证明的构造.为了突出构造证明方法在 FPCC 系统中的应用,本节给出的是一个经过简化的 FPCC 系统,并略去了 FPCC 系统中的部分定义和证明的细 节,完整的 FPCC 系统细节参见 Coq 实现代码. 3.1 可执行代码与安全性证明 一个简单的机器模型如图 3 所示.该机器模型略去了数据堆与内存操作的指令,目标机器 M 仅由一个代码 堆 C 和一个机器状态的描述 S 组成;代码堆 C 是从地址标号 f 到指令 i 的映射;机器状态 S 由寄存器文件 R 以及 程序计数器 pc 组成;寄存器文件 R 是从寄存器名称 r 到数值 w 的映射;程序计数器 pc 是指向代码地址的寄存 器.目标机器在运行内存中的代码之前的状态称为初始状态,此时,寄存器文件与程序计数器全部置 0,分别用 R0 与 pc0 表示. n M M x ′ 表示机器 M 向前执行 n(n>0)步.下面定义代码的安全性与 FPCC 代码. 定义 1(Safety). 如果加载代码 C 的目标机器可以一直不出错地执行下去,那么认为代码 C 是安全的.这是 该 FPCC 系统的安全策略,在 CiC 中表示为 0 0 Safety( 0 . ( ( ,( ,pc )) ) . n C M C R M ) ∀> ∃ n ′ x ′ . 定义 2(FPCC package). FPCC 代码是一个依赖对,第 1 个分量是可执行代码;第 2 个分量是机器安全运行 的证明,它的类型是一个依赖和类型(dependent sum type).在 CiC 中表示为 FPCC 〈 〉 C,Proof : . Safety( ) FPCC ΣC C . 3.2 TAL推理系统 本节将要介绍的推理系统是一个经过简化的 TAL 类型系统,它只包含整型与代码指针类型,不包含多态类 型以及数据指针类型等等.TAL 的类型语法定义与部分推理规则如图 4 所示. 在 TAL 类型系统中,值类型τ包括整数类型 int 与代码指针类型 code(Γ);寄存器文件类型Γ是从寄存器 r 到 值类型τ的映射;代码规范Ψ是从地址标号 f 到寄存器文件类型Γ的映射.具有代码指针类型 code(Γ)的值是指向 一段指令序列的地址,而这段指令序列的前条件为Γ.Γ是某个时刻寄存器文件中所有寄存器类型的集合,可以被 看作是 TAL 系统中的前条件(pre-condition).代码规范Ψ是代码中所有前条件Γ的集合. TAL 类型系统的推理规则(safe)规定了可执行代码是否安全取决于加载指令代码后的初始机器 0 0 ( ,( ,pc )) C R 是否是良类型的.规则(mach)规定了一个机器的良类型性需要满足 3 个前提条件:(1) 代码堆 C 的 类型为代码规范Ψ;(2) 当前寄存器文件 R 的类型为Γ;(3) 即将执行的指令序列的类型为Γ.规则(rfile)规定了 R 的类型是Γ,当且仅当 R 中的所有值的类型分别对应于Γ中的类型.规则(cdhp)的含义是 C 中所有指令序列的类 型分别对应于Ψ中的Γ.指令序列的类型规则表示为Ψ , { } :: ( ) C C A Γ f f ,这部分类型规则可参考传统的 TAL 系 统[14]或者 Coq 实现代码,这里不再赘述.TAL 可靠性的证明思路是“可靠性=前进性+保持性”. (Machine) M ::= (C, S) (State) S ::= (R, pc) (Code heap) C ::= {f6i}* (Register) r ::= r1|r2|…|r8 (Registers file) R ::= {r6w}* (Program counter) pc ::= f (Instruction) i ::= addu rd rs rt | move rd rs|li rd w|bgtz rs, f|j f|... (Execution) n M M x ′ (n is number of instruction) Fig.3 Machine model defintion 图 3 机器模型定义
郭宇等：一种构造代码安全性证明的方法 2725 (Value type) = Int code( (Register file type) 厂 = {ri,2五-rg:ts (Code spec.) +乃 Ψ卜(C,(Rpc》 (afeCΨR:r平.Cpe:Cpg (mach) ΨSafe C 平F(C,(R,pc) r∈dom(T).平kR(r):T(r .(rfile)edom()((cdhp) ΨkR:厂 平kC Fig.4 TAL syntax and inference rules(partly) 图4TAL类型语法定义与推理规则（部分） 定理2(TAL soundness).如果一个代码堆C是良类型的，那么代码堆C满足安全策略，在CiC中表示为 tΨ.VC.(ΨSafe C)→Safety(C)). 证明：先证明前进性，再证明保持性，最后对机器执行的步长进行归纳。 ▣ 由TAL类型规则就可以证明可执行代码的良类型性，然后再根据定理3即可得到代码的安全性证明.但是 在没有基础逻辑之外的工具的情况下，构造这样的证明需要人工指导给出应用类型规则的步骤这样，最后的证 明项的规模也会随着代码的长度而大幅度增大应用本文的证明构造方法将会避免这些问题， 3.3TAL类型检查器 上一节的TAL类型系统存在可判定的类型检查算法，因此，在TAL中构造安全性证明的过程是可算法化的 根据第2节提出的方法，可以使用递归函数TALCheck来代替TAL类型规则来构造代码的安全性证 明.TALCheck函数需要两个参数：代码规范和代码C,函数的返回值是布尔值true或者false,定义如下： fix ick(Ψ，T,f,C)兰case C(f)of fix cck(Ψ，C,Ψ)兰case平Ψ'of |addu ra rr.… |g→true |move ra→… |{f→厂}U平'→ick(平，T,f,C)and cck(平，C,Ψ → end end TALCheck(,C)cck(C,)and ick(,(pco),pco,C) 这里的and表示布尔运算中的“与”运算符.TALCheck的核心内容是对指令序列进行递归检查.可以看出， TALCheck函数本身的长度固定，但是它可以检查任意大小的代码堆 由第2节可知，利用递归函数构造证明项需要递归函数的可靠性证明. 引理1.通过TALCheck函数检查的代码一定在TAL系统中是良类型的： H平.C.(TALCheck(平，C)=true)→(SafeC)) 证明：展开TALCheck函数的定义，然后对代码规范与代码C进行双重归纳 口 定理3(type checking soundness).通过TALCheck函数检查的代码一定是安全的代码： tΨ.tC.((TALCheck(Ψ，C)=true)→Safety(C)). 证明：由定理2和引理1立即可得 ▣ 3.4安全性证明的构造 本节利用上一小节得到的TALCheck函数的可靠性证明项来构造代码的安全性证明.使用Prfm表示定理 3的证明项，PrfH的类型是廿平，C.(TALCheck(平，C)=true)→Safety(C).Prf接受3个参数：第1个参数是 代码规范平，第2个参数是代码C,第3个参数是代码通过类型检查的证明项Prf函数的返回结果是Safety(C) 命题的证明项，正是代码要携带的证明项.由第2节可知，Prf函数的第3个参数可以是命题true=tue的证明 项，即(refl_equal true)).当PrfTHS接受前两个参数与C后，CiC的类型检查器就能自动地推断出第3个参数的类 型TALCheck(平，C)=true.最后可以构造代码的安全性证明项： PrfC(refl_equal true):Safety(C)
郭宇 等:一种构造代码安全性证明的方法 2725 (Value type) τ ::= Int | code(Γ) (Register file type) Γ ::= {r1:τ1,r2:τ2,…,r8:τ8} (Code spec.) Ψ {f 6 Γ}* 0 0 ( ,( ,pc )) (safe) Safe Ψ Ψ C R C A A : , { } pc :: (pc) (mach) ( ,( ,pc)) Ψ Ψ ΓΨ Γ Ψ CR C C C R AA A A dom( ). ( ) : ( ) (rfile) : r rr ΓΨ Γ Ψ Γ ∀ R R ∈ A A dom( ). , { ( )} :: ( ) (cdhp) f ff f ΨΨΨ Ψ ∀ C C C ∈ A A Fig.4 TAL syntax and inference rules (partly) 图 4 TAL 类型语法定义与推理规则(部分) 定理 2(TAL soundness). 如果一个代码堆 C 是良类型的,那么代码堆 C 满足安全策略,在 CiC 中表示为 ∀∀ → Ψ Ψ . . ( ( Safe ) Safety( ) ) C C C A . 证明:先证明前进性,再证明保持性,最后对机器执行的步长进行归纳. □ 由 TAL 类型规则就可以证明可执行代码的良类型性,然后再根据定理 3 即可得到代码的安全性证明.但是 在没有基础逻辑之外的工具的情况下,构造这样的证明需要人工指导给出应用类型规则的步骤.这样,最后的证 明项的规模也会随着代码的长度而大幅度增大.应用本文的证明构造方法将会避免这些问题. 3.3 TAL类型检查器 上一节的 TAL类型系统存在可判定的类型检查算法,因此,在 TAL中构造安全性证明的过程是可算法化的. 根据第 2 节提出的方法,可以使用递归函数 TALCheck 来代替 TAL 类型规则来构造代码的安全性证 明.TALCheck 函数需要两个参数:代码规范Ψ和代码 C ,函数的返回值是布尔值 true 或者 false,定义如下: ( , ,,) () | addu | move | ... d st d s ick f f r r r r r fix case of Ψ Γ end C C ⇒ ... ⇒ ... ⇒ ... (,, ) | true |{ } ( , , , ) ( , , ) cck f ick f cck Ψ Ψ Ψ Γ Ψ ΨΓ Ψ Ψ ′ ′ ∅ ′ ′ 6 fix case of and end C C C ⇒ ∪ ⇒ TALCheck( , ) ( , , ) ( , (pc ),pc , ) 0 0 Ψ Ψ Ψ ΨΨ CC C cck ick and 这里的 and 表示布尔运算中的“与”运算符.TALCheck 的核心内容是对指令序列进行递归检查.可以看出, TALCheck 函数本身的长度固定,但是它可以检查任意大小的代码堆. 由第 2 节可知,利用递归函数构造证明项需要递归函数的可靠性证明. 引理 1. 通过 TALCheck 函数检查的代码一定在 TAL 系统中是良类型的: ∀∀ = → Ψ ΨΨ . . ( (TALCheck( , ) true) ( Safe ) ) CC C A . 证明:展开 TALCheck 函数的定义,然后对代码规范Ψ与代码 C 进行双重归纳. □ 定理 3(type checking soundness). 通过 TALCheck 函数检查的代码一定是安全的代码: ∀∀ = → Ψ Ψ . . ( (TALCheck( , ) true) Safety( ) ) CC C . 证明:由定理 2 和引理 1 立即可得. □ 3.4 安全性证明的构造 本节利用上一小节得到的 TALCheck 函数的可靠性证明项来构造代码的安全性证明.使用 PrfTH3 表示定理 3 的证明项,PrfTH3 的类型是 ∀∀ = → Ψ Ψ . . ((TALCheck( , ) true) Safety( )) CC C .PrfTH3 接受 3 个参数:第 1 个参数是 代码规范Ψ,第 2 个参数是代码 C ,第 3 个参数是代码通过类型检查的证明项.PrfTH3函数的返回结果是 Safety( ) C 命题的证明项,正是代码要携带的证明项.由第 2 节可知,PrfTH3 函数的第 3 个参数可以是命题 true=true 的证明 项,即(refl_equal true).当 PrfTH3 接受前两个参数Ψ与 C 后,CiC 的类型检查器就能自动地推断出第 3 个参数的类 型 TALCheck( , ) true Ψ C = .最后可以构造代码的安全性证明项: Prf (refl_equal true) :Safety( ) TH3Ψ C C
2726 Journal of Software软件学报ol.19,No.10 October2008 对于任意的代码C,只有它能够通过类型检查函数的检查，上面的安全性证明项才是有效的.可以看到，上 面的证明项的规模不会跟随代码规范4和代码C的规模而增长.而且此证明项的形式与代码规范和代码C无 关，是一个固定且通用的证明项，因此代码生产方可以自动地产生携带证明的代码此安全性证明项是基础的， 即代码消费方仅使用CC类型检查器就可以检验代码的安全性. 4实现 我们在Cog中实现了一个完整的FPCC系统，包括了本文介绍的所有内容，其结构与代码量见表1.Coq实 现代码中定义了一个接近真实MPS架构的机器模型和一个较为复杂的TAL类型系统，它包括多态类型、指针 类型等等，C0q实现代码中的TL类型检查器的定义与可靠性证明也较为复杂，它涉及一个多态类型的合一算 法(unification algorithm).因此，这个FPCC系统可以用来证明实际的汇编程序 C0g针对不同方法构造出的安全性证明进行检查的资源消耗情况比较见表2.虽然递归函数本身的规模占 用的资源并不小，但是它不会再随着代码的规模而变化.与代码相关部分的证明，从规模上远小于使用传统方法 构造的证明(100：1)：虽然递归函数会在证明检查期带来一些额外的计算开销，但是检查时间上仍占有优势(5：1)， 这是因为这些计算仅涉及较少的内存操作：从证明检查期的内存占用情况来看，两者差距不大，利用递归函数构 造的证明稍小一些(3：2).当代码的规模较大时，使用传统的方法构造证明极其困难，因此也难以进行测试对比，但 是本文提出的方法构造出的证明无论是从规模上、构造难易程度上，还是从检查开销方面都具有明显的优势 Table 1 Cog implementation code Table 2 Test results of an example 表1Cog实现代码 表2 一段简单代码的安全性证明的测试数据 Module Code (Line)Definition Lemmas Machine 1095 Old proof New proof 26 24 Code Pf.Rec.Fun. Type system 8195 60 279 Proof size 84906B 766B 63627B Type checker 2155 1 28 Check-Time 5.223s 1.096s 54.339s Others 6303 124 324 Memory 34948KB 20089KB Total 18671 225 666 5相关工作比较 与本文的FPCC系统相比，Appl等人的LTAL系统多出了额外的没有经过验证的Prolog风格解释器.LTAL 的基础逻辑证明检查器是一个C语言程序，而本文中FPCC系统的证明检查器是Coq系统中的编译器.本文的 FPCC系统采用了为代码构造显式的证明项的策略，而不是简单地在代码消费方进行类型检查.这种策略的一 个优点是这些显式的基础性证明项可以与其他FPCC模块进行代码与证明的链接，从而构成了完整的可执行代 码的安全性证明 Crry等人的TALT系统中的类型系统是不可判定的，因此使用本文的证明构造方法只能进行半自动构造 证明，而无法完全自动化，而TALT采用Prolog风格解释器的优势在于对不可判定的类型系统仍然可以自动化 地进行证明构造.TALT系统采用的Prolog风格的解释器理论上也可以产生对应的证明项，从而此解释器可以被 排除出TCB.但是这样产生的证明项将庞大无比且难以检查，因而无法实际应用. Necula采用了一种Oracle-bits1s的技术来压缩证明项.Oracle-bits是一些数字的序列，它记录了在产生证明 的过程中哪些中间子目标一定是失败的(fail).这些Oracle-bits被附加在可执行代码上传输到代码消费方，代码 消费方使用同样的一个证明工具来证明代码，通过Oracle-bits使得证明器避免多余回溯搜索.研究如何将这种 证明压缩的方法与本文的方法相结合是我们未来的工作之一 6结束语 本文提出了一种利用辅助递归函数来构造代码的安全性证明的方法.此方法利用递归函数代替推理系统 中部分或全部的推理规则来构造代码的安全性证明，在不增加系统信任计算基础的前提下，可以提高证明构造 过程的自动化程度并降低证明的复杂性.此方法适用于各种FPCC系统研究如何将此证明构造方法应用在更
2726 Journal of Software 软件学报 Vol.19, No.10, October 2008 对于任意的代码 C ,只有它能够通过类型检查函数的检查,上面的安全性证明项才是有效的.可以看到,上 面的证明项的规模不会跟随代码规范Ψ和代码 C 的规模而增长.而且此证明项的形式与代码规范Ψ和代码 C 无 关,是一个固定且通用的证明项,因此代码生产方可以自动地产生携带证明的代码.此安全性证明项是基础的, 即代码消费方仅使用 CiC 类型检查器就可以检验代码的安全性. 4 实 现 我们在 Coq 中实现了一个完整的 FPCC 系统,包括了本文介绍的所有内容,其结构与代码量见表 1.Coq 实 现代码中定义了一个接近真实 MIPS 架构的机器模型和一个较为复杂的 TAL 类型系统,它包括多态类型、指针 类型等等;Coq 实现代码中的 TAL 类型检查器的定义与可靠性证明也较为复杂,它涉及一个多态类型的合一算 法(unification algorithm).因此,这个 FPCC 系统可以用来证明实际的汇编程序. Coq 针对不同方法构造出的安全性证明进行检查的资源消耗情况比较见表 2.虽然递归函数本身的规模占 用的资源并不小,但是它不会再随着代码的规模而变化.与代码相关部分的证明,从规模上远小于使用传统方法 构造的证明(100:1);虽然递归函数会在证明检查期带来一些额外的计算开销,但是检查时间上仍占有优势(5:1), 这是因为这些计算仅涉及较少的内存操作;从证明检查期的内存占用情况来看,两者差距不大,利用递归函数构 造的证明稍小一些(3:2).当代码的规模较大时,使用传统的方法构造证明极其困难,因此也难以进行测试对比,但 是本文提出的方法构造出的证明无论是从规模上、构造难易程度上,还是从检查开销方面都具有明显的优势. Table 1 Coq implementation code 表 1 Coq 实现代码 Module Code (Line) Definition Lemmas Machine 1 095 26 24 Type system 8 195 60 279 Type checker 2 155 14 28 Others 6 303 124 324 Total 18 671 225 666 Table 2 Test results of an example 表 2 一段简单代码的安全性证明的测试数据 New proof Code Pf. Rec. Fun. Proof size 84 906 B 766B 63 627 B Check-Time 5.223s 1.096s 54.339s Memory 34 948 KB 20 089 KB 5 相关工作比较 与本文的 FPCC 系统相比,Appel 等人的 LTAL 系统多出了额外的没有经过验证的 Prolog 风格解释器.LTAL 的基础逻辑证明检查器是一个 C 语言程序,而本文中 FPCC 系统的证明检查器是 Coq 系统中的编译器.本文的 FPCC 系统采用了为代码构造显式的证明项的策略,而不是简单地在代码消费方进行类型检查.这种策略的一 个优点是这些显式的基础性证明项可以与其他 FPCC 模块进行代码与证明的链接,从而构成了完整的可执行代 码的安全性证明. Crary 等人的 TALT 系统中的类型系统是不可判定的,因此使用本文的证明构造方法只能进行半自动构造 证明,而无法完全自动化,而 TALT 采用 Prolog 风格解释器的优势在于对不可判定的类型系统仍然可以自动化 地进行证明构造.TALT 系统采用的 Prolog 风格的解释器理论上也可以产生对应的证明项,从而此解释器可以被 排除出 TCB.但是这样产生的证明项将庞大无比且难以检查,因而无法实际应用. Necula 采用了一种 Oracle-bits[15]的技术来压缩证明项.Oracle-bits 是一些数字的序列,它记录了在产生证明 的过程中哪些中间子目标一定是失败的(fail).这些 Oracle-bits 被附加在可执行代码上传输到代码消费方,代码 消费方使用同样的一个证明工具来证明代码,通过 Oracle-bits 使得证明器避免多余回溯搜索.研究如何将这种 证明压缩的方法与本文的方法相结合是我们未来的工作之一. 6 结束语 本文提出了一种利用辅助递归函数来构造代码的安全性证明的方法.此方法利用递归函数代替推理系统 中部分或全部的推理规则来构造代码的安全性证明,在不增加系统信任计算基础的前提下,可以提高证明构造 过程的自动化程度并降低证明的复杂性.此方法适用于各种 FPCC 系统.研究如何将此证明构造方法应用在更 Old proof
郭宇等：一种构造代码安全性证明的新方法 2727 多的领域也是我们未来工作的一部分 References: [1]Necula G.Proof-Carrying code.In:Jones N,Lee P,eds.Proc.of the POPL'97.New York:ACM Press,1997.106-119. [2]Appel AW.Foundational proof-carrying code.In:Mairson H,ed.Proc.of the 16th Annual IEEE Symp.on Logic in Computer Science.Washington:IEEE Computer Society,2001.247-258. (3]Chen J,Wu D.Appel AW.Fang H.A provably sound tail for back-end optimization.In:Cytron R.Gupta R,eds.Proc.of the PLDI 2003.New York:ACM Press,2003.208-219. [4]Crary K.Toward a foundational typed assembly language.In:Morrisett G,ed.Proc.of the POPL 2003.New York:ACM Press, 2003.198-212. [5]Yu DC,Hamid NA,Shao Z.Building certified libraries for PCC:Dynamic storage allocation.In:Degano P,ed.Proc.of the 2003 European Symp.on Programming.LNCS 2618.Berlin:Springer-Verlag,2003. [6]Feng XY,Shao Z,Vaynberg A.Xiang S,Ni ZZ.Modular verification of assembly code with stack-based control abstractions.In: Schwartzbach M,Ball T,eds.Proc.of the PLDI 2006.New York:ACM Press,2006.401-414. [7]Feng XY,Ni ZZ,Shao Z,and Guo Y.An open framework for foundational proof-carrying code.In:Hofmann M,Felleisen M,eds Proc.of the TLDI 2007.New York:ACM Press,2007.67-78 [8]Wu D,Appel AW,Stump A.Foundational proof checkers with small witnesses.In:Sagonas K,Miller D,eds.Proc.of the PPDP 2003.New York:ACM Press,2003.264-274. [9]Crary K,Sarkar S.Foundational certified code in a metalogical framework.In:Baade F,ed.Automated Deduction.LNCS 2741, Berlin:Springer-Verlag,2003.106-120. [10]Pfenning F.Logic programming in the LF logical framework.In:Huet G,Plotkin G,eds,Logical Frameworks.Cambridge: Cambridge University Press,1991.149-181. [11]Paulin-Mohring C.Inductive definitions in the system Coq-rules and properties.In:Bezem M,Groote J,eds.Proc.of the TLCA. LNCS 664,Berlin:Springer-Verlag,1993.328-345. [12]Lin CX,Chen YY,Li L,Hua B.Garbage collector verification for proof-carrying code.Journal of Computer Science and Technology,2007,22(3y:426-437. [13]Guo Y,Jiang XY,Chen YY,Lin CX.A certified thread library for multithreaded user programs.In:Hinchkey M,He J,Sanders J, eds.Proc.of the TASE 2007.Washington:IEEE Computer Society,2007.127-136. [14]Morrisett G,Walker D,Crary K,Glew N.From system F to typed assembly language.In:Wirsing M,Nivat M,eds.Proc.of the POPL'98.New York:ACM Press,1998.85-97. [15]Necula G,Rahul S.Oracle-Based checking of untrusted software.In:Nielson H,Hankin C,Schmidt D,eds.Proc.of the POPL 2001.New York:ACM Press,2001.142-154. 郭宇(1979一)，男，河南卫辉人，博士，CCF 林春晓(1981一)，男，博士生，主要研究领域 会员，主要研究领域为程序验证，软件 为程序验证，软件安全 安全 陈意云(1946一)，男，教授，博士生导师，CC℉ 高级会员，主要研究领域为程序设计语言 的理论和实现技术，程序验证，软件安全」
郭宇 等:一种构造代码安全性证明的新方法 2727 多的领域也是我们未来工作的一部分. References: [1] Necula G. Proof-Carrying code. In: Jones N, Lee P, eds. Proc. of the POPL’97. New York: ACM Press, 1997. 106−119. [2] Appel AW. Foundational proof-carrying code. In: Mairson H, ed. Proc. of the 16th Annual IEEE Symp. on Logic in Computer Science. Washington: IEEE Computer Society, 2001. 247−258. [3] Chen J, Wu D, Appel AW, Fang H. A provably sound tail for back-end optimization. In: Cytron R, Gupta R, eds. Proc. of the PLDI 2003. New York: ACM Press, 2003. 208−219. [4] Crary K. Toward a foundational typed assembly language. In: Morrisett G, ed. Proc. of the POPL 2003. New York: ACM Press, 2003. 198−212. [5] Yu DC, Hamid NA, Shao Z. Building certified libraries for PCC: Dynamic storage allocation. In: Degano P, ed. Proc. of the 2003 European Symp. on Programming. LNCS 2618. Berlin: Springer-Verlag, 2003. [6] Feng XY, Shao Z, Vaynberg A, Xiang S, Ni ZZ. Modular verification of assembly code with stack-based control abstractions. In: Schwartzbach M, Ball T, eds. Proc. of the PLDI 2006. New York: ACM Press, 2006. 401−414. [7] Feng XY, Ni ZZ, Shao Z, and Guo Y. An open framework for foundational proof-carrying code. In: Hofmann M, Felleisen M, eds. Proc. of the TLDI 2007. New York: ACM Press, 2007. 67−78. [8] Wu D, Appel AW, Stump A. Foundational proof checkers with small witnesses. In: Sagonas K, Miller D, eds. Proc. of the PPDP 2003. New York: ACM Press, 2003. 264−274. [9] Crary K, Sarkar S. Foundational certified code in a metalogical framework. In: Baade F, ed. Automated Deduction. LNCS 2741, Berlin: Springer-Verlag, 2003. 106−120. [10] Pfenning F. Logic programming in the LF logical framework. In: Huet G, Plotkin G, eds, Logical Frameworks. Cambridge: Cambridge University Press, 1991. 149−181. [11] Paulin-Mohring C. Inductive definitions in the system Coq-rules and properties. In: Bezem M, Groote J, eds. Proc. of the TLCA. LNCS 664, Berlin: Springer-Verlag, 1993. 328−345. [12] Lin CX, Chen YY, Li L, Hua B. Garbage collector verification for proof-carrying code. Journal of Computer Science and Technology, 2007,22(3):426−437. [13] Guo Y, Jiang XY, Chen YY, Lin CX. A certified thread library for multithreaded user programs. In: Hinchkey M, He J, Sanders J, eds. Proc. of the TASE 2007. Washington: IEEE Computer Society, 2007. 127−136. [14] Morrisett G, Walker D, Crary K, Glew N. From system F to typed assembly language. In: Wirsing M, Nivat M, eds. Proc. of the POPL’98. New York: ACM Press, 1998. 85−97. [15] Necula G, Rahul S. Oracle-Based checking of untrusted software. In: Nielson H, Hankin C, Schmidt D, eds. Proc. of the POPL 2001. New York: ACM Press, 2001. 142−154. 郭宇(1979－),男,河南卫辉人,博士,CCF 会 员 , 主要研究领域为程序验证 ,软 件 安全. 林春晓(1981－),男,博士生,主要研究领域 为程序验证,软件安全. 陈意云(1946－),男,教授,博士生导师,CCF 高级会员,主要研究领域为程序设计语言 的理论和实现技术,程序验证,软件安全