郭宇等：一种构造代码安全性证明的方法 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