5期 高鹰等：基于抽象解释的代码迷惑有效性比较框架 807 保护客户代码的目的. 针对目前代码迷惑研究中缺乏基于语义的有效 代码迷惑以前的研究主要集中在构造有效的代 性证明以及缺乏限定环境下有效性证明的问题，本 码迷惑算法.Collbergt)中给出了有关这方面研究 文以代码迷惑引起的语义信息变化来刻画有效性， 比较完整的综述，引入了代码迷惑的定义，代码迷惑 提出了与语言无关的代码迷惑有效性比较框架，能 是一种以增加理解难度为目的的程序变换技术. 够为迷惑算法在静态分析这样的限定环境下提供严 Wang建立了针对恶意主机问题的代码安全体系， 格的有效性证明，也能够严格比较不同迷惑算法之 该安全体系的主要部件基于代码迷惑技术构造， 间的有效性.静态分析作为限定环境是指，攻击者使 而其中迷惑算法的核心思想是破坏程序的控制信 用静态分析作为攻击手段的攻击场景。 息.Ogiso)推广了Wang的算法，不仅破坏程序控 本文第2节概述代码迷惑有效性比较框架组成 制流信息，还进一步地破坏程序过程间的调用信息， 部分；第3节采用抽象解释理论形式化有效性比较 Douglas)针对Java语言的特征，通过构造复杂数 框架；第4节结合具体的迷惑算法描述如何实例化 据结构来增加代码的理解难度，关于构造代码迷惑 有效性比较框架：最后给出相关工作比较和结论. 算法的研究已经比较成熟. 但是，对于构造的代码迷惑算法是否有效，这些 2问题的提出 研究都没有提供严格证明，代码迷惑算法的构造缺 乏有效性证明的理论支持.而另一方面，许多研究已 建立代码迷惑有效性比较框架分两个部分进 经从理论上证明了代码迷惑作为安全方法的局限 行：形式化代码迷惑空间；形式地定义代码迷惑有效 性[5]，即证明了不存在代码迷惑能够完全保证信息 性度量 的安全性，经过迷惑后的代码总还或多或少存在信 第一步，形式化迷惑算法组成的代码迷惑空间. 息泄漏 关于代码迷惑，Collberg)给出了非形式的定义. 尽管在理论上代码迷惑并不能保证高机密信息 定义1.代码迷惑.程序变换τ。是代码迷惑是 的安全，但代码迷惑仍是代码安全问题中一种有效 指：(1)变换x保持程序可观察语义的等价性：(2)经 的安全技术，其原因是在很多场合下它能提供安全 过变换x使得程序某些属性的理解难度增加. 性，因此代码迷惑的研究一直活跃.一些具有代表性 根据上述定义，代码迷惑包含了两个性质，与程 的代码迷惑应用如下： 序变换一样保证程序可观察语义等价以及使得属性 恶意移动代理.移动代理在主机之间移动时， 的理解难度增加.形式化代码迷惑定义，也需要从刻 代码和执行的中间结果可能会被主机恶意获取篡 画这两个性质进行. 改.SPMA[]的研究表明，代码迷惑技术能够保证代 代码迷惑是一类特殊的程序变换，因此与程序 理在其移动存活期内被攻击的难度增加，从而达到 变换同样需要满足正确性性质.程序变换正确性是 保护移动代理的安全，对于恶意攻击者来说，恶意移 指变换前和变换后程序具有可观察语义等价性，由 动代理是一种时间受限环境，因为代理驻留在主机 文献[8]可知，可观察语义是对标准语义的抽象，程 上的时间是有限的。 序变换正确性等价于要求变换前后程序的标准语义 恶意逆向工程，越来越多的代码使用容易被反 在某种层次的抽象下相等，这为定义代码迷惑正确 编译的中间代码发布，使得软件开发者需要更多地 性提供了理论基础.属性是指从程序中提取的信息， 考虑其竞争者可能会反编译发布的代码，进而获取 可以使用上界闭包来刻画町，属性组成的属性空间 软件的设计以及其中的重要算法.虽然代码迷惑技 可定义偏序结构，属性的理解难度增加是通过属性 术无法为代码提供完全保护.但是，代码迷惑能够使 空间上的偏序关系来定义， 攻击者发现：复用反迷惑后得到的代码要比其重写 第二步，给出代码迷惑的有效性度量.代码迷惑 等效代码更加困难。 的有效性证明是基于定义的有效性度量.我们采用 这些都说明代码迷惑能够提供限定环境下的安 语义信息的变化来刻画有效性，通过迷惑前后的语 全性，如上述的时间受限环境以及不可复用环境等， 义信息来度量代码迷惑的有效性.语义信息通常是 限定环境是针对攻击者所处的攻击场景受到某些限 不可计算的，静态分析是对程序语义信息的保守近 制的情况，如在时间受限环境下，攻击者必须在代理 似，静态分析的结果能够可计算地反映语义信息的 存活期内篡改程序，攻击者的攻击时间是受限的. 变化.而且静态分析具有动态分析所不具备的可靠保护客户代码的目的． 代码迷惑以前的研究主要集中在构造有效的代 码迷惑算法．Ｃｏｌｌｂｅｒｇ［１］中给出了有关这方面研究 比较完整的综述，引入了代码迷惑的定义，代码迷惑 是一种以 增 加 理 解 难 度 为 目 的 的 程 序 变 换 技 术． Ｗａｎｇ［２］建立了针对恶意主机问题的代码安全体系， 该安全体系 的 主 要 部 件 基 于 代 码 迷 惑 技 术 构 造， 而其中迷惑算法的核心思想是破坏程序的控制信 息．Ｏｇｉｓｏ［３］推广了 Ｗａｎｇ的算法，不仅破坏程序控 制流信息，还进一步地破坏程序过程间的调用信息． Ｄｏｕｇｌａｓ［４］针对Ｊａｖａ语言的特征，通过构造复杂数 据结构来增加代码的理解难度．关于构造代码迷惑 算法的研究已经比较成熟． 但是，对于构造的代码迷惑算法是否有效，这些 研究都没有提供严格证明，代码迷惑算法的构造缺 乏有效性证明的理论支持．而另一方面，许多研究已 经从理论上证明了代码迷惑作为安全方法的局限 性［５６］，即证明了不存在代码迷惑能够完全保证信息 的安全性，经过迷惑后的代码总还或多或少存在信 息泄漏． 尽管在理论上代码迷惑并不能保证高机密信息 的安全，但代码迷惑仍是代码安全问题中一种有效 的安全技术，其原因是在很多场合下它能提供安全 性，因此代码迷惑的研究一直活跃．一些具有代表性 的代码迷惑应用如下： 恶意移动代理．移动代理在主机之间移动时， 代码和执行的中间结果可能会被主机恶意获取篡 改．ＳＰＭＡ［７］的研究表明，代码迷惑技术能够保证代 理在其移动存活期内被攻击的难度增加，从而达到 保护移动代理的安全．对于恶意攻击者来说，恶意移 动代理是一种时间受限环境，因为代理驻留在主机 上的时间是有限的． 恶意逆向工程．越来越多的代码使用容易被反 编译的中间代码发布，使得软件开发者需要更多地 考虑其竞争者可能会反编译发布的代码，进而获取 软件的设计以及其中的重要算法．虽然代码迷惑技 术无法为代码提供完全保护．但是，代码迷惑能够使 攻击者发现：复用反迷惑后得到的代码要比其重写 等效代码更加困难． 这些都说明代码迷惑能够提供限定环境下的安 全性，如上述的时间受限环境以及不可复用环境等． 限定环境是针对攻击者所处的攻击场景受到某些限 制的情况，如在时间受限环境下，攻击者必须在代理 存活期内篡改程序，攻击者的攻击时间是受限的． 针对目前代码迷惑研究中缺乏基于语义的有效 性证明以及缺乏限定环境下有效性证明的问题，本 文以代码迷惑引起的语义信息变化来刻画有效性， 提出了与语言无关的代码迷惑有效性比较框架，能 够为迷惑算法在静态分析这样的限定环境下提供严 格的有效性证明，也能够严格比较不同迷惑算法之 间的有效性．静态分析作为限定环境是指，攻击者使 用静态分析作为攻击手段的攻击场景． 本文第２节概述代码迷惑有效性比较框架组成 部分；第３节采用抽象解释理论形式化有效性比较 框架；第４节结合具体的迷惑算法描述如何实例化 有效性比较框架；最后给出相关工作比较和结论． ２ 问题的提出 建立代码迷惑有效性比较框架分两个部分进 行：形式化代码迷惑空间；形式地定义代码迷惑有效 性度量． 第一步，形式化迷惑算法组成的代码迷惑空间． 关于代码迷惑，Ｃｏｌｌｂｅｒｇ［１］给出了非形式的定义． 定义１． 代码迷惑．程序变换τ狅犫是代码迷惑是 指：（１）变换τ狅犫保持程序可观察语义的等价性；（２）经 过变换τ狅犫使得程序某些属性的理解难度增加． 根据上述定义，代码迷惑包含了两个性质，与程 序变换一样保证程序可观察语义等价以及使得属性 的理解难度增加．形式化代码迷惑定义，也需要从刻 画这两个性质进行． 代码迷惑是一类特殊的程序变换，因此与程序 变换同样需要满足正确性性质．程序变换正确性是 指变换前和变换后程序具有可观察语义等价性．由 文献［８］可知，可观察语义是对标准语义的抽象，程 序变换正确性等价于要求变换前后程序的标准语义 在某种层次的抽象下相等．这为定义代码迷惑正确 性提供了理论基础．属性是指从程序中提取的信息， 可以使用上界闭包来刻画［９］，属性组成的属性空间 可定义偏序结构，属性的理解难度增加是通过属性 空间上的偏序关系来定义． 第二步，给出代码迷惑的有效性度量．代码迷惑 的有效性证明是基于定义的有效性度量．我们采用 语义信息的变化来刻画有效性，通过迷惑前后的语 义信息来度量代码迷惑的有效性．语义信息通常是 不可计算的，静态分析是对程序语义信息的保守近 似，静态分析的结果能够可计算地反映语义信息的 变化．而且静态分析具有动态分析所不具备的可靠 ５ 期 高 鹰等：基于抽象解释的代码迷惑有效性比较框架 ８０７