郭宇等：一种构造代码安全性证明的方法 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 ) = → .根据 Curry￾Howard 同构原理,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 算术与集合等价判定等推 理系统都存在判定过程,因此也可以应用本节介绍的方法