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