第30卷第5期 计 算机学报 Vol.30 No.5 2007年5月 CHINESE JOURNAL OF COMPUTERS May 2007 基于抽象解释的代码迷惑有效性比较框架 鹰” 高 陈意云a ”(中国科技大学计算机科学与技术系合肥230027) )(中国科学院软件研究所计算机科学实验室北京100080) 摘要代码迷惑是一种以增加理解难度为目的的程序变换技术，用来保护软件免遭逆向剖析，代码迷惑是否有 效是代码迷惑研究中首要解决的问题.目前对有效性证明的研究大都是基于非语义的方式.文章将语义与有效性 证明联系起来，建立了基于语义的代码迷惑有效性比较框架，该框架能够为迷惑算法在静态分析这样的限定环境 下提供有效性证明，而且也能严格比较迷惑算法之间的有效性，最后使用实例描述比较框架如何应用到证明代码 迷惑的有效性. 关键词抽象解释；程序变换：程序分析：代码迷惑：压平算法 中图法分类号TP311 A Comparable Code Obfuscation Framework Measuring Efficiency Based on Abstract Interpretation GAO Ying CHEN Yi-YunD.2) (Department of Computer Science Technology.University of Science Technology of China.Hefei 230027) 2)(Laboratory of Computer Science,Institute of Software.Chinese Academy of Sciences.Beijing 100080) Abstract Code obfuscation,which is an effective program transformation,can obscure the pro- gram understanding and thus protect the program from reverse engineering.There are a lot of ap- plications about code obfuscation.This shows the efficiency of code obfuscation under some limit- ed environments.So the proving of its efficiency is the prime problem of the research.But cur- rent research takes no account of the semantic information.This paper constructs a semantics- based comparable framework measuring obfuscation efficiency,which not only prove efficiency under the limited environment of static analysis,but also can establish the formal foundation for obfuscation efficiency comparison.The last part of the paper illustrates how the framework can be applied to measure the efficiency of code obfuscation with an instantiation. Keywords abstract interpretation;program transformation;program analysis;code obfusca- tion;flattening algorithm 安全性不会受下载的客户代码的影响：另一类是恶 1引言 意主机问题，这时需要保证客户代码不会被恶意主 机窃取信息或篡改.代码迷惑是针对恶意主机问题 客户代码移动到主机执行时面临两类问题。一 而提出的一种保护客户代码的技术，它通过对代码 类是恶意客户问题，这时需要保护主机执行环境的 进行程序变换，提高变换后代码的理解难度，来达到 收稿日期：2006-02-23：修改稿收到日期：2006-06-22.本课题得到国家自然科学基金(60473068)资助.高鹰，男，1980年生，博土研究 生，主要研究方向为程序设计语言理论和实现技术、主机代码安全.E-mail:gaoying(@ustc.edu.陈意云，男，1946年生，教授，博士生导 师，主要研究领域为程序设计语言理论和实现技术，形式描述技术、软件安全等
书 第３０卷 第５期 ２００７年５月 计 算 机 学 报 ＣＨＩＮＥＳＥＪＯＵＲＮＡＬＯＦＣＯＭＰＵＴＥＲＳ Ｖｏｌ．３０ Ｎｏ．５ Ｍａｙ２００７ 收稿日期：２００６０２２３；修改稿收到日期：２００６０６２２．本课题得到国家自然科学基金（６０４７３０６８）资助．高 鹰，男，１９８０年生，博士研究 生，主要研究方向为程序设计语言理论和实现技术、主机代码安全．Ｅｍａｉｌ：ｇａｏｙｉｎｇ＠ｕｓｔｃ．ｅｄｕ．陈意云，男，１９４６年生，教授，博士生导 师，主要研究领域为程序设计语言理论和实现技术、形式描述技术、软件安全等． 基于抽象解释的代码迷惑有效性比较框架 高 鹰１） 陈意云１），２） １）（中国科技大学计算机科学与技术系 合肥 ２３００２７） ２）（中国科学院软件研究所计算机科学实验室 北京 １０００８０） 摘 要 代码迷惑是一种以增加理解难度为目的的程序变换技术，用来保护软件免遭逆向剖析．代码迷惑是否有 效是代码迷惑研究中首要解决的问题．目前对有效性证明的研究大都是基于非语义的方式．文章将语义与有效性 证明联系起来，建立了基于语义的代码迷惑有效性比较框架，该框架能够为迷惑算法在静态分析这样的限定环境 下提供有效性证明，而且也能严格比较迷惑算法之间的有效性，最后使用实例描述比较框架如何应用到证明代码 迷惑的有效性． 关键词 抽象解释；程序变换；程序分析；代码迷惑；压平算法 中图法分类号 ＴＰ３１１ 犃犆狅犿狆犪狉犪犫犾犲犆狅犱犲犗犫犳狌狊犮犪狋犻狅狀犉狉犪犿犲狑狅狉犽犕犲犪狊狌狉犻狀犵犈犳犳犻犮犻犲狀犮狔 犅犪狊犲犱狅狀犃犫狊狋狉犪犮狋犐狀狋犲狉狆狉犲狋犪狋犻狅狀 ＧＡＯＹｉｎｇ１） ＣＨＥＮ ＹｉＹｕｎ１），２） １）（犇犲狆犪狉狋犿犲狀狋狅犳犆狅犿狆狌狋犲狉犛犮犻犲狀犮犲牔 犜犲犮犺狀狅犾狅犵狔，犝狀犻狏犲狉狊犻狋狔狅犳犛犮犻犲狀犮犲牔 犜犲犮犺狀狅犾狅犵狔狅犳犆犺犻狀犪，犎犲犳犲犻 ２３００２７） ２）（犔犪犫狅狉犪狋狅狉狔狅犳犆狅犿狆狌狋犲狉犛犮犻犲狀犮犲，犐狀狊狋犻狋狌狋犲狅犳犛狅犳狋狑犪狉犲，犆犺犻狀犲狊犲犃犮犪犱犲犿狔狅犳犛犮犻犲狀犮犲狊，犅犲犻犼犻狀犵 １０００８０） 犃犫狊狋狉犪犮狋 Ｃｏｄｅｏｂｆｕｓｃａｔｉｏｎ，ｗｈｉｃｈｉｓａｎｅｆｆｅｃｔｉｖｅｐｒｏｇｒａｍｔｒａｎｓｆｏｒｍａｔｉｏｎ，ｃａｎｏｂｓｃｕｒｅｔｈｅｐｒｏ ｇｒａｍｕｎｄｅｒｓｔａｎｄｉｎｇａｎｄｔｈｕｓｐｒｏｔｅｃｔｔｈｅｐｒｏｇｒａｍｆｒｏｍｒｅｖｅｒｓｅｅｎｇｉｎｅｅｒｉｎｇ．Ｔｈｅｒｅａｒｅａｌｏｔｏｆａｐ ｐｌｉｃａｔｉｏｎｓａｂｏｕｔｃｏｄｅｏｂｆｕｓｃａｔｉｏｎ．Ｔｈｉｓｓｈｏｗｓｔｈｅｅｆｆｉｃｉｅｎｃｙｏｆｃｏｄｅｏｂｆｕｓｃａｔｉｏｎｕｎｄｅｒｓｏｍｅｌｉｍｉｔ ｅｄｅｎｖｉｒｏｎｍｅｎｔｓ．Ｓｏｔｈｅｐｒｏｖｉｎｇｏｆｉｔｓｅｆｆｉｃｉｅｎｃｙｉｓｔｈｅｐｒｉｍｅｐｒｏｂｌｅｍｏｆｔｈｅｒｅｓｅａｒｃｈ．Ｂｕｔｃｕｒ ｒｅｎｔｒｅｓｅａｒｃｈｔａｋｅｓｎｏａｃｃｏｕｎｔｏｆｔｈｅｓｅｍａｎｔｉｃｉｎｆｏｒｍａｔｉｏｎ．Ｔｈｉｓｐａｐｅｒｃｏｎｓｔｒｕｃｔｓａｓｅｍａｎｔｉｃｓ ｂａｓｅｄｃｏｍｐａｒａｂｌｅｆｒａｍｅｗｏｒｋ ｍｅａｓｕｒｉｎｇｏｂｆｕｓｃａｔｉｏｎｅｆｆｉｃｉｅｎｃｙ，ｗｈｉｃｈｎｏｔｏｎｌｙｐｒｏｖｅｅｆｆｉｃｉｅｎｃｙ ｕｎｄｅｒｔｈｅｌｉｍｉｔｅｄｅｎｖｉｒｏｎｍｅｎｔｏｆｓｔａｔｉｃａｎａｌｙｓｉｓ，ｂｕｔａｌｓｏｃａｎｅｓｔａｂｌｉｓｈｔｈｅｆｏｒｍａｌｆｏｕｎｄａｔｉｏｎｆｏｒ ｏｂｆｕｓｃａｔｉｏｎｅｆｆｉｃｉｅｎｃｙｃｏｍｐａｒｉｓｏｎ．Ｔｈｅｌａｓｔｐａｒｔｏｆｔｈｅｐａｐｅｒｉｌｌｕｓｔｒａｔｅｓｈｏｗｔｈｅｆｒａｍｅｗｏｒｋｃａｎ ｂｅａｐｐｌｉｅｄｔｏｍｅａｓｕｒｅｔｈｅｅｆｆｉｃｉｅｎｃｙｏｆｃｏｄｅｏｂｆｕｓｃａｔｉｏｎｗｉｔｈａｎｉｎｓｔａｎｔｉａｔｉｏｎ． 犓犲狔狑狅狉犱狊 ａｂｓｔｒａｃｔｉｎｔｅｒｐｒｅｔａｔｉｏｎ；ｐｒｏｇｒａｍｔｒａｎｓｆｏｒｍａｔｉｏｎ；ｐｒｏｇｒａｍ ａｎａｌｙｓｉｓ；ｃｏｄｅｏｂｆｕｓｃａ ｔｉｏｎ；ｆｌａｔｔｅｎｉｎｇａｌｇｏｒｉｔｈｍ １ 引 言 客户代码移动到主机执行时面临两类问题．一 类是恶意客户问题，这时需要保护主机执行环境的 安全性不会受下载的客户代码的影响；另一类是恶 意主机问题，这时需要保证客户代码不会被恶意主 机窃取信息或篡改．代码迷惑是针对恶意主机问题 而提出的一种保护客户代码的技术，它通过对代码 进行程序变换，提高变换后代码的理解难度，来达到
5期 高鹰等：基于抽象解释的代码迷惑有效性比较框架 807 保护客户代码的目的. 针对目前代码迷惑研究中缺乏基于语义的有效 代码迷惑以前的研究主要集中在构造有效的代 性证明以及缺乏限定环境下有效性证明的问题，本 码迷惑算法.Collbergt)中给出了有关这方面研究 文以代码迷惑引起的语义信息变化来刻画有效性， 比较完整的综述，引入了代码迷惑的定义，代码迷惑 提出了与语言无关的代码迷惑有效性比较框架，能 是一种以增加理解难度为目的的程序变换技术. 够为迷惑算法在静态分析这样的限定环境下提供严 Wang建立了针对恶意主机问题的代码安全体系， 格的有效性证明，也能够严格比较不同迷惑算法之 该安全体系的主要部件基于代码迷惑技术构造， 间的有效性.静态分析作为限定环境是指，攻击者使 而其中迷惑算法的核心思想是破坏程序的控制信 用静态分析作为攻击手段的攻击场景。 息.Ogiso)推广了Wang的算法，不仅破坏程序控 本文第2节概述代码迷惑有效性比较框架组成 制流信息，还进一步地破坏程序过程间的调用信息， 部分；第3节采用抽象解释理论形式化有效性比较 Douglas)针对Java语言的特征，通过构造复杂数 框架；第4节结合具体的迷惑算法描述如何实例化 据结构来增加代码的理解难度，关于构造代码迷惑 有效性比较框架：最后给出相关工作比较和结论. 算法的研究已经比较成熟. 但是，对于构造的代码迷惑算法是否有效，这些 2问题的提出 研究都没有提供严格证明，代码迷惑算法的构造缺 乏有效性证明的理论支持.而另一方面，许多研究已 建立代码迷惑有效性比较框架分两个部分进 经从理论上证明了代码迷惑作为安全方法的局限 行：形式化代码迷惑空间；形式地定义代码迷惑有效 性[5]，即证明了不存在代码迷惑能够完全保证信息 性度量 的安全性，经过迷惑后的代码总还或多或少存在信 第一步，形式化迷惑算法组成的代码迷惑空间. 息泄漏 关于代码迷惑，Collberg)给出了非形式的定义. 尽管在理论上代码迷惑并不能保证高机密信息 定义1.代码迷惑.程序变换τ。是代码迷惑是 的安全，但代码迷惑仍是代码安全问题中一种有效 指：(1)变换x保持程序可观察语义的等价性：(2)经 的安全技术，其原因是在很多场合下它能提供安全 过变换x使得程序某些属性的理解难度增加. 性，因此代码迷惑的研究一直活跃.一些具有代表性 根据上述定义，代码迷惑包含了两个性质，与程 的代码迷惑应用如下： 序变换一样保证程序可观察语义等价以及使得属性 恶意移动代理.移动代理在主机之间移动时， 的理解难度增加.形式化代码迷惑定义，也需要从刻 代码和执行的中间结果可能会被主机恶意获取篡 画这两个性质进行. 改.SPMA[]的研究表明，代码迷惑技术能够保证代 代码迷惑是一类特殊的程序变换，因此与程序 理在其移动存活期内被攻击的难度增加，从而达到 变换同样需要满足正确性性质.程序变换正确性是 保护移动代理的安全，对于恶意攻击者来说，恶意移 指变换前和变换后程序具有可观察语义等价性，由 动代理是一种时间受限环境，因为代理驻留在主机 文献[8]可知，可观察语义是对标准语义的抽象，程 上的时间是有限的。 序变换正确性等价于要求变换前后程序的标准语义 恶意逆向工程，越来越多的代码使用容易被反 在某种层次的抽象下相等，这为定义代码迷惑正确 编译的中间代码发布，使得软件开发者需要更多地 性提供了理论基础.属性是指从程序中提取的信息， 考虑其竞争者可能会反编译发布的代码，进而获取 可以使用上界闭包来刻画町，属性组成的属性空间 软件的设计以及其中的重要算法.虽然代码迷惑技 可定义偏序结构，属性的理解难度增加是通过属性 术无法为代码提供完全保护.但是，代码迷惑能够使 空间上的偏序关系来定义， 攻击者发现：复用反迷惑后得到的代码要比其重写 第二步，给出代码迷惑的有效性度量.代码迷惑 等效代码更加困难。 的有效性证明是基于定义的有效性度量.我们采用 这些都说明代码迷惑能够提供限定环境下的安 语义信息的变化来刻画有效性，通过迷惑前后的语 全性，如上述的时间受限环境以及不可复用环境等， 义信息来度量代码迷惑的有效性.语义信息通常是 限定环境是针对攻击者所处的攻击场景受到某些限 不可计算的，静态分析是对程序语义信息的保守近 制的情况，如在时间受限环境下，攻击者必须在代理 似，静态分析的结果能够可计算地反映语义信息的 存活期内篡改程序，攻击者的攻击时间是受限的. 变化.而且静态分析具有动态分析所不具备的可靠
保护客户代码的目的． 代码迷惑以前的研究主要集中在构造有效的代 码迷惑算法．Ｃｏｌｌｂｅｒｇ［１］中给出了有关这方面研究 比较完整的综述，引入了代码迷惑的定义，代码迷惑 是一种以 增 加 理 解 难 度 为 目 的 的 程 序 变 换 技 术． Ｗａｎｇ［２］建立了针对恶意主机问题的代码安全体系， 该安全体系 的 主 要 部 件 基 于 代 码 迷 惑 技 术 构 造， 而其中迷惑算法的核心思想是破坏程序的控制信 息．Ｏｇｉｓｏ［３］推广了 Ｗａｎｇ的算法，不仅破坏程序控 制流信息，还进一步地破坏程序过程间的调用信息． Ｄｏｕｇｌａｓ［４］针对Ｊａｖａ语言的特征，通过构造复杂数 据结构来增加代码的理解难度．关于构造代码迷惑 算法的研究已经比较成熟． 但是，对于构造的代码迷惑算法是否有效，这些 研究都没有提供严格证明，代码迷惑算法的构造缺 乏有效性证明的理论支持．而另一方面，许多研究已 经从理论上证明了代码迷惑作为安全方法的局限 性［５６］，即证明了不存在代码迷惑能够完全保证信息 的安全性，经过迷惑后的代码总还或多或少存在信 息泄漏． 尽管在理论上代码迷惑并不能保证高机密信息 的安全，但代码迷惑仍是代码安全问题中一种有效 的安全技术，其原因是在很多场合下它能提供安全 性，因此代码迷惑的研究一直活跃．一些具有代表性 的代码迷惑应用如下： 恶意移动代理．移动代理在主机之间移动时， 代码和执行的中间结果可能会被主机恶意获取篡 改．ＳＰＭＡ［７］的研究表明，代码迷惑技术能够保证代 理在其移动存活期内被攻击的难度增加，从而达到 保护移动代理的安全．对于恶意攻击者来说，恶意移 动代理是一种时间受限环境，因为代理驻留在主机 上的时间是有限的． 恶意逆向工程．越来越多的代码使用容易被反 编译的中间代码发布，使得软件开发者需要更多地 考虑其竞争者可能会反编译发布的代码，进而获取 软件的设计以及其中的重要算法．虽然代码迷惑技 术无法为代码提供完全保护．但是，代码迷惑能够使 攻击者发现：复用反迷惑后得到的代码要比其重写 等效代码更加困难． 这些都说明代码迷惑能够提供限定环境下的安 全性，如上述的时间受限环境以及不可复用环境等． 限定环境是针对攻击者所处的攻击场景受到某些限 制的情况，如在时间受限环境下，攻击者必须在代理 存活期内篡改程序，攻击者的攻击时间是受限的． 针对目前代码迷惑研究中缺乏基于语义的有效 性证明以及缺乏限定环境下有效性证明的问题，本 文以代码迷惑引起的语义信息变化来刻画有效性， 提出了与语言无关的代码迷惑有效性比较框架，能 够为迷惑算法在静态分析这样的限定环境下提供严 格的有效性证明，也能够严格比较不同迷惑算法之 间的有效性．静态分析作为限定环境是指，攻击者使 用静态分析作为攻击手段的攻击场景． 本文第２节概述代码迷惑有效性比较框架组成 部分；第３节采用抽象解释理论形式化有效性比较 框架；第４节结合具体的迷惑算法描述如何实例化 有效性比较框架；最后给出相关工作比较和结论． ２ 问题的提出 建立代码迷惑有效性比较框架分两个部分进 行：形式化代码迷惑空间；形式地定义代码迷惑有效 性度量． 第一步，形式化迷惑算法组成的代码迷惑空间． 关于代码迷惑，Ｃｏｌｌｂｅｒｇ［１］给出了非形式的定义． 定义１． 代码迷惑．程序变换τ狅犫是代码迷惑是 指：（１）变换τ狅犫保持程序可观察语义的等价性；（２）经 过变换τ狅犫使得程序某些属性的理解难度增加． 根据上述定义，代码迷惑包含了两个性质，与程 序变换一样保证程序可观察语义等价以及使得属性 的理解难度增加．形式化代码迷惑定义，也需要从刻 画这两个性质进行． 代码迷惑是一类特殊的程序变换，因此与程序 变换同样需要满足正确性性质．程序变换正确性是 指变换前和变换后程序具有可观察语义等价性．由 文献［８］可知，可观察语义是对标准语义的抽象，程 序变换正确性等价于要求变换前后程序的标准语义 在某种层次的抽象下相等．这为定义代码迷惑正确 性提供了理论基础．属性是指从程序中提取的信息， 可以使用上界闭包来刻画［９］，属性组成的属性空间 可定义偏序结构，属性的理解难度增加是通过属性 空间上的偏序关系来定义． 第二步，给出代码迷惑的有效性度量．代码迷惑 的有效性证明是基于定义的有效性度量．我们采用 语义信息的变化来刻画有效性，通过迷惑前后的语 义信息来度量代码迷惑的有效性．语义信息通常是 不可计算的，静态分析是对程序语义信息的保守近 似，静态分析的结果能够可计算地反映语义信息的 变化．而且静态分析具有动态分析所不具备的可靠 ５ 期 高 鹰等：基于抽象解释的代码迷惑有效性比较框架 ８０７
808 计算 机 学报 2007年 性，能够保守地反映程序的性质.许多研究者147.1町 抽象两种语义，将不可计算语义定义成具体语义，将 都采用静态分析建立攻击模型.因此，除不可计算语 可计算的语义定义成抽象语义，然后建立二者间的 义信息外，也需要采用静态分析得到的语义信息来 正确性联系，通过对可计算的抽象语义的求解来达 度量有效性。 到保守地计算不可计算语义的目的.后面我们将会 采用静态分析得到的语义信息来刻画有效性， 给出不可计算语义和可计算语义的例子.下面给出 是指对迷惑前和迷惑后程序进行分析，如果得到的 抽象解释的主要组成部分，抽象解释存在许多等价 分析集合变得更加庞大，则称迷惑算法是有效的.因 描述，本文使用与程序分析联系比较紧密的伽罗瓦 为迷惑使得静态分析工具只能得到平凡的结果 联系来描述抽象解释框架， 使用流图语言给出一个简单的例子，来解释基 定义2.伽罗瓦联系.完全偏序集〈C,二〉与完 于静态分析结果的有效性定义：关于流图语言的定 全偏序集〈C,二)满足伽罗瓦联系(Galois Connec- 义见第4节 tion),是指存在抽象函数a:C→C#以及具体函数 程序OP为：L1:x=?→L2; Y:C#→C,HX∈C,HX“∈C,满足关系： L2:y=1→L3；L3:y=y米x→Leit; a(X)|X台X|(X). 在程序中插入一段死代码，L处的分支条件 伽罗瓦联系也记为 false表示Ls是不会被执行到的，得到变换后的程序 (C,E)≠(C,E). OP'为 对程序语言L中的程序P,给出组成抽象解释框 L1:x=?→L2；L2:y=1→L3 架两种语义的定义. L3:true→L4;L4:y=y￥x→Let; 定义3.具体语义，具体语义论域是由偏序集 La:false→Ls;Ls:x=1→Lea. 合〈D,三)构成，其中三‘是定义在集合D上的偏序， 到达定值分析的目的是分析程序中的赋值信 S∈P→D,是基于语言L语法构造的到域D上的指 息)，我们将看到死代码插入会导致分析结果精度 称，称为具体域D上的具体语义函数，具体语义函数 的下降 就构成了程序的具体语义， 针对程序点L入口处，来分析比较变换前程 定义4.抽象语义.抽象语义论域是由偏序集 序OP和变换后程序OP'的分析结果： 合(A,三“〉构成，其中二“是定义在集合A上的偏序， 对于程序OP,分析得到的集合为 S∈P→A是基于语言L语法构造的到域A上的指 m{(x,L1),(y,L2)}, 称，称为抽象域A上的抽象语义函数，抽象语义函数 其中，m{(x,L)}表示在程序点Lm的入口处存在 就构成了程序的抽象语义. 着对x的赋值，括号里的第二个元素表示赋值发生 通常，为保证求解终止性，具体域和抽象域需要 的程序点. 具有比偏序集更强的性质，下面提到的语义论域都 对于变换后程序OP',分析得到的集合增大 是指完全偏序或是完全格.通过寻找伽罗瓦联系，建 为{(x,L),(x,L4),(y,L3)},是变换前在该程 立具体域和抽象域间的联系： 序点分析集合的超集.而且进一步计算整个程序的 (D,E),≠(A,E) (1) 定值集合就能发现，变换后程序的分析集合也是变 在建立了论域间的伽罗瓦联系后，抽象语义通 换前程序的分析集合的超集.所以，死代码变换是一 过式子S=a·S建立了对具体语义的抽象 种代码迷惑，死代码变换对于到达定值分析来说是 这样就建立了抽象解释框架，抽象解释框架只 有效的 考虑语义之间的正确性联系，而忽略语义定义的细 节，因此具体语义和抽象语义是通用的概念，需要根 3 建立代码迷惑有效性比较框架 据不同的应用对二者进行实例化，下面给出几组需 要用到的抽象解释框架下的实例. 首先简要介绍抽象解释[町.经典抽象解释是一 定义5.标准语义.它是指定义语言的动态语 种针对计算机系统语义模型的近似理论.抽象解释 义，通常是指对语言的标准指称解释，其中标准语义 为不可计算语义建立了安全可靠的近似语义，通过 论域由偏序集〈Ds,二s)组成，Ss:P→Ds为标准语 可计算的近似语义来达到描述不可计算的语义的目 义函数 的.主要思想是对给定的程序设计语言赋予具体和 定义6.可观察语义.它是指程序中针对某些
性，能够保守地反映程序的性质．许多研究者［１４，７，１０］ 都采用静态分析建立攻击模型．因此，除不可计算语 义信息外，也需要采用静态分析得到的语义信息来 度量有效性． 采用静态分析得到的语义信息来刻画有效性， 是指对迷惑前和迷惑后程序进行分析，如果得到的 分析集合变得更加庞大，则称迷惑算法是有效的．因 为迷惑使得静态分析工具只能得到平凡的结果． 使用流图语言给出一个简单的例子，来解释基 于静态分析结果的有效性定义：关于流图语言的定 义见第４节 程序 ＯＰ为：犔１：狓··＝？→犔２； 犔２：狔··＝１→犔３；犔３：狔··＝狔狓→犔ｅｘｉｔ； 在程 序 中 插 入 一 段 死 代 码，犔３ 处 的 分 支 条 件 ｆａｌｓｅ表示犔５是不会被执行到的，得到变换后的程序 ＯＰ′为 犔１：狓··＝？→犔２；犔２：狔··＝１→犔３； 犔３：ｔｒｕｅ→犔４；犔４：狔··＝狔狓→犔ｅｘｉｔ； 犔３：ｆａｌｓｅ→犔５；犔５：狓··＝１→犔ｅｘｉｔ． 到达定值分析的目的是分析程序中的赋值信 息［１１］，我们将看到死代码插入会导致分析结果精度 的下降． 针对程序点 犔ｅｘｉｔ入口处，来分析比较变换前程 序 ＯＰ和变换后程序 ＯＰ′的分析结果： 对于程序 ＯＰ，分析得到的集合为 犔ｅｘｉｔ｛（狓，犔１），（狔，犔２）｝， 其中，犔ｅｘｉｔ｛（狓，犔１）｝表示在程序点犔ｅｘｉｔ的入口处存在 着对狓的赋值，括号里的第二个元素表示赋值发生 的程序点． 对于变 换 后 程 序 ＯＰ′，分 析 得 到 的 集 合 增 大 为犔ｅｘｉｔ｛（狓，犔１），（狓，犔４），（狔，犔３）｝，是变换前在该程 序点分析集合的超集．而且进一步计算整个程序的 定值集合就能发现，变换后程序的分析集合也是变 换前程序的分析集合的超集．所以，死代码变换是一 种代码迷惑，死代码变换对于到达定值分析来说是 有效的． ３ 建立代码迷惑有效性比较框架 首先简要介绍抽象解释［９］ ．经典抽象解释是一 种针对计算机系统语义模型的近似理论．抽象解释 为不可计算语义建立了安全可靠的近似语义，通过 可计算的近似语义来达到描述不可计算的语义的目 的．主要思想是对给定的程序设计语言赋予具体和 抽象两种语义，将不可计算语义定义成具体语义，将 可计算的语义定义成抽象语义，然后建立二者间的 正确性联系，通过对可计算的抽象语义的求解来达 到保守地计算不可计算语义的目的．后面我们将会 给出不可计算语义和可计算语义的例子．下面给出 抽象解释的主要组成部分，抽象解释存在许多等价 描述，本文使用与程序分析联系比较紧密的伽罗瓦 联系来描述抽象解释框架． 定义２． 伽罗瓦联系．完全偏序集〈!，!〉与完 全偏序集〈!＃，!＃〉满足伽罗瓦联系（ＧａｌｏｉｓＣｏｎｎｅｃ ｔｉｏｎ），是指存在抽象函数α：! → !＃ 以及具体函数 γ：!＃ → !，犡∈!，犡＃∈!＃，满足关系： α（犡）｜＃ 犡＃犡｜γ（犡＃）． 伽罗瓦联系也记为 〈!，!〉←→ α γ 〈!＃，!＃〉． 对程序语言"中的程序#，给出组成抽象解释框 架两种语义的定义． 定义３． 具体语义．具体语义论域是由偏序集 合〈"，!犮〉构成，其中!犮是定义在集合"上的偏序， #∈#→ "，是基于语言"语法构造的到域"上的指 称，称为具体域"上的具体语义函数，具体语义函数 就构成了程序的具体语义． 定义４． 抽象语义．抽象语义论域是由偏序集 合〈$，!犪〉构成，其中!犪 是定义在集合$ 上的偏序， #犪 ∈#→ $ 是基于语言"语法构造的到域$ 上的指 称，称为抽象域$ 上的抽象语义函数，抽象语义函数 就构成了程序的抽象语义． 通常，为保证求解终止性，具体域和抽象域需要 具有比偏序集更强的性质．下面提到的语义论域都 是指完全偏序或是完全格．通过寻找伽罗瓦联系，建 立具体域和抽象域间的联系： 〈"，!犮〉←→ α γ 〈$ ，!犪〉 （１） 在建立了论域间的伽罗瓦联系后，抽象语义通 过式子#犪 ＝α#建立了对具体语义的抽象． 这样就建立了抽象解释框架，抽象解释框架只 考虑语义之间的正确性联系，而忽略语义定义的细 节，因此具体语义和抽象语义是通用的概念，需要根 据不同的应用对二者进行实例化，下面给出几组需 要用到的抽象解释框架下的实例． 定义５． 标准语义．它是指定义语言的动态语 义，通常是指对语言的标准指称解释，其中标准语义 论域由偏序集〈"犛，!犛〉组成，#犛：# → "犛为标准语 义函数． 定义６． 可观察语义．它是指程序中针对某些 ８０８ 计 算 机 学 报 ２００７年
5期 高鹰等：基于抽象解释的代码迷惑有效性比较框架 809 属性在语义域上的感兴趣的取值，其中D。是可观察 空间的定义.属性是形式化代码迷惑定义所需的， 语义论域，一般与标准语义域(Ds,二s》相同.O:P→ 只有定义了属性才能定义程序理解难度的增加； Ds为可观察语义函数 3.2节在给出的属性定义的基础上，形式化代码迷 标准语义提供了程序动态运行行为的精确定 惑组成的迷惑空间：3.3节基于程序分析框架，建立 义，是其它一切语义模型建立抽象的起点，所有其它 有效性度量的标准，为比较代码迷惑的有效性提供 的语义都是对标准语义的抽象.而可观察语义正是 语义上的度量. 对标准语义某个方面的抽象，若建立了标准语义域 3.1建立属性空间 到可观察语义域之间的伽罗瓦联系： 程序在具体域上的取值称为具体属性，在抽象 (DE)房D,) (2) 域上的取值称为抽象属性，通常具体属性都是不可 计算的，需要使用对应的可计算抽象属性来描述具体 又因为抽象语义可以通过式子S“=a·S建立了 属性.具体属性和抽象属性间的联系称为属性关系. 对具体语义的抽象，在建立了论域间的伽罗瓦联系 首先给出定义属性空间所需的上界闭包的定义， 后，可观察语义就可由O=a。·Ss定义， 定义9.上界闭包.对于偏序集(P,三〉，算子 抽象解释框架应用到静态程序分析时，具体语 P:P→P是上界闭包算子，是指具备以下性质： 义和抽象语义分别实例化成收集语义和分析语义， (1)单调的(monotone).HP,Q∈P,PgQ, 定义7.收集语义.它是指可到达程序动态运行 (P)E(Q); 行为的并集.收集语义论域(Da,三a),Dal△(D (2)幂等的(idempotent).pp=p; s),由标准语义论域的幂集组成，S:P→Da为收 (3)外延的(extensive).VP∈P,p(P)口P. 集语义函数. 那么，(P)就称为是偏序集P关于闭包算子p 定义8.分析语义，它是指静态分析时基于收 的一个上界闭包.uco(P)表示偏序集P上的全部上 集语义得到的保守语义信息.分析语义论域由偏序 界闭包算子集合，需要注意的是，许多研究并不区分 集〈A。,三)组成，S。:P→A,为分析语义函数. 上界闭包算子和上界闭包的使用.本文需要区分二者 对于静态分析算法，可以建立收集语义域 作为属性关系和属性的定义，所以，又引入UCO(P) 〈Da,三)到分析语义域(A。,三，)间的伽罗瓦联系： 表示偏序集P上的全部上界闭包集合. (Da,Ed）(Ag,ee） (3) 抽象域可以使用上界闭包等价地刻画町，本文 同样，根据论域间建立的伽罗瓦联系，分析语义 的抽象解释框架是使用伽罗瓦联系定义，因此下面 可由Sg=ag°Sat定义. 给出基于伽罗瓦联系的上界闭包算子定义，由伽罗 对于例子中提到的到达定值分析，我们来看基 瓦联系(1)，可定义PA=Ya,PA∈D→D,得到的PA 于抽象解释框架是如何定义程序分析算法的.首先 就是与抽象域A相关的上界闭包算子.对于抽象域 是实例化具体语义得到收集语义，通常是到达程序 〈A,三〉，根据定义的P4,存在关系Pa(D)≥A,即 点的所有状态的并.对于程序OP,进入程序点L3的 Pa(D)与A具有相同的逻辑含义，具体域的上界闭 状态为{x=?,y=?,之=1}，这里的状态只包含 包Pa(D)是抽象域A的同构刻画. 了环境中值的映射，因为x取值的不确定性，使得 使用上界闭包表示抽象域的好处是，在推导抽 程序点L3处y值是不可解的，因此这里的收集语义 象域上的属性时，无需得到抽象域上的对象，因为对 是不可计算的.然后是实例化抽象语义得到分析语 于抽象域(A,三“〉，〈Pa(D),三)能同构地反映它的 义，是通过定义到达定值分析的抽象函数a,:Dl→ 元素，而Pa(D)的构造与抽象域A的定义是无关的. A。,由收集语义构造得到.限于篇幅，这里不再给出 程序的属性空间是由全体具体属性和抽象属性 a,的形式定义.对于程序OP进入程序点L的分析 组成.抽象域可由上界闭包等价刻画，具体域D上所 语义是：{(x,?),(y,L1),(,L2)},表示所有到达程 有抽象域组成的偏序集L(D)=UCO(D),二〉.由 序点L:的定值信息.分析语义中关心的是定值信 上界闭包算子的外延性可知：D三UCO(D),即具体 息，程序点Ls处y的定值信息是可解的，因此x定 域D上的元素也属于UCO(D),因此，偏序集L:就组 值信息的分析是可计算的， 成了具体域D的属性空间.UCO(D)上的偏序关系 本节主要内容是基于抽象解释框架，建立代码 二可以比较属性之间的语义的精度. 迷惑有效性比较框架.3.1节给出属性组成的属性 属性关系表示了具体属性和抽象属性的联系
属性在语义域上的感兴趣的取值，其中"狅是可观察 语义论域，一般与标准语义域〈"犛，!犛〉相同．%：# → "犛为可观察语义函数． 标准语义提供了程序动态运行行为的精确定 义，是其它一切语义模型建立抽象的起点，所有其它 的语义都是对标准语义的抽象．而可观察语义正是 对标准语义某个方面的抽象．若建立了标准语义域 到可观察语义域之间的伽罗瓦联系： 〈"犛，!犛〉→ α ← ０ γ０ 〈"狅，!狅〉 （２） 又因为抽象语义可以通过式子#犪 ＝α# 建立了 对具体语义的抽象，在建立了论域间的伽罗瓦联系 后，可观察语义就可由% ＝α狅#犛 定义． 抽象解释框架应用到静态程序分析时，具体语 义和抽象语义分别实例化成收集语义和分析语义． 定义７． 收集语义．它是指可到达程序动态运行 行为的并集．收集语义论域〈"犮狅犾，!犮狅犾〉，"犮狅犾 !（" 犛），由标准语义论域的幂集组成，#犮狅犾：# → "犮狅犾为收 集语义函数． 定义８． 分析语义．它是指静态分析时基于收 集语义得到的保守语义信息．分析语义论域由偏序 集〈$φ，!φ〉组成，#φ：# → $φ为分析语义函数． 对于静 态 分 析 算 法φ，可 以 建 立 收 集 语 义 域 〈"犮狅犾，!犮狅犾〉到分析语义域〈$φ，!φ〉间的伽罗瓦联系： 〈"犮狅犾，!犮狅犾〉→ α ← φ γφ 〈$φ，!φ〉 （３） 同样，根据论域间建立的伽罗瓦联系，分析语义 可由#φ＝αφ#犮狅犾定义． 对于例子中提到的到达定值分析，我们来看基 于抽象解释框架是如何定义程序分析算法的．首先 是实例化具体语义得到收集语义，通常是到达程序 点的所有状态的并．对于程序 ＯＰ，进入程序点犔３的 状态为｛狓··＝？，狔··＝ ？，狕··＝１｝，这里的状态只包含 了环境中值的映射，因为狓 取值的不确定性，使得 程序点犔３处狔值是不可解的，因此这里的收集语义 是不可计算的．然后是实例化抽象语义得到分析语 义，是通过定义到达定值分析的抽象函数αφ："犮狅犾 → $φ，由收集语义构造得到．限于篇幅，这里不再给出 αφ的形式定义．对于程序 ＯＰ进入程序点犔３的分析 语义是：｛（狓，？），（狔，犔１），（狕，犔２）｝，表示所有到达程 序点犔３的定值信息．分析语义中关心的是定值信 息，程序点犔３处狔 的定值信息是可解的，因此狓 定 值信息的分析是可计算的． 本节主要内容是基于抽象解释框架，建立代码 迷惑有效性比较框架．３．１节给出属性组成的属性 空间的定义．属性是形式化代码迷惑定义所需的， 只有 定 义 了 属 性 才 能 定 义 程 序 理 解 难 度 的 增 加； ３．２节在给出的属性定义的基础上，形式化代码迷 惑组成的迷惑空间；３．３节基于程序分析框架，建立 有效性度量的标准，为比较代码迷惑的有效性提供 语义上的度量． ３１ 建立属性空间 程序在具体域上的取值称为具体属性，在抽象 域上的取值称为抽象属性，通常具体属性都是不可 计算的，需要使用对应的可计算抽象属性来描述具体 属性．具体属性和抽象属性间的联系称为属性关系． 首先给出定义属性空间所需的上界闭包的定义． 定义９． 上界闭包．对于偏序集〈&，!〉，算子 ρ：& → &是上界闭包算子，是指具备以下性质： （１）单 调 的 （ｍｏｎｏｔｏｎｅ）．犘，犙∈ &，犘 !犙， ρ（犘）!ρ（犙）； （２）幂等的（ｉｄｅｍｐｏｔｅｎｔ）．ρρ＝ρ； （３）外延的（ｅｘｔｅｎｓｉｖｅ）．犘∈&，ρ（犘）$犘． 那么，ρ（&）就称为是偏序集 &关于闭包算子ρ 的一个上界闭包．狌犮狅（&）表示偏序集&上的全部上 界闭包算子集合．需要注意的是，许多研究并不区分 上界闭包算子和上界闭包的使用．本文需要区分二者 作为属性关系和属性的定义，所以，又引入犝犆犗（&） 表示偏序集&上的全部上界闭包集合． 抽象域可以使用上界闭包等价地刻画［９］ ．本文 的抽象解释框架是使用伽罗瓦联系定义，因此下面 给出基于伽罗瓦联系的上界闭包算子定义．由伽罗 瓦联系（１），可定义ρ犃＝γα，ρ犃 ∈" → "，得到的ρ犃 就是与抽象域$ 相关的上界闭包算子．对于抽象域 〈$，!犪〉，根据定义的ρ犃，存在关系ρ犃 （"）$，即 ρ犃（"）与$ 具有相同的逻辑含义，具体域的上界闭 包ρ犃（"）是抽象域$ 的同构刻画． 使用上界闭包表示抽象域的好处是，在推导抽 象域上的属性时，无需得到抽象域上的对象，因为对 于抽象域〈$，!犪〉，〈ρ犃（"），!犮〉能同构地反映它的 元素，而ρ犃（"）的构造与抽象域$ 的定义是无关的． 程序的属性空间是由全体具体属性和抽象属性 组成．抽象域可由上界闭包等价刻画，具体域"上所 有抽象域组成的偏序集"犮（"）＝〈犝犆犗（"），!犮〉．由 上界闭包算子的外延性可知："犝犆犗（"），即具体 域"上的元素也属于犝犆犗（"），因此，偏序集"犮就组 成了具体域"的属性空间．犝犆犗（"）上的偏序关系 !犮可以比较属性之间的语义的精度． 属性关系表示了具体属性和抽象属性的联系， ５ 期 高 鹰等：基于抽象解释的代码迷惑有效性比较框架 ８０９
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]二
可以由上界闭包算子来定义，对于具体域"，属性关 系组成偏序集!犮（"）＝〈狌犮狅（"），!狉〉，!狉表示算子 之间的偏序，即犘∈"，ρ!狉 ρρ（犘）!犮 ρ（犘）．当" 为完全格时，能得到!犮也为完全格．因此，抽象解释 格!犮就组成了具体域"的属性关系空间． ３２ 模型化迷惑空间 为形式地定义代码迷惑组成的迷惑空间，根据 代码迷惑非形式定义，需要刻画两个性质：与程序变 换一样需要保持程序可观察语义等价性以及属性的 理解难度增加． 首先，代码迷惑是一种特殊的程序变换，因此需 要具有与程序变换相同的可靠性和正确性． （１）根据变换规则是基于语法的或是基于语义 的，程序变换可以分成两类：语法变换和语义变换． 这里τ狅犫：# → # 来表示语法变换，它对于输入程序 犘∈#得到变换后程序τ狅犫 !犘"；狋狅犫：" → "表示语义 变换，对于输入程序 犘 的具体语义#!犘"，变换后得 到语义狋狅犫［#!犘"］．抽象解释是基于语义的形式化框 架，使用语义来给出程序变换的规范，为证明语法变 换τ狅犫对程序的变化满足规范，需要建立与满足规范 定义的语义变换狋狅犫 之间的正确性联系．为此，语法 变换需要满足性质：#!τ狅犫 !犘""$狋狅犫［#!犘"］．在证明 程序变换的可靠性时，这是需要证明满足的性质．本 文是讨论程序变换的语义信息的变化行为，并不涉 及到语法变换需要满足一定语义规范的性质，因此， 代码迷惑有效性比较框架不需要证明语法变换的可 靠性性质． （２）程序变换的正确性是要求程序变换在可观 察抽象%下具有等价性．由图１，对于语法变换τ狅犫， 变换后的程序τ狅犫［犘］的具体语义为#!τ狅犫!犘""；对于 语义变换狋狅犫，基于程序 犘 的具体语义#!犘"，经过语 义变换后得到具体语义狋狅犫［#!犘"］；加上程序 犘 的 具体语义#!犘"，这三者之间需要满足可观察语义的 等价性． ! !"# ! ! ! $"#!! ! # % % ! ! ' $"& !"& ! ! !"& ! ! 图 １ 迷惑算法的正确性关系 即代码迷惑需要满足以下正确性定理：给定程 序犘∈#，那么等式 %（#!犘"）＝%（狋狅犫［#!犘"］）＝%（#!τ狅犫!犘""） 必须要成立，这就是代码迷惑的可观察语义等价性 定理． 根据属性空间的定义，具体域"的属性空间由 偏序集"犮（"）组成，偏序关系意味着信息的丢失，我 们使用"犮（"）上的偏序关系来反映属性的理解难度 的增加，因此，可以得到代码迷惑形式的定义． 定义１０． 代码迷惑．程序变换τ狅犫 是代码迷惑 是指τ狅犫使得某种属性关系狆∈狌犮狅（"）满足偏序关系： 狆（#!犘"）!犮 狆（#!τ狅犫!犘""）， 其中!犮是具体域〈"，!犮〉上的偏序关系． 该定义反映了代码迷惑需要满足的两个性质： 可观察语义等价和存在属性理解难度增加． ３３ 模型化迷惑有效性 为了比较代码迷惑的有效性，需要选择比较的 度量．本文主要采用以静态程序分析结果作为评价 的基准，原因是：第一，基于语义角度的代码迷惑有 效性评估，能够比基于语法的度量更加反映程序的 本质，而且更加接近于逆向工程者的角度；第二，具 体属性通常是不可计算的，需要得到具体属性的可 靠保守解答，当然，不完备性使得抽象属性不能精确 地回答具体域上的问题．基于抽象解释框架下的程 序分析定义，下面以命题的形式给出使用语义信息 作为有效性比较的度量标准． 一般地，迷惑的有效性比较是基于可计算的语 义上的． 命题１（迷惑的有效性）．犘∈#，φ∈狌犮狅（"）， 如果关系#φ!犘"!φ #φ! τ狅犫 !犘""成立，则称变换τ狅犫针 对分析算法φ是有效的．上界闭包算子φ是伽罗瓦 联系的等效描述，当实例化为对程序分析框架时，φ 指代具体的分析算法． 抽象解释框架下，程序的收集语义和分析语义 分别是具体语义和抽象语义的实例化，迷惑的有效 性比较是基于收集语义或是分析语义，而有效性度 量则是由论域上的偏序关系来确定．这里的有效性 度量与代码迷惑的定义是一致的，当然，为了使得有 效性比较框架更加具有描述力，在此基础上可以使 用与定义不一致的更加复杂的有效性度量定义． 传递定理． 犘，犙∈#，#!犘"!犮#!犙"#犪 !犘" !犪 #犪 !犙"． 证明． 由伽罗瓦联系（１），#到#犪 间可以建立单 调的映射关系 #犪 ＝α#，由α 的单调性且 #!犘 "!犮 ８１０ 计 算 机 学 报 ２００７年