第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]二
可以由上界闭包算子来定义，对于具体域"，属性关 系组成偏序集!犮（"）＝〈狌犮狅（"），!狉〉，!狉表示算子 之间的偏序，即犘∈"，ρ!狉 ρρ（犘）!犮 ρ（犘）．当" 为完全格时，能得到!犮也为完全格．因此，抽象解释 格!犮就组成了具体域"的属性关系空间． ３２ 模型化迷惑空间 为形式地定义代码迷惑组成的迷惑空间，根据 代码迷惑非形式定义，需要刻画两个性质：与程序变 换一样需要保持程序可观察语义等价性以及属性的 理解难度增加． 首先，代码迷惑是一种特殊的程序变换，因此需 要具有与程序变换相同的可靠性和正确性． （１）根据变换规则是基于语法的或是基于语义 的，程序变换可以分成两类：语法变换和语义变换． 这里τ狅犫：# → # 来表示语法变换，它对于输入程序 犘∈#得到变换后程序τ狅犫 !犘"；狋狅犫：" → "表示语义 变换，对于输入程序 犘 的具体语义#!犘"，变换后得 到语义狋狅犫［#!犘"］．抽象解释是基于语义的形式化框 架，使用语义来给出程序变换的规范，为证明语法变 换τ狅犫对程序的变化满足规范，需要建立与满足规范 定义的语义变换狋狅犫 之间的正确性联系．为此，语法 变换需要满足性质：#!τ狅犫 !犘""$狋狅犫［#!犘"］．在证明 程序变换的可靠性时，这是需要证明满足的性质．本 文是讨论程序变换的语义信息的变化行为，并不涉 及到语法变换需要满足一定语义规范的性质，因此， 代码迷惑有效性比较框架不需要证明语法变换的可 靠性性质． （２）程序变换的正确性是要求程序变换在可观 察抽象%下具有等价性．由图１，对于语法变换τ狅犫， 变换后的程序τ狅犫［犘］的具体语义为#!τ狅犫!犘""；对于 语义变换狋狅犫，基于程序 犘 的具体语义#!犘"，经过语 义变换后得到具体语义狋狅犫［#!犘"］；加上程序 犘 的 具体语义#!犘"，这三者之间需要满足可观察语义的 等价性． ! !"# ! ! ! $"#!! ! # % % ! ! ' $"& !"& ! ! !"& ! ! 图 １ 迷惑算法的正确性关系 即代码迷惑需要满足以下正确性定理：给定程 序犘∈#，那么等式 %（#!犘"）＝%（狋狅犫［#!犘"］）＝%（#!τ狅犫!犘""） 必须要成立，这就是代码迷惑的可观察语义等价性 定理． 根据属性空间的定义，具体域"的属性空间由 偏序集"犮（"）组成，偏序关系意味着信息的丢失，我 们使用"犮（"）上的偏序关系来反映属性的理解难度 的增加，因此，可以得到代码迷惑形式的定义． 定义１０． 代码迷惑．程序变换τ狅犫 是代码迷惑 是指τ狅犫使得某种属性关系狆∈狌犮狅（"）满足偏序关系： 狆（#!犘"）!犮 狆（#!τ狅犫!犘""）， 其中!犮是具体域〈"，!犮〉上的偏序关系． 该定义反映了代码迷惑需要满足的两个性质： 可观察语义等价和存在属性理解难度增加． ３３ 模型化迷惑有效性 为了比较代码迷惑的有效性，需要选择比较的 度量．本文主要采用以静态程序分析结果作为评价 的基准，原因是：第一，基于语义角度的代码迷惑有 效性评估，能够比基于语法的度量更加反映程序的 本质，而且更加接近于逆向工程者的角度；第二，具 体属性通常是不可计算的，需要得到具体属性的可 靠保守解答，当然，不完备性使得抽象属性不能精确 地回答具体域上的问题．基于抽象解释框架下的程 序分析定义，下面以命题的形式给出使用语义信息 作为有效性比较的度量标准． 一般地，迷惑的有效性比较是基于可计算的语 义上的． 命题１（迷惑的有效性）．犘∈#，φ∈狌犮狅（"）， 如果关系#φ!犘"!φ #φ! τ狅犫 !犘""成立，则称变换τ狅犫针 对分析算法φ是有效的．上界闭包算子φ是伽罗瓦 联系的等效描述，当实例化为对程序分析框架时，φ 指代具体的分析算法． 抽象解释框架下，程序的收集语义和分析语义 分别是具体语义和抽象语义的实例化，迷惑的有效 性比较是基于收集语义或是分析语义，而有效性度 量则是由论域上的偏序关系来确定．这里的有效性 度量与代码迷惑的定义是一致的，当然，为了使得有 效性比较框架更加具有描述力，在此基础上可以使 用与定义不一致的更加复杂的有效性度量定义． 传递定理． 犘，犙∈#，#!犘"!犮#!犙"#犪 !犘" !犪 #犪 !犙"． 证明． 由伽罗瓦联系（１），#到#犪 间可以建立单 调的映射关系 #犪 ＝α#，由α 的单调性且 #!犘 "!犮 ８１０ 计 算 机 学 报 ２００７年
5期 高鹰等：基于抽象解释的代码迷惑有效性比较框架 811 SQ],可以保证结论成立. 代码迷惑有效性定理。 传递定理也可以表述为抽象α是保偏序的. 4.1定义实例语言 推论.HP,Q∈P,SaIP]ESu IQ]→S,IP] 首先在流图语言[]（如图2）的基础上定义离散 E+S,IQ1. 转移系统T=〈∑，：，〉定义如下： 传递定律及其推论的含义在于：抽象解释将程 ∑表示状态集合，Σ三3×C,其中3是环境集 序分析看成是语义的近似，分析算法即是建立对语 合，环境是变量到值的映射，C是命令集合.状态s= 义的抽象：而且程序分析算法之间可以建立相互之 (p,C)中，p表示下一条命令C的执行环境. 间的抽象.所以可以根据传递定理，只要对于某一种 ,二Σ表示程序的初始状态 抽象的程序分析算法满足偏序，那么这样的偏序关 程序 P:PP△(C) 系是可以传递到其它由该抽象构造的其它程序分析 命令 C:CC::=LI:A-L2 算法上的， 程序动作A:AA:=V:=EV:=?引hpB 算术表达式E:EE:=nlxlEiop.E: 因此，如果在收集语义上可以比较迷惑有效性， 布尔表达式B:BB:=true|falsel Biops B2|-E:|Biop.Bz 能得到更强的结论，因为此时还不涉及到分析语义 变量 V:V标签L:L整数n:Z 的实例化，迷惑算法在收集语义上的有效性，对于所 图2流图语言的语法（其中op.是二元算术算子，0p是 有分析算法来说都是有效的. 二元逻辑算子，0p.是二元逻辑比较算子) 所以，迷惑的有效性比较是能够基于不可计算 图3是对流图语言语义的定义，转移关系S∈ 的语义上的. C→（∑和(）)可以定义为 命题2（迷惑的有效性）.VP∈P,如果关系 S((p,C))=(p,C')lp'ES lact [C]]pA Sa[P]Ecol Sco ITob[P]成立，则称变换t针对任意 suc [C]=labIC']). 分析算法都是有效的. 定义程序P∈P的转移语义S∈P→（Σ→和(）) 命题1和命题2为比较迷惑前后的程序的语义 为：SPs={(p,C)∈S(p,C)|s=〈p,C)p, 提供了理论基础.命题2要求的是对通常是不可计 p'∈3∧C∈P. 算的收集语义上的比较，通常无法直接计算得到二 二∑XΣ，表示状态s∈Σ与其可能后继s'∈ 者间的关系，但是可以得到比较强的结论，是通过语 的二元传递关系，(s,s)∈t当且仅当s'∈S(s),简记 义信息的变化来定义有效性的，与具体的分析算法 为s￥s',‘是转移关系S的另一种表达.如果命令 无关；而命题1是建立在分析语义基础上的，是基于 A,K∈C,且有suc[A]=lab[K],K是A的后继，为 分析得到的语义信息来定义有效性，可以直接计算 统一标记，也记为A￥K. 得到二者间的关系，不过有效性只是适用于这个具 体的分析算法. 程序动作：S[A]e:A→(3→3) SIskip le=p SIV :=El=[VA[El] 4 实例化有效性比较框架 s[V=l,=p[V一n],其中n∈z S[B]==p,其中B[Ble=true 布尔表达式：B[Elp:B→(3→3) 本节主要内容是根据上节提出的代码迷惑有效 B[ELOP6 E2le=A[E:leOpA [E:le 性比较框架，针对一个具体的迷惑算法，使用例子说 B[B1oP.B:le=B[B:lop.B [B:le 明有效性比较框架证明迷惑算法有效性的过程.为 算术表达式：A[E]:B→(3→3) A[rle=p(r) 证明迷惑算法的有效性，首先需要证明所比较的变 AIn le=p(n) 换算法是属于迷惑空间的，然后需要证明算法的有 A[E1op.E:le=A[E leop.A [E2le 效性满足有效性命题.为此，需要实例化的部分有实 图3流图语言的语义 例语言和迷惑算法，通过定义实例语言，就能够得到 标准语义.由抽象解释框架理论，实例化框架所需要 几个使用到的基本语义函数： 的其它语义，包括可观察语义、收集语义、分析语义， lab[L1:A→Lzl=L1 act IL1:A→Lz=A 都能通过对标准语义的定义抽象得到.在实例化这 sc[L1:A→L2l=L:war IL1:A→L2l=wr【A] 些部分后，就可以严格证明保证代码迷惑正确性的 迹是指状态转移序列，迹语义使用有限或是无 可观察语义等价性定理以及说明代码迷惑有效性的 限的状态序列来模型化计算过程，反映了程序最精
#!犙"，可以保证结论成立． 传递定理也可以表述为抽象α是保偏序的． 推论． 犘，犙∈#，#犮狅犾!犘"!#犮狅犾!犙"#φ!犘" !φ#φ!犙"． 传递定律及其推论的含义在于：抽象解释将程 序分析看成是语义的近似，分析算法即是建立对语 义的抽象；而且程序分析算法之间可以建立相互之 间的抽象．所以可以根据传递定理，只要对于某一种 抽象的程序分析算法满足偏序，那么这样的偏序关 系是可以传递到其它由该抽象构造的其它程序分析 算法上的． 因此，如果在收集语义上可以比较迷惑有效性， 能得到更强的结论，因为此时还不涉及到分析语义 的实例化，迷惑算法在收集语义上的有效性，对于所 有分析算法来说都是有效的． 所以，迷惑的有效性比较是能够基于不可计算 的语义上的． 命题２（迷惑的有效性）． 犘∈#，如果关系 #犮狅犾!犘"!犮狅犾#犮狅犾! τ狅犫!犘""成立，则称变换τ狅犫针对任意 分析算法都是有效的． 命题１和命题２为比较迷惑前后的程序的语义 提供了理论基础．命题２要求的是对通常是不可计 算的收集语义上的比较，通常无法直接计算得到二 者间的关系，但是可以得到比较强的结论，是通过语 义信息的变化来定义有效性的，与具体的分析算法 无关；而命题１是建立在分析语义基础上的，是基于 分析得到的语义信息来定义有效性，可以直接计算 得到二者间的关系，不过有效性只是适用于这个具 体的分析算法． ４ 实例化有效性比较框架 本节主要内容是根据上节提出的代码迷惑有效 性比较框架，针对一个具体的迷惑算法，使用例子说 明有效性比较框架证明迷惑算法有效性的过程．为 证明迷惑算法的有效性，首先需要证明所比较的变 换算法是属于迷惑空间的，然后需要证明算法的有 效性满足有效性命题．为此，需要实例化的部分有实 例语言和迷惑算法．通过定义实例语言，就能够得到 标准语义．由抽象解释框架理论，实例化框架所需要 的其它语义，包括可观察语义、收集语义、分析语义， 都能通过对标准语义的定义抽象得到．在实例化这 些部分后，就可以严格证明保证代码迷惑正确性的 可观察语义等价性定理以及说明代码迷惑有效性的 代码迷惑有效性定理． ４１ 定义实例语言 首先在流图语言［８］（如图２）的基础上定义离散 转移系统 %＝〈Σ，Σ犻，ι〉定义如下： Σ 表示状态集合，Σ "× &，其中 "是 环 境 集 合，环境是变量到值的映射，&是命令集合．状态狊＝ 〈ρ，犆〉中，ρ表示下一条命令犆 的执行环境． Σ犻Σ 表示程序的初始状态． 程序 犘：# 犘!（犆） 命令 犆：& 犆∷＝犔１：犃→犔２； 程序动作 犃：' 犃∷＝犞··＝ 犈｜犞··＝？｜狊犽犻狆｜犅 算术表达式 犈：( 犈∷＝狀｜狓｜犈１狅狆犪犈２ 布尔表达式 犅：) 犅∷＝ｔｒｕｅ｜ｆａｌｓｅ｜犅１狅狆犫犅２｜!犈２｜犅１狅狆犮犅２ 变量 犞：* 标签犔：" 整数狀：+ 图 ２ 流图语言的语法（其中狅狆犪是二元算术算子，狅狆犫是 二元逻辑算子，狅狆犮是二元逻辑比较算子） 图３是对流图语言语义的定义，转移关系犛∈ & →（Σ→ !（Σ））可以定义为 犛（〈ρ，犆〉）＝｛〈ρ′，犆′〉｜ρ′∈犛! 犪犮狋!犆"" ρ∧ 狊狌犮!犆"＝犾犪犫!犆′"｝． 定义程序犘∈#的转移语义犛∈#→（Σ→!（Σ）） 为：犛!犘狊" ＝｛〈ρ′，犆′〉∈犛（〈ρ，犆〉）｜狊＝〈ρ，犆〉∧ρ， ρ′∈"∧犆′∈犘｝． ιΣ×Σ，表示状态狊∈Σ 与其可能后继狊′∈Σ 的二元传递关系，〈狊，狊′〉∈ι当且仅当狊′∈犛（狊），简记 为狊↓狊′，ι是转移关系犛 的另一种表达．如果命令 Λ，Κ∈&，且有狊狌犮! Λ"＝犾犪犫! Κ"，Κ 是Λ 的后继，为 统一标记，也记为Λ↓Κ． 程序动作：犛!犃" ρ：'→ （" → "） 犛! 狊犽犻狆" ρ＝ρ 犛!犞··＝犈" ρ＝ρ［犞 #犃!犈" ρ］ 犛!犞··＝？" ρ＝ρ［犞 #狀］，其中狀∈+ 犛!犅" ρ＝ρ，其中犅!犅" ρ＝ｔｒｕｅ 布尔表达式：犅!犈" ρ：( → （" → "） 犅!犈１狅狆犫犈２" ρ＝犃!犈１" ρ狅狆犫犃!犈２" ρ 犅!犅１狅狆犮犅２" ρ＝犅!犅１" ρ狅狆犮犅!犅２" ρ 算术表达式：犃!犈" ρ：( → （" → "） 犃!狓" ρ＝ρ（狓） 犃! 狀" ρ＝ρ（狀） 犃!犈１狅狆犪犈２" ρ＝犃!犈１" ρ狅狆犪犃!犈２" ρ 图 ３ 流图语言的语义 几个使用到的基本语义函数： 犾犪犫!犔１：犃→犔２；"＝犔１ 犪犮狋!犔１：犃→犔２；"＝犃 狊狌犮!犔１：犃→犔２；"＝犔２ 狏犪狉!犔１：犃→犔２；"＝狏犪狉!犃" 迹是指状态转移序列，迹语义使用有限或是无 限的状态序列来模型化计算过程，反映了程序最精 ５ 期 高 鹰等：基于抽象解释的代码迷惑有效性比较框架 ８１１
812 计算 机学报 2007年 确的含义.对于定义的转移系统T(∑，，).={e} 数.设有标签映射对：2={l1→L1;…;l一Lm.分支 表示长度为0的迹的集合，e是空迹；表示长度为 函数：的作用是实现标签映射对2中的映射关系，将 n的迹的集合，Σ+={U>o}表示长度大于0的迹 到达标签点l,的控制转移跳转到标签L:(1≤≤n). 的集合；Σ·=Σ+UΣ表示有限长度迹的集合；= 对应到流图语言中，为实现标签映射对21，分支函 s…s。…表示长度为无穷的迹的集合.有非空迹σ∈ 数可以定义为{l1:A1→L1:…;ln:An→Ln}. UΣ+，则迹o可表示为s1s2￥s3…￥…，其中 算法的构造思想是，使用引入的控制变量来保 s∈∑；=ΣUΣ"表示迹的集合.对于程序P∈P 证变换前后的执行路径一致，即使得分支函数在变 和初始状态，迹语义函数：P→，[P]= 换前后都存在相同的映射.图4给出了压平算法的 {so=}U{oss'|s∈ΣAs￥s〉.下面将使用迹语义 变换过程，左边是迷惑前的控制流图，表示的标签映 来作为抽象解释框架的标准语义的定义， 射对为2={l1一L1；…;ln→Ln},右边是迷惑后的 为方便下文的叙述，给出几个符号的定义： 控制流图，同样需要具有与21相同的映射.通过 (1)限制(|.)：对于V二V下的环境p,l.是环境 switch节点和phi节点的构造来实现.sVar是其 p在变量集合y上的限制.定义为 中的控制变量，sVar的构造通常是迟钝的.这里由 对于程序P∈P,pl。={p(y)ly∈dom[p]Ay∈ 迟钝谓词V"表示，于是可以得到switch节点的构 ,dom[p]表示环境p包含的变量集合 造：{switch:swVar=Vh→l1;…;switch:swVar= 也用在对程序P的限制，P|。是程序P在变量 V八.→ln},switch节点就等价于分支函数的作用，构 集合V上的限制.定义为 造的分支映射对为2mih={swVar=V乃→l1;…; 对于程序P∈P,P|={yly∈ar【PAy∈. sVar=V.一→lm}.因此构造中只需要加入命令来 (2)分支（‖）：若序列A=a1￥a2￥…￥am和序 对控制变量swVar赋值，就能保证分支函数具有与 列B=b1￥b2￥…↓b.满足a1=b1八am=bn八(i∈ 2相同的映射. (1,m).Hj∈(1，n).a:≠b),那么称序列A和序列 B是分支的，记为A‖B. G switch 4.2实例化迷惑算法 基于流图语言的定义，下面来形式地描述需要 证明的迷惑算法，证明它是满足可观察语义等价的. 首先形式化可观察语义定义，这里使用的是指 影响指定变量集合的迹集合。 phi 定义抽象函数ao:a(T;)={a(o;)|o∈T}; (a)代码迷惑前的控制流图 (b)压平后的控制流图 a(o;)={入iao(o:;V)};ao(o;V)=〈pv,C).表示 图4压平算法变换示意图 迹序列T中限制到变量集合V上得到的迹序列. 我们选择的例子是Wang的压平算法.压平 图5给出压平算法的形式描述.其中：L一L 算法属于控制流迷惑，它包含的将控制流图展平的 是变换前的分支映射函数，映射对2={l1→2；…： 思想成为许多迷惑系统中的核心，如Cloak公司的 lm-1→l..为简化流图语言语法，我们给出的压平 Cloakware技术；Wang的安全性框架；Collbergf 算法没有使用复杂数据结构来构造控制变量，这与 的Sandmark项目：Li町的基于函数指针的迷惑技 Wang的压平算法不同，但是简单表达式也是一种 术.因此，证明压平算法的有效性是有意义的 常用的构造迟钝谓词的方法[)，因此这样的变化并 压平算法中，迟钝变量是其中一个基本部件.由 不影响对原算法的说明。 Collberg在文献[1]中提出. nput:程序P(p1:p2…:pa) 定义11.如果变量V在程序点p具有某种属 FL(P)=((C.mdCp). =1 性q,q在迷惑过程中是已知的，但是在分析时是难 (C.mitp Cpli Caap)ll FL(P-P:),Vi>1 其中， 以理解的，这样的表达式称为是迟钝的.记为V%,如 (1)C.wich (lawi :swVar=V)D)Al=lab [pi] 果根据上下文程序点p是显然的，则可简写成V. (2)Cpl=(suc(p:)(swVar :=VI))A(I=next(p:)) (3)C与=lhi:kip→lweh； 迟钝变量通常是静态难以推导的值，但是运行时的 (4)FL(P-p:)=P(p1…:p:-1p:+1:p) (5)next(C)=kn(lab [C]) 值满足一定的性质. 下面给出压平算法的构造思路.首先定义分支函 图5压平算法的描述
确的含义．对于定义的转移系统%〈Σ，Σ犻，ι〉．Σ０＝｛ε｝ 表示长度为０的迹的集合，ε是空迹；Σ狀 表示长度为 狀 的迹的集合，Σ＋ ＝｛∪狀＞０Σ狀｝表示长度大于０的迹 的集合；Σ ＝Σ＋ ∪Σ０表示有限长度迹的集合；Σω ＝ 狊０…狊狀…表示长度为无穷的迹的集合．有非空迹σ∈ Σω ∪Σ＋ ，则迹σ可表示为狊１ ↓狊２ ↓狊３ …↓…．其中 狊犻∈Σ；Σι＝Σ∪Σω 表示迹的集合．对于程序 犘∈# 和初始状 态 Σ犻，迹 语 义 函 数 Σι：# →Σι，Σι!犘"＝ ｛狊０＝Σ犻｝∪｛σ狊狊′｜σ狊∈Σι∧狊↓狊′｝．下面将使用迹语义 来作为抽象解释框架的标准语义的定义． 为方便下文的叙述，给出几个符号的定义： （１）限制（｜狏）：对于' *下的环境ρ，ρ｜狏是环境 ρ在变量集合'上的限制．定义为 对于程序犘∈#，ρ｜狏 ＝｛ρ（狔）｜狔∈犱狅犿［ρ］∧狔∈ '｝，犱狅犿［ρ］表示环境ρ包含的变量集合． 也用在对程序犘 的限制，犘｜狏是程序犘 在变量 集合'上的限制．定义为 对于程序犘∈#，犘｜狏＝｛狔｜狔∈狏犪狉!犘" ∧狔∈'｝． （２）分支（‖）：若序列犃＝犪１↓犪２↓…↓犪犿和序 列犅＝犫１↓犫２↓…↓犫狀满足犪１＝犫１∧犪犿 ＝犫狀∧（犻∈ （１，犿）．犼∈（１，狀）．犪犻≠犫犼），那么称序列 犃 和序列 犅 是分支的，记为犃‖犅． ４２ 实例化迷惑算法 基于流图语言的定义，下面来形式地描述需要 证明的迷惑算法，证明它是满足可观察语义等价的． 首先形式化可观察语义定义，这里使用的是指 影响指定变量集合的迹集合． 定义抽象函数α０：α０（犜；'）＝｛α０（σ；'）｜σ∈犜｝； α０（σ；'）＝｛λ犻α．０（σ犻；'）｝；α０（σ犻；'）＝〈ρ｜犞 ，犆〉．表示 迹序列犜 中限制到变量集合'上得到的迹序列． 我们选择的例子是 Ｗａｎｇ［２］的压平算法．压平 算法属于控制流迷惑，它包含的将控制流图展平的 思想成为许多迷惑系统中的核心，如 Ｃｌｏａｋ公司的 Ｃｌｏａｋｗａｒｅ技术；Ｗａｎｇ［２］的安全性框架；Ｃｏｌｌｂｅｒｇ［１］ 的Ｓａｎｄｍａｒｋ项目；Ｌｉ［１２］的基于函数指针的迷惑技 术．因此，证明压平算法的有效性是有意义的． 压平算法中，迟钝变量是其中一个基本部件．由 Ｃｏｌｌｂｅｒｇ在文献［１］中提出． 定义１１． 如果变量犞 在程序点狆 具有某种属 性狇，狇在迷惑过程中是已知的，但是在分析时是难 以理解的，这样的表达式称为是迟钝的．记为犞狇 狆，如 果根据上下文程序点狆 是显然的，则可简写成犞狇 ． 迟钝变量通常是静态难以推导的值，但是运行时的 值满足一定的性质． 下面给出压平算法的构造思路．首先定义分支函 数．设有标签映射对：Ω＝｛犾１#犔１；…；犾狀#犔狀｝．分支 函数κΩ的作用是实现标签映射对Ω中的映射关系，将 到达标签点犾犻的控制转移跳转到标签犔犻（１犻狀）． 对应到流图语言中，为实现标签映射对 Ω１，分支函 数可以定义为｛犾１：犃１→犔１；…；犾狀：犃狀→犔狀｝． 算法的构造思想是，使用引入的控制变量来保 证变换前后的执行路径一致，即使得分支函数在变 换前后都存在相同的映射．图４给出了压平算法的 变换过程，左边是迷惑前的控制流图，表示的标签映 射对为Ω＝｛犾１ #犔１；…；犾狀 #犔狀｝，右边是迷惑后的 控制流 图，同 样 需 要 具 有 与 Ω１ 相 同 的 映 射．通 过 狊狑犻狋犮犺节点和狆犺犻节点的构造来实现．狊狑犞犪狉是其 中的控制变量，狊狑犞犪狉的构造通常是迟钝的．这里由 迟钝谓词犞狇 表示，于是可以得到狊狑犻狋犮犺 节点的构 造：｛狊狑犻狋犮犺：狊狑犞犪狉＝犞犾１ →犾１；…；狊狑犻狋犮犺：狊狑犞犪狉＝ 犞犾狀 →犾狀｝，狊狑犻狋犮犺节点就等价于分支函数的作用，构 造的分支映射对为 Ωｓｗｉｔｃｈ＝｛狊狑犞犪狉＝犞犾１ #犾１；…； 狊狑犞犪狉＝犞犾狀 #犾狀｝．因此构造中只需要加入命令来 对控制变量狊狑犞犪狉赋值，就能保证分支函数具有与 Ω 相同的映射． !! !" !" !##! !# $%&'() *)& !! !" !" !#$" ! ! !#$! !" !+ ! !"%& ! !#$! !# ,-. 代码迷惑前的控制流图 ,0. 压平后的控制流图 图 ４ 压平算法变换示意图 图５给出压平算法的形式描述．其中κΩ：" # " 是变换前的分支映射函数，映射对Ω＝｛犾１ #犾２；…； 犾狀－１ #犾狀｝．为简化流图语言语法，我们给出的压平 算法没有使用复杂数据结构来构造控制变量，这与 Ｗａｎｇ［２］的压平算法不同，但是简单表达式也是一种 常用的构造迟钝谓词的方法［１］，因此这样的变化并 不影响对原算法的说明． Ｉｎｐｕｔ：程序犘（狆１；狆２；…；狆狀）． 犉犔（犘）＝ （犆ｓｗｉｔｃｈ↓狆犻↓犆ｐｈｉ）， 犻＝１ ｛（犆ｓｗｉｔｃｈ↓狆犻↓犆ｐｈｉ↓犆ｓｋｉｐ）‖犉犔（犘－狆犻），犻＞１ 其中， （１）犆ｓｗｉｔｃｈ＝（犾ｓｗｉｔｃｈ：｛狊狑犞犪狉＝犞犾｝→犾）∧犾＝犾犪犫!狆犻" （２）犆ｐｈｉ＝（狊狌犮（狆犻）：｛狊狑犞犪狉··＝犞犾｝→犾｝）∧（犾＝狀犲狓狋（狆犻）） （３）犆ｓｋｉｐ＝犾ｐｈｉ：狊犽犻狆→犾ｓｗｉｔｃｈ； （４）犉犔（犘－狆犻）＝犘（狆１；…；狆犻－１；狆犻＋１；狆狀） （５）狀犲狓狋（犆）＝κΩ（犾犪犫!犆"） 图 ５ 压平算法的描述 ８１２ 计 算 机 学 报 ２００７年
5期 高鹰等：基于抽象解释的代码迷惑有效性比较框架 813 4.3定理的证明 些证明都不是基于语义模型，只是分析迷惑算法给 根据我们提出的代码迷惑有效性比较框架，实例 反迷惑分析算法带来分析时间上的影响.类似的，基 化压平算法的过程还需要证明两个基本的定理：保证 于密码理论的迷惑算法有效性研究也只是分析反迷 代码迷惑正确性的可观察语义等价性定理以及说明 惑算法的分析时间与所花费的控制，而无法从分析 代码迷惑有效性的代码迷惑有效性定理.限于篇幅， 的结果来证明代码迷惑带来的影响. 我们这里只给出定理的形式，而略去具体证明过程， 本文建立了证明代码迷惑有效性的理论框架， 这并不影响我们说明建立代码迷惑比较框架的过程， 目的是为代码迷惑有效性的比较提供与语言无关的 详细的证明过程可以查阅我们的网站(http:/ssg. 平台，其中的有效性证明依赖于有效性度量的定义： ustcsz.edu.cn/publication/jsj06_proof.doc). 关于有效性度量的研究，Dala1-1]的工作与我们的 定理1.压平算法可观察语义等价性.给定 工作比较接近.简要比较二者的不同：首先，Dalla的 任意P(p1:p2;…;pn)∈P,满足OP;ar[P]小= 工作是针对迹语义建立基于语义的有效性度量，目 O[FL(P);var[P].即算法FL是保O可观察语义 的是为了建立有效性度量.而本文建立了证明代码 等价性， 迷惑的有效性的理论框架，有效性度量只是有效性 代码迷惑有效性比较框架的主要目的就是证明 比较框架中的一部分，需要的话，可以在建立的属性 迷惑算法的有效性.因此下面需要证明压平算法的 空间上选择不同的有效性度量；其次，Dalla使用静 有效性.基于压平算法的形式化描述，根据有效性命 态分析模型化反迷惑1)，其中一个重要定理是：如 题2可以证明压平算法的有效性定理。 果静态分析得到的元素是格的顶元，那么称迷惑针 定理2.压平算法有效性.对任意p∈uco(Σ·)， 对该静态分析是有效的，根据本文的有效性命题1 满足偏序关系(P)二(FL(P)).即FL(P)是针对 和命题2知这个定理是显然的；最后，在有效性度量 任意分析算法都是有效的. 的选择方面，Dalla扩展了Collberg提出的评价迷 这样，基于我们提出的代码迷惑有效性比较框 惑效果的potency性质，提出使用变换前后分析结 架，就完成了对压平算法的有效性证明，完成了压平 果的不等来定义有效性度量，这实际是认为如果变 算法的实例化过程. 换影响了原本的抽象域就称为有效的，按照代码迷 需要注意的是，为了简化代码迷惑有效性框架 惑的定义，理解难度的增加应该是指抽象域发生了 的说明，这里的实例化是针对单个算法，比较的是单 偏序变化，也就是导致分析降低了精度，Dalla的有 个算法的对语义分析结果的影响，当然，也可以使用 效性无法刻画程序变换给语义带来的是降低了精度 有效性比较框架来针对不同的算法进行类似地实例 或是提高了精度，这样的有效性度量是不准确的.其 化，从而严格地比较算法之间的有效性。 它还有许多有效性度量的研究，Collbergt]使用软 件工程中评测软件品质的软件复杂性尺度作为度 5 相关工作比较 量，如程序文本中的程序长度，程序中出现的函数调 用数目：使用程序中语法语义结构的图属性作为度 目前还缺乏从形式语义的角度来进行代码迷惑 量，这些图通常是程序语法和语义构造的可视化反 有效性证明的研究，一些其它角度的有效性研究包 映，如程序控制流图、过程调用图、各种标注信息的 括：Wang和Ogiso采用反迷惑算法的计算复杂度 依赖图等，有效性是通过图的属性差异来比较，如边 来证明代码迷惑的有效性[2].通过证明使用静态分 的总数、图的圈数等 析迷惑后程序的控制流问题可以转化成线性有界图 灵机(LBTM)可接受问题，而LBTM可接受问题是 6 结束语 PSPACE-complete的，从而推导出使用静态分析 获得原程序的攻击过程是PSPACE-complete的. 本文使用抽象解释作为统一的框架来表示迷惑 Barak)最早从密码分析的复杂性角度来分析代码 算法和模型化攻击者，从语义的角度建立了代码迷 迷惑的有效性，建立了代码迷惑的密码分析框架.该 惑有效性比较框架.许多研究已经证明了代码迷惑 框架的核心部分是：定义虚拟黑盒属性，形式化了代 作为安全方法的局限性，而本文的工作给出了积极 码迷惑的要求.Lynn]推广了Barak的结论，证明 的结果，为证明限定环境下的代码迷惑安全性提供 了更大一类代码迷惑无法完全保证信息的安全.这 了有益的讨论
４３ 定理的证明 根据我们提出的代码迷惑有效性比较框架，实例 化压平算法的过程还需要证明两个基本的定理：保证 代码迷惑正确性的可观察语义等价性定理以及说明 代码迷惑有效性的代码迷惑有效性定理．限于篇幅， 我们这里只给出定理的形式，而略去具体证明过程， 这并不影响我们说明建立代码迷惑比较框架的过程， 详细的证明过程可以查阅我们的网站（ｈｔｔｐ：／／ｓｓｇ． ｕｓｔｃｓｚ．ｅｄｕ．ｃｎ／ｐｕｂｌｉｃａｔｉｏｎ／ｊｓｊ０６＿ｐｒｏｏｆ．ｄｏｃ）． 定理１． 压 平 算 法 可 观 察 语 义 等 价 性．给 定 任意犘（狆１；狆２；…；狆狀）∈ #，满 足 %!犘；狏犪狉!犘""＝ %!犉犔（犘）；狏犪狉!犘""．即算法犉犔 是保%可观察语义 等价性． 代码迷惑有效性比较框架的主要目的就是证明 迷惑算法的有效性．因此下面需要证明压平算法的 有效性．基于压平算法的形式化描述，根据有效性命 题２可以证明压平算法的有效性定理． 定理２． 压平算法有效性．对任意φ∈狌犮狅（Σ）， 满足偏序关系φ（犘）!φ（犉犔（犘））．即犉犔（犘）是针对 任意分析算法都是有效的． 这样，基于我们提出的代码迷惑有效性比较框 架，就完成了对压平算法的有效性证明，完成了压平 算法的实例化过程． 需要注意的是，为了简化代码迷惑有效性框架 的说明，这里的实例化是针对单个算法，比较的是单 个算法的对语义分析结果的影响，当然，也可以使用 有效性比较框架来针对不同的算法进行类似地实例 化，从而严格地比较算法之间的有效性． ５ 相关工作比较 目前还缺乏从形式语义的角度来进行代码迷惑 有效性证明的研究，一些其它角度的有效性研究包 括：Ｗａｎｇ和 Ｏｇｉｓｏ采用反迷惑算法的计算复杂度 来证明代码迷惑的有效性［２３］ ．通过证明使用静态分 析迷惑后程序的控制流问题可以转化成线性有界图 灵机（ＬＢＴＭ）可接受问题，而 ＬＢＴＭ 可接受问题是 ＰＳＰＡＣＥｃｏｍｐｌｅｔｅ的，从 而 推 导 出 使 用 静 态 分 析 获得原程序的攻击过程 是 ＰＳＰＡＣＥｃｏｍｐｌｅｔｅ的． Ｂａｒａｋ［５］最早从密码分析的复杂性角度来分析代码 迷惑的有效性，建立了代码迷惑的密码分析框架．该 框架的核心部分是：定义虚拟黑盒属性，形式化了代 码迷惑的要求．Ｌｙｎｎ［６］推广了 Ｂａｒａｋ 的结论，证明 了更大一类代码迷惑无法完全保证信息的安全．这 些证明都不是基于语义模型，只是分析迷惑算法给 反迷惑分析算法带来分析时间上的影响．类似的，基 于密码理论的迷惑算法有效性研究也只是分析反迷 惑算法的分析时间与所花费的控制，而无法从分析 的结果来证明代码迷惑带来的影响． 本文建立了证明代码迷惑有效性的理论框架， 目的是为代码迷惑有效性的比较提供与语言无关的 平台，其中的有效性证明依赖于有效性度量的定义． 关于有效性度量的研究，Ｄａｌｌａ［１４１５］的工作与我们的 工作比较接近．简要比较二者的不同：首先，Ｄａｌｌａ的 工作是针对迹语义建立基于语义的有效性度量，目 的是为了建立有效性度量．而本文建立了证明代码 迷惑的有效性的理论框架，有效性度量只是有效性 比较框架中的一部分，需要的话，可以在建立的属性 空间上选择不同的有效性度量；其次，Ｄａｌｌａ使用静 态分析模型化反迷惑［１４］，其中一个重要定理是：如 果静态分析得到的元素是格的顶元，那么称迷惑针 对该静态分析是有效的，根据本文的有效性命题１ 和命题２知这个定理是显然的；最后，在有效性度量 的选择方面，Ｄａｌｌａ扩展了 Ｃｏｌｌｂｅｒｇ提出的评价迷 惑效果的ｐｏｔｅｎｃｙ性质，提出使用变换前后分析结 果的不等来定义有效性度量，这实际是认为如果变 换影响了原本的抽象域就称为有效的，按照代码迷 惑的定义，理解难度的增加应该是指抽象域发生了 偏序变化，也就是导致分析降低了精度，Ｄａｌｌａ的有 效性无法刻画程序变换给语义带来的是降低了精度 或是提高了精度，这样的有效性度量是不准确的．其 它还有许多有效性度量的研究，Ｃｏｌｌｂｅｒｇ［１］使用软 件工程中评测软件品质的软件复杂性尺度作为度 量，如程序文本中的程序长度，程序中出现的函数调 用数目；使用程序中语法语义结构的图属性作为度 量，这些图通常是程序语法和语义构造的可视化反 映，如程序控制流图、过程调用图、各种标注信息的 依赖图等，有效性是通过图的属性差异来比较，如边 的总数、图的圈数等． ６ 结束语 本文使用抽象解释作为统一的框架来表示迷惑 算法和模型化攻击者，从语义的角度建立了代码迷 惑有效性比较框架．许多研究已经证明了代码迷惑 作为安全方法的局限性，而本文的工作给出了积极 的结果，为证明限定环境下的代码迷惑安全性提供 了有益的讨论． ５ 期 高 鹰等：基于抽象解释的代码迷惑有效性比较框架 ８１３
814 计 算 机 学 报 2007年 mation frameworks by abstract interpretation//Proceedings 参考文献 of the ACM SIGPLAN Conference on Principles of Program- ming Languages.Portland Oregon.2002:178-190 [9]Cousot P.Cousot R.Abstract interpretation:A unified lat- [1]Collberg C.Clark T.Douglas L.A taxonomy of obfuscating tice model for static analysis of program by construction or transformations.Department of Computer Science,the Uni- approximation of fixpoints//Proceedings of the ACM SIGP. versity of Auckland:Technical Report #148,1997 LAN on Principles of Programming Languages.Los Angel- [2]Wang C X.A security architecture for survivability mecha- es.California.1977:238-252 nisms[Ph.D.dissertation].University of Virginia.Depart- [10] Gregory Wroblewski.General method of program code ob- ment of Computer Science,2000 fuscation[Ph.D.dissertation].Wroclaw University of Tech- [3]Ogiso T.Sakabe Y.Software obfuscation on a theoretical nology.Institute of Engineering Cybernetics.2002 basis and its implementation.IEEE Transactions on Funda- [11]Chen Yi-Yun,Zhang Yu.Theory of Compiler.Beijing: mentals,2003,E86-A(1):176-186 Higher Education Press,2003(in Chinese) [4]Douglas L.Protecting java code via code obfuscation.ACM (陈意云，张昱.编译原理.北京：高等教有出版社，2003) Crossroads,1998,4(3):21-23 [12]Li Yong-Xiang,Chen Yi-Yun.Technique of code obfuscation [5]Barak B.Goldreich O.Impagliazzo R.Rudich S.Sahai A. based on function pointer array.Chinese Journal of Comput- Vadhan S P.Yang K.On the (im)possibility of obfuscating ers,2004,27(12):1706-1711(in Chinese) programs//Kilian J ed.Proceedings of the 21st Annual Inter- (李永祥，陈意云.基于函数指针数组的代码迷惑技术.计算 national Cryptology Conference on Advances in Cryptology. 机学报，2004,27(12)：1706-1711) Santa Barbara.California:Springer-Verlag.2001.19-23: [13] Cousot P.Constructive design of a hierarchy of semantics of 1-18 a transition system by abstract interpretation.Theoretical [6]Lynn Benjamin.Manoj P.Amit S.Positive results and tech- Computer Science,2002,277(1-2):47-103 niques for obfuscation//Proceedings of the EuroCRYPT.In- [14]Dalla Preda M,Giacobazzi R.Semantic-based code obfusca- terlaken.Switzerland.2004:20-39 tion by abstract interpretation//Proceedings of the ICALP'05. [7]Lee B.Larry D.Self-protecting mobile agents obfuscation Lisbon,Portugal,2005:1325-1336 technique evaluation report.Network Associates Laborato- [15]Dalla Preda M.Giacobazzi R.Control code obfuscation by ries:Report #01-036.2002 abstract interpretation//Proceedings of the SEFM'05.Kobl- [8]Cousot P.Cousot R.Systematic design of program transfor- benz,Germany,2005:301-310 GAO Ying,born in 1980.Ph.D. CHEN Yi-Yun,born in 1946.professor,Ph.D.super- candidate.His research interests include visor.His research interests include theory and implementa- theory and implementation of program- tion of programming language,formal description technolo- ming language and the security of mobile gies,and software security. host. Background This research is supported by the National Natural Sci-many researches have shown the limitation of code obfusca- ence Foundation of China(grant No.60473068).Code Obfus- tion as a security method.which puts the application of code cation is a program transformation for the purpose of increas- obfuscation into doubt.Therefore,how to measure and ing the difficulty of program understanding.It is a useful prove the efficiency of code obfuscation is an important prob- method to guarantee the security in mobile agent and protect lem.The contribution of this paper is to present a new for- the program from reverse engineering.At present,the inter- mal framework for proving the efficiency of code obfuscation ests on code obfuscation focus on two major aspects:The algorithm.Based on abstract interpretation framework,the construction of code obfuscation algorithm and the proof of authors construct the comparable code obfuscation frame- its efficiency.Although the construction of code obfuscation work,which can formally prove its efficiency under the limit- algorithm grows more mature.the proof of its efficiency is ed environment of static analysis and compare the efficiency still blank in the formal semantic foundation.Meanwhile, among code obfuscation algorithms
参 考 文 献 ［１］ ＣｏｌｌｂｅｒｇＣ，ＣｌａｒｋＴ，ＤｏｕｇｌａｓＬ．Ａｔａｘｏｎｏｍｙｏｆｏｂｆｕｓｃａｔｉｎｇ ｔｒａｎｓｆｏｒｍａｔｉｏｎｓ．ＤｅｐａｒｔｍｅｎｔｏｆＣｏｍｐｕｔｅｒＳｃｉｅｎｃｅ，ｔｈｅＵｎｉ ｖｅｒｓｉｔｙｏｆＡｕｃｋｌａｎｄ：ＴｅｃｈｎｉｃａｌＲｅｐｏｒｔ＃１４８，１９９７ ［２］ ＷａｎｇＣＸ．Ａｓｅｃｕｒｉｔｙａｒｃｈｉｔｅｃｔｕｒｅｆｏｒｓｕｒｖｉｖａｂｉｌｉｔｙｍｅｃｈａ ｎｉｓｍｓ［Ｐｈ．Ｄ．ｄｉｓｓｅｒｔａｔｉｏｎ］．ＵｎｉｖｅｒｓｉｔｙｏｆＶｉｒｇｉｎｉａ，Ｄｅｐａｒｔ ｍｅｎｔｏｆＣｏｍｐｕｔｅｒＳｃｉｅｎｃｅ，２０００ ［３］ ＯｇｉｓｏＴ，ＳａｋａｂｅＹ．Ｓｏｆｔｗａｒｅｏｂｆｕｓｃａｔｉｏｎｏｎａｔｈｅｏｒｅｔｉｃａｌ ｂａｓｉｓａｎｄｉｔｓｉｍｐｌｅｍｅｎｔａｔｉｏｎ．ＩＥＥＥ ＴｒａｎｓａｃｔｉｏｎｓｏｎＦｕｎｄａ ｍｅｎｔａｌｓ，２００３，Ｅ８６Ａ（１）：１７６１８６ ［４］ ＤｏｕｇｌａｓＬ．Ｐｒｏｔｅｃｔｉｎｇｊａｖａｃｏｄｅｖｉａｃｏｄｅｏｂｆｕｓｃａｔｉｏｎ．ＡＣＭ Ｃｒｏｓｓｒｏａｄｓ，１９９８，４（３）：２１２３ ［５］ ＢａｒａｋＢ，ＧｏｌｄｒｅｉｃｈＯ，ＩｍｐａｇｌｉａｚｚｏＲ，ＲｕｄｉｃｈＳ，ＳａｈａｉＡ， ＶａｄｈａｎＳＰ，ＹａｎｇＫ．Ｏｎｔｈｅ（ｉｍ）ｐｏｓｓｉｂｉｌｉｔｙｏｆｏｂｆｕｓｃａｔｉｎｇ ｐｒｏｇｒａｍｓ／／ＫｉｌｉａｎＪｅｄ．Ｐｒｏｃｅｅｄｉｎｇｓｏｆｔｈｅ２１ｓｔＡｎｎｕａｌＩｎｔｅｒ ｎａｔｉｏｎａｌＣｒｙｐｔｏｌｏｇｙ Ｃｏｎｆｅｒｅｎｃｅｏｎ Ａｄｖａｎｃｅｓｉｎ Ｃｒｙｐｔｏｌｏｇｙ． ＳａｎｔａＢａｒｂａｒａ，Ｃａｌｉｆｏｒｎｉａ：ＳｐｒｉｎｇｅｒＶｅｒｌａｇ，２００１，１９２３： １１８ ［６］ ＬｙｎｎＢｅｎｊａｍｉｎ，ＭａｎｏｊＰ，ＡｍｉｔＳ．Ｐｏｓｉｔｉｖｅｒｅｓｕｌｔｓａｎｄｔｅｃｈ ｎｉｑｕｅｓｆｏｒｏｂｆｕｓｃａｔｉｏｎ／／ＰｒｏｃｅｅｄｉｎｇｓｏｆｔｈｅＥｕｒｏＣＲＹＰＴ．Ｉｎ ｔｅｒｌａｋｅｎ，Ｓｗｉｔｚｅｒｌａｎｄ，２００４：２０３９ ［７］ ＬｅｅＢ，ＬａｒｒｙＤ．Ｓｅｌｆｐｒｏｔｅｃｔｉｎｇ ｍｏｂｉｌｅａｇｅｎｔｓｏｂｆｕｓｃａｔｉｏｎ ｔｅｃｈｎｉｑｕｅｅｖａｌｕａｔｉｏｎｒｅｐｏｒｔ．Ｎｅｔｗｏｒｋ ＡｓｓｏｃｉａｔｅｓＬａｂｏｒａｔｏ ｒｉｅｓ：Ｒｅｐｏｒｔ＃０１０３６，２００２ ［８］ ＣｏｕｓｏｔＰ，ＣｏｕｓｏｔＲ．Ｓｙｓｔｅｍａｔｉｃｄｅｓｉｇｎｏｆｐｒｏｇｒａｍｔｒａｎｓｆｏｒ ｍａｔｉｏｎｆｒａｍｅｗｏｒｋｓｂｙａｂｓｔｒａｃｔｉｎｔｅｒｐｒｅｔａｔｉｏｎ／／Ｐｒｏｃｅｅｄｉｎｇｓ ｏｆｔｈｅＡＣＭＳＩＧＰＬＡＮＣｏｎｆｅｒｅｎｃｅｏｎＰｒｉｎｃｉｐｌｅｓｏｆＰｒｏｇｒａｍ ｍｉｎｇＬａｎｇｕａｇｅｓ．ＰｏｒｔｌａｎｄＯｒｅｇｏｎ，２００２：１７８１９０ ［９］ ＣｏｕｓｏｔＰ，ＣｏｕｓｏｔＲ．Ａｂｓｔｒａｃｔｉｎｔｅｒｐｒｅｔａｔｉｏｎ：Ａｕｎｉｆｉｅｄｌａｔ ｔｉｃｅｍｏｄｅｌｆｏｒｓｔａｔｉｃａｎａｌｙｓｉｓｏｆｐｒｏｇｒａｍ ｂｙｃｏｎｓｔｒｕｃｔｉｏｎｏｒ ａｐｐｒｏｘｉｍａｔｉｏｎｏｆｆｉｘｐｏｉｎｔｓ／／ＰｒｏｃｅｅｄｉｎｇｓｏｆｔｈｅＡＣＭ ＳＩＧＰ ＬＡＮｏｎＰｒｉｎｃｉｐｌｅｓｏｆＰｒｏｇｒａｍｍｉｎｇＬａｎｇｕａｇｅｓ．ＬｏｓＡｎｇｅｌ ｅｓ，Ｃａｌｉｆｏｒｎｉａ，１９７７：２３８２５２ ［１０］ Ｇｒｅｇｏｒｙ Ｗｒｏｂｌｅｗｓｋｉ．Ｇｅｎｅｒａｌｍｅｔｈｏｄｏｆｐｒｏｇｒａｍｃｏｄｅｏｂ ｆｕｓｃａｔｉｏｎ［Ｐｈ．Ｄ．ｄｉｓｓｅｒｔａｔｉｏｎ］．ＷｒｏｃｌａｗＵｎｉｖｅｒｓｉｔｙｏｆＴｅｃｈ ｎｏｌｏｇｙ，ＩｎｓｔｉｔｕｔｅｏｆＥｎｇｉｎｅｅｒｉｎｇＣｙｂｅｒｎｅｔｉｃｓ，２００２ ［１１］ Ｃｈｅｎ ＹｉＹｕｎ，Ｚｈａｎｇ Ｙｕ．Ｔｈｅｏｒｙ ｏｆ Ｃｏｍｐｉｌｅｒ．Ｂｅｉｊｉｎｇ： ＨｉｇｈｅｒＥｄｕｃａｔｉｏｎＰｒｅｓｓ，２００３（ｉｎＣｈｉｎｅｓｅ） （陈意云，张 昱．编译原理．北京：高等教育出版社，２００３） ［１２］ ＬｉＹｏｎｇＸｉａｎｇ，ＣｈｅｎＹｉＹｕｎ．Ｔｅｃｈｎｉｑｕｅｏｆｃｏｄｅｏｂｆｕｓｃａｔｉｏｎ ｂａｓｅｄｏｎｆｕｎｃｔｉｏｎｐｏｉｎｔｅｒａｒｒａｙ．ＣｈｉｎｅｓｅＪｏｕｒｎａｌｏｆＣｏｍｐｕｔ ｅｒｓ，２００４，２７（１２）：１７０６１７１１（ｉｎＣｈｉｎｅｓｅ） （李永祥，陈意云．基于函数指针数组的代码迷惑技术．计算 机学报，２００４，２７（１２）：１７０６１７１１） ［１３］ ＣｏｕｓｏｔＰ．Ｃｏｎｓｔｒｕｃｔｉｖｅｄｅｓｉｇｎｏｆａｈｉｅｒａｒｃｈｙｏｆｓｅｍａｎｔｉｃｓｏｆ ａｔｒａｎｓｉｔｉｏｎｓｙｓｔｅｍ ｂｙａｂｓｔｒａｃｔｉｎｔｅｒｐｒｅｔａｔｉｏｎ．Ｔｈｅｏｒｅｔｉｃａｌ ＣｏｍｐｕｔｅｒＳｃｉｅｎｃｅ，２００２，２７７（１２）：４７１０３ ［１４］ ＤａｌｌａＰｒｅｄａ Ｍ，ＧｉａｃｏｂａｚｚｉＲ．Ｓｅｍａｎｔｉｃｂａｓｅｄｃｏｄｅｏｂｆｕｓｃａ ｔｉｏｎｂｙａｂｓｔｒａｃｔｉｎｔｅｒｐｒｅｔａｔｉｏｎ／／ＰｒｏｃｅｅｄｉｎｇｓｏｆｔｈｅＩＣＡＬＰ′０５． Ｌｉｓｂｏｎ，Ｐｏｒｔｕｇａｌ，２００５：１３２５１３３６ ［１５］ ＤａｌｌａＰｒｅｄａ Ｍ，ＧｉａｃｏｂａｚｚｉＲ．Ｃｏｎｔｒｏｌｃｏｄｅｏｂｆｕｓｃａｔｉｏｎｂｙ ａｂｓｔｒａｃｔｉｎｔｅｒｐｒｅｔａｔｉｏｎ／／ＰｒｏｃｅｅｄｉｎｇｓｏｆｔｈｅＳＥＦＭ′０５．Ｋｏｂｌ ｂｅｎｚ，Ｇｅｒｍａｎｙ，２００５：３０１３１０ 犌犃犗犢犻狀犵，ｂｏｒｎｉｎ１９８０，Ｐｈ．Ｄ． ｃａｎｄｉｄａｔｅ．Ｈｉｓｒｅｓｅａｒｃｈｉｎｔｅｒｅｓｔｓｉｎｃｌｕｄｅ ｔｈｅｏｒｙａｎｄｉｍｐｌｅｍｅｎｔａｔｉｏｎｏｆｐｒｏｇｒａｍ ｍｉｎｇｌａｎｇｕａｇｅａｎｄｔｈｅｓｅｃｕｒｉｔｙｏｆｍｏｂｉｌｅ ｈｏｓｔ． 犆犎犈犖犢犻犢狌狀，ｂｏｒｎｉｎ１９４６，ｐｒｏｆｅｓｓｏｒ，Ｐｈ．Ｄ．ｓｕｐｅｒ ｖｉｓｏｒ．Ｈｉｓｒｅｓｅａｒｃｈｉｎｔｅｒｅｓｔｓｉｎｃｌｕｄｅｔｈｅｏｒｙａｎｄｉｍｐｌｅｍｅｎｔａ ｔｉｏｎｏｆｐｒｏｇｒａｍｍｉｎｇｌａｎｇｕａｇｅ，ｆｏｒｍａｌｄｅｓｃｒｉｐｔｉｏｎｔｅｃｈｎｏｌｏ ｇｉｅｓ，ａｎｄｓｏｆｔｗａｒｅｓｅｃｕｒｉｔｙ． 犅犪犮犽犵狉狅狌狀犱 ＴｈｉｓｒｅｓｅａｒｃｈｉｓｓｕｐｐｏｒｔｅｄｂｙｔｈｅＮａｔｉｏｎａｌＮａｔｕｒａｌＳｃｉ ｅｎｃｅＦｏｕｎｄａｔｉｏｎｏｆＣｈｉｎａ（ｇｒａｎｔＮｏ．６０４７３０６８）．ＣｏｄｅＯｂｆｕｓ ｃａｔｉｏｎｉｓａｐｒｏｇｒａｍｔｒａｎｓｆｏｒｍａｔｉｏｎｆｏｒｔｈｅｐｕｒｐｏｓｅｏｆｉｎｃｒｅａｓ ｉｎｇｔｈｅｄｉｆｆｉｃｕｌｔｙｏｆｐｒｏｇｒａｍ ｕｎｄｅｒｓｔａｎｄｉｎｇ．Ｉｔｉｓａｕｓｅｆｕｌ ｍｅｔｈｏｄｔｏｇｕａｒａｎｔｅｅｔｈｅｓｅｃｕｒｉｔｙｉｎｍｏｂｉｌｅａｇｅｎｔａｎｄｐｒｏｔｅｃｔ ｔｈｅｐｒｏｇｒａｍｆｒｏｍｒｅｖｅｒｓｅｅｎｇｉｎｅｅｒｉｎｇ．Ａｔｐｒｅｓｅｎｔ，ｔｈｅｉｎｔｅｒ ｅｓｔｓｏｎｃｏｄｅｏｂｆｕｓｃａｔｉｏｎｆｏｃｕｓｏｎｔｗｏ ｍａｊｏｒａｓｐｅｃｔｓ：Ｔｈｅ ｃｏｎｓｔｒｕｃｔｉｏｎｏｆｃｏｄｅｏｂｆｕｓｃａｔｉｏｎａｌｇｏｒｉｔｈｍａｎｄｔｈｅｐｒｏｏｆｏｆ ｉｔｓｅｆｆｉｃｉｅｎｃｙ．Ａｌｔｈｏｕｇｈｔｈｅｃｏｎｓｔｒｕｃｔｉｏｎｏｆｃｏｄｅｏｂｆｕｓｃａｔｉｏｎ ａｌｇｏｒｉｔｈｍｇｒｏｗｓｍｏｒｅｍａｔｕｒｅ，ｔｈｅｐｒｏｏｆｏｆｉｔｓｅｆｆｉｃｉｅｎｃｙｉｓ ｓｔｉｌｌｂｌａｎｋｉｎｔｈｅｆｏｒｍａｌｓｅｍａｎｔｉｃｆｏｕｎｄａｔｉｏｎ．Ｍｅａｎｗｈｉｌｅ， ｍａｎｙｒｅｓｅａｒｃｈｅｓｈａｖｅｓｈｏｗｎｔｈｅｌｉｍｉｔａｔｉｏｎｏｆｃｏｄｅｏｂｆｕｓｃａ ｔｉｏｎａｓａｓｅｃｕｒｉｔｙｍｅｔｈｏｄ，ｗｈｉｃｈｐｕｔｓｔｈｅａｐｐｌｉｃａｔｉｏｎｏｆｃｏｄｅ ｏｂｆｕｓｃａｔｉｏｎｉｎｔｏ ｄｏｕｂｔ．Ｔｈｅｒｅｆｏｒｅ，ｈｏｗ ｔｏ ｍｅａｓｕｒｅ ａｎｄ ｐｒｏｖｅｔｈｅｅｆｆｉｃｉｅｎｃｙｏｆｃｏｄｅｏｂｆｕｓｃａｔｉｏｎｉｓａｎｉｍｐｏｒｔａｎｔｐｒｏｂ ｌｅｍ．Ｔｈｅｃｏｎｔｒｉｂｕｔｉｏｎｏｆｔｈｉｓｐａｐｅｒｉｓｔｏｐｒｅｓｅｎｔａｎｅｗｆｏｒ ｍａｌｆｒａｍｅｗｏｒｋｆｏｒｐｒｏｖｉｎｇｔｈｅｅｆｆｉｃｉｅｎｃｙｏｆｃｏｄｅｏｂｆｕｓｃａｔｉｏｎ ａｌｇｏｒｉｔｈｍ．Ｂａｓｅｄｏｎａｂｓｔｒａｃｔｉｎｔｅｒｐｒｅｔａｔｉｏｎｆｒａｍｅｗｏｒｋ，ｔｈｅ ａｕｔｈｏｒｓｃｏｎｓｔｒｕｃｔｔｈｅｃｏｍｐａｒａｂｌｅｃｏｄｅｏｂｆｕｓｃａｔｉｏｎｆｒａｍｅ ｗｏｒｋ，ｗｈｉｃｈｃａｎｆｏｒｍａｌｌｙｐｒｏｖｅｉｔｓｅｆｆｉｃｉｅｎｃｙｕｎｄｅｒｔｈｅｌｉｍｉｔ ｅｄｅｎｖｉｒｏｎｍｅｎｔｏｆｓｔａｔｉｃａｎａｌｙｓｉｓａｎｄｃｏｍｐａｒｅｔｈｅｅｆｆｉｃｉｅｎｃｙ ａｍｏｎｇｃｏｄｅｏｂｆｕｓｃａｔｉｏｎａｌｇｏｒｉｔｈｍｓ． ８１４ 计 算 机 学 报 ２００７年