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