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