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的结论，证明 的结果，为证明限定环境下的代码迷惑安全性提供 了更大一类代码迷惑无法完全保证信息的安全.这 了有益的讨论４３ 定理的证明 根据我们提出的代码迷惑有效性比较框架，实例 化压平算法的过程还需要证明两个基本的定理：保证 代码迷惑正确性的可观察语义等价性定理以及说明 代码迷惑有效性的代码迷惑有效性定理．限于篇幅， 我们这里只给出定理的形式，而略去具体证明过程， 这并不影响我们说明建立代码迷惑比较框架的过程， 详细的证明过程可以查阅我们的网站（ｈｔｔｐ：／／ｓｓｇ． ｕｓｔｃｓｚ．ｅｄｕ．ｃｎ／ｐｕｂｌｉｃａｔｉｏｎ／ｊｓｊ０６＿ｐｒｏｏｆ．ｄｏｃ）． 定理１． 压 平 算 法 可 观 察 语 义 等 价 性．给 定 任意犘（狆１；狆２；…；狆狀）∈ #，满 足 %!犘；狏犪狉!犘""＝ %!犉犔（犘）；狏犪狉!犘""．即算法犉犔 是保%可观察语义 等价性． 代码迷惑有效性比较框架的主要目的就是证明 迷惑算法的有效性．因此下面需要证明压平算法的 有效性．基于压平算法的形式化描述，根据有效性命 题２可以证明压平算法的有效性定理． 定理２． 压平算法有效性．对任意φ∈狌犮狅（Σ）， 满足偏序关系φ（犘）!φ（犉犔（犘））．即犉犔（犘）是针对 任意分析算法都是有效的． 这样，基于我们提出的代码迷惑有效性比较框 架，就完成了对压平算法的有效性证明，完成了压平 算法的实例化过程． 需要注意的是，为了简化代码迷惑有效性框架 的说明，这里的实例化是针对单个算法，比较的是单 个算法的对语义分析结果的影响，当然，也可以使用 有效性比较框架来针对不同的算法进行类似地实例 化，从而严格地比较算法之间的有效性． ５ 相关工作比较 目前还缺乏从形式语义的角度来进行代码迷惑 有效性证明的研究，一些其它角度的有效性研究包 括：Ｗａｎｇ和 Ｏｇｉｓｏ采用反迷惑算法的计算复杂度 来证明代码迷惑的有效性［２３］ ．通过证明使用静态分 析迷惑后程序的控制流问题可以转化成线性有界图 灵机（ＬＢＴＭ）可接受问题，而 ＬＢＴＭ 可接受问题是 ＰＳＰＡＣＥｃｏｍｐｌｅｔｅ的，从 而 推 导 出 使 用 静 态 分 析 获得原程序的攻击过程 是 ＰＳＰＡＣＥｃｏｍｐｌｅｔｅ的． Ｂａｒａｋ［５］最早从密码分析的复杂性角度来分析代码 迷惑的有效性，建立了代码迷惑的密码分析框架．该 框架的核心部分是：定义虚拟黑盒属性，形式化了代 码迷惑的要求．Ｌｙｎｎ［６］推广了 Ｂａｒａｋ 的结论，证明 了更大一类代码迷惑无法完全保证信息的安全．这 些证明都不是基于语义模型，只是分析迷惑算法给 反迷惑分析算法带来分析时间上的影响．类似的，基 于密码理论的迷惑算法有效性研究也只是分析反迷 惑算法的分析时间与所花费的控制，而无法从分析 的结果来证明代码迷惑带来的影响． 本文建立了证明代码迷惑有效性的理论框架， 目的是为代码迷惑有效性的比较提供与语言无关的 平台，其中的有效性证明依赖于有效性度量的定义． 关于有效性度量的研究，Ｄａｌｌａ［１４１５］的工作与我们的 工作比较接近．简要比较二者的不同：首先，Ｄａｌｌａ的 工作是针对迹语义建立基于语义的有效性度量，目 的是为了建立有效性度量．而本文建立了证明代码 迷惑的有效性的理论框架，有效性度量只是有效性 比较框架中的一部分，需要的话，可以在建立的属性 空间上选择不同的有效性度量；其次，Ｄａｌｌａ使用静 态分析模型化反迷惑［１４］，其中一个重要定理是：如 果静态分析得到的元素是格的顶元，那么称迷惑针 对该静态分析是有效的，根据本文的有效性命题１ 和命题２知这个定理是显然的；最后，在有效性度量 的选择方面，Ｄａｌｌａ扩展了 Ｃｏｌｌｂｅｒｇ提出的评价迷 惑效果的ｐｏｔｅｎｃｙ性质，提出使用变换前后分析结 果的不等来定义有效性度量，这实际是认为如果变 换影响了原本的抽象域就称为有效的，按照代码迷 惑的定义，理解难度的增加应该是指抽象域发生了 偏序变化，也就是导致分析降低了精度，Ｄａｌｌａ的有 效性无法刻画程序变换给语义带来的是降低了精度 或是提高了精度，这样的有效性度量是不准确的．其 它还有许多有效性度量的研究，Ｃｏｌｌｂｅｒｇ［１］使用软 件工程中评测软件品质的软件复杂性尺度作为度 量，如程序文本中的程序长度，程序中出现的函数调 用数目；使用程序中语法语义结构的图属性作为度 量，这些图通常是程序语法和语义构造的可视化反 映，如程序控制流图、过程调用图、各种标注信息的 依赖图等，有效性是通过图的属性差异来比较，如边 的总数、图的圈数等． ６ 结束语 本文使用抽象解释作为统一的框架来表示迷惑 算法和模型化攻击者，从语义的角度建立了代码迷 惑有效性比较框架．许多研究已经证明了代码迷惑 作为安全方法的局限性，而本文的工作给出了积极 的结果，为证明限定环境下的代码迷惑安全性提供 了有益的讨论． ５ 期 高 鹰等：基于抽象解释的代码迷惑有效性比较框架 ８１３