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 机器模型定义