810 计算 乡 学 报 2007年 可以由上界闭包算子来定义，对于具体域D,属性关 序P∈P,那么等式 系组成偏序集C:(D)=〈tco(D),二)，二'表示算子 O(S[P])=O([S[P]])=O(S[[P]]) 之间的偏序，即HP∈D,p三'p→(P)Ep(P).当D 必须要成立，这就是代码迷惑的可观察语义等价性 为完全格时，能得到C也为完全格.因此，抽象解释 定理 格C就组成了具体域D的属性关系空间. 根据属性空间的定义，具体域D的属性空间由 3.2模型化迷惑空间 偏序集L(D)组成，偏序关系意味着信息的丢失，我 为形式地定义代码迷惑组成的迷惑空间，根据 们使用L,(D)上的偏序关系来反映属性的理解难度 代码迷惑非形式定义，需要刻画两个性质：与程序变 的增加，因此，可以得到代码迷惑形式的定义。 换一样需要保持程序可观察语义等价性以及属性的 定义10.代码迷惑.程序变换t是代码迷惑 理解难度增加 是指t。使得某种属性关系p∈uco(D)满足偏序关系： 首先，代码迷惑是一种特殊的程序变换，因此需 (SIP])Ep(SIT[P]), 要具有与程序变换相同的可靠性和正确性. 其中二是具体域〈D,二)上的偏序关系， (1)根据变换规则是基于语法的或是基于语义 该定义反映了代码迷惑需要满足的两个性质： 的，程序变换可以分成两类：语法变换和语义变换. 可观察语义等价和存在属性理解难度增加. 这里t:P→P来表示语法变换，它对于输入程序 3.3模型化迷惑有效性 P∈P得到变换后程序tdIP】;t:D→D表示语义 为了比较代码迷惑的有效性，需要选择比较的 变换，对于输入程序P的具体语义S[P],变换后得 度量.本文主要采用以静态程序分析结果作为评价 到语义t[SP].抽象解释是基于语义的形式化框 的基准，原因是：第一，基于语义角度的代码迷惑有 架，使用语义来给出程序变换的规范，为证明语法变 效性评估，能够比基于语法的度量更加反映程序的 换τ。对程序的变化满足规范，需要建立与满足规范 本质，而且更加接近于逆向工程者的角度；第二，具 定义的语义变换t。之间的正确性联系.为此，语法 体属性通常是不可计算的，需要得到具体属性的可 变换需要满足性质：S[tw[P]口t[S[P]门.在证明 靠保守解答，当然，不完备性使得抽象属性不能精确 程序变换的可靠性时，这是需要证明满足的性质，本 地回答具体域上的问题.基于抽象解释框架下的程 文是讨论程序变换的语义信息的变化行为，并不涉 序分析定义，下面以命题的形式给出使用语义信息 及到语法变换需要满足一定语义规范的性质，因此， 作为有效性比较的度量标准。 代码迷惑有效性比较框架不需要证明语法变换的可 一般地，迷惑的有效性比较是基于可计算的语 靠性性质。 义上的 (2)程序变换的正确性是要求程序变换在可观 命题1（迷惑的有效性）.HP∈P,3p∈uco(D), 察抽象O下具有等价性.由图1，对于语法变换x, 如果关系S,IP]ES,IrIP]成立，则称变换t针 变换后的程序[P]的具体语义为Sx[P];对于 对分析算法9是有效的.上界闭包算子P是伽罗瓦 语义变换t,基于程序P的具体语义SP],经过语 联系的等效描述，当实例化为对程序分析框架时，9 义变换后得到具体语义t.[S[PI门；加上程序P的 指代具体的分析算法， 具体语义SP],这三者之间需要满足可观察语义的 抽象解释框架下，程序的收集语义和分析语义 等价性. 分别是具体语义和抽象语义的实例化，迷惑的有效 性比较是基于收集语义或是分析语义，而有效性度 量则是由论域上的偏序关系来确定.这里的有效性 FP] S[P] 度量与代码迷惑的定义是一致的，当然，为了使得有 S SP] 效性比较框架更加具有描述力，在此基础上可以使 saP]t、 当ksP] 用与定义不一致的更加复杂的有效性度量定义， 传递定理.HP,Q∈P,SP]ESQ]→S[P] 0 g“S[Ql. 图】迷惑算法的正确性关系 证明，由伽罗瓦联系(1)，S到S“间可以建立单 即代码迷惑需要满足以下正确性定理：给定程 调的映射关系S“=a·S,由a的单调性且S[P]二可以由上界闭包算子来定义，对于具体域"，属性关 系组成偏序集!犮（"）＝〈狌犮狅（"），!狉〉，!狉表示算子 之间的偏序，即犘∈"，ρ!狉 ρρ（犘）!犮 ρ（犘）．当" 为完全格时，能得到!犮也为完全格．因此，抽象解释 格!犮就组成了具体域"的属性关系空间． ３２ 模型化迷惑空间 为形式地定义代码迷惑组成的迷惑空间，根据 代码迷惑非形式定义，需要刻画两个性质：与程序变 换一样需要保持程序可观察语义等价性以及属性的 理解难度增加． 首先，代码迷惑是一种特殊的程序变换，因此需 要具有与程序变换相同的可靠性和正确性． （１）根据变换规则是基于语法的或是基于语义 的，程序变换可以分成两类：语法变换和语义变换． 这里τ狅犫：# → # 来表示语法变换，它对于输入程序 犘∈#得到变换后程序τ狅犫 !犘"；狋狅犫：" → "表示语义 变换，对于输入程序 犘 的具体语义#!犘"，变换后得 到语义狋狅犫［#!犘"］．抽象解释是基于语义的形式化框 架，使用语义来给出程序变换的规范，为证明语法变 换τ狅犫对程序的变化满足规范，需要建立与满足规范 定义的语义变换狋狅犫 之间的正确性联系．为此，语法 变换需要满足性质：#!τ狅犫 !犘""$狋狅犫［#!犘"］．在证明 程序变换的可靠性时，这是需要证明满足的性质．本 文是讨论程序变换的语义信息的变化行为，并不涉 及到语法变换需要满足一定语义规范的性质，因此， 代码迷惑有效性比较框架不需要证明语法变换的可 靠性性质． （２）程序变换的正确性是要求程序变换在可观 察抽象%下具有等价性．由图１，对于语法变换τ狅犫， 变换后的程序τ狅犫［犘］的具体语义为#!τ狅犫!犘""；对于 语义变换狋狅犫，基于程序 犘 的具体语义#!犘"，经过语 义变换后得到具体语义狋狅犫［#!犘"］；加上程序 犘 的 具体语义#!犘"，这三者之间需要满足可观察语义的 等价性． ! !"# ! ! ! $"#!! ! # % % ! ! ' $"& !"& ! ! !"& ! ! 图 １ 迷惑算法的正确性关系 即代码迷惑需要满足以下正确性定理：给定程 序犘∈#，那么等式 %（#!犘"）＝%（狋狅犫［#!犘"］）＝%（#!τ狅犫!犘""） 必须要成立，这就是代码迷惑的可观察语义等价性 定理． 根据属性空间的定义，具体域"的属性空间由 偏序集"犮（"）组成，偏序关系意味着信息的丢失，我 们使用"犮（"）上的偏序关系来反映属性的理解难度 的增加，因此，可以得到代码迷惑形式的定义． 定义１０． 代码迷惑．程序变换τ狅犫 是代码迷惑 是指τ狅犫使得某种属性关系狆∈狌犮狅（"）满足偏序关系： 狆（#!犘"）!犮 狆（#!τ狅犫!犘""）， 其中!犮是具体域〈"，!犮〉上的偏序关系． 该定义反映了代码迷惑需要满足的两个性质： 可观察语义等价和存在属性理解难度增加． ３３ 模型化迷惑有效性 为了比较代码迷惑的有效性，需要选择比较的 度量．本文主要采用以静态程序分析结果作为评价 的基准，原因是：第一，基于语义角度的代码迷惑有 效性评估，能够比基于语法的度量更加反映程序的 本质，而且更加接近于逆向工程者的角度；第二，具 体属性通常是不可计算的，需要得到具体属性的可 靠保守解答，当然，不完备性使得抽象属性不能精确 地回答具体域上的问题．基于抽象解释框架下的程 序分析定义，下面以命题的形式给出使用语义信息 作为有效性比较的度量标准． 一般地，迷惑的有效性比较是基于可计算的语 义上的． 命题１（迷惑的有效性）．犘∈#，φ∈狌犮狅（"）， 如果关系#φ!犘"!φ #φ! τ狅犫 !犘""成立，则称变换τ狅犫针 对分析算法φ是有效的．上界闭包算子φ是伽罗瓦 联系的等效描述，当实例化为对程序分析框架时，φ 指代具体的分析算法． 抽象解释框架下，程序的收集语义和分析语义 分别是具体语义和抽象语义的实例化，迷惑的有效 性比较是基于收集语义或是分析语义，而有效性度 量则是由论域上的偏序关系来确定．这里的有效性 度量与代码迷惑的定义是一致的，当然，为了使得有 效性比较框架更加具有描述力，在此基础上可以使 用与定义不一致的更加复杂的有效性度量定义． 传递定理． 犘，犙∈#，#!犘"!犮#!犙"#犪 !犘" !犪 #犪 !犙"． 证明． 由伽罗瓦联系（１），#到#犪 间可以建立单 调的映射关系 #犪 ＝α#，由α 的单调性且 #!犘 "!犮 ８１０ 计 算 机 学 报 ２００７年