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.可观察语义.它是指程序中针对某些性，能够保守地反映程序的性质．许多研究者［１４，７，１０］ 都采用静态分析建立攻击模型．因此，除不可计算语 义信息外，也需要采用静态分析得到的语义信息来 度量有效性． 采用静态分析得到的语义信息来刻画有效性， 是指对迷惑前和迷惑后程序进行分析，如果得到的 分析集合变得更加庞大，则称迷惑算法是有效的．因 为迷惑使得静态分析工具只能得到平凡的结果． 使用流图语言给出一个简单的例子，来解释基 于静态分析结果的有效性定义：关于流图语言的定 义见第４节 程序 ＯＰ为：犔１：狓··＝？→犔２； 犔２：狔··＝１→犔３；犔３：狔··＝狔狓→犔ｅｘｉｔ； 在程 序 中 插 入 一 段 死 代 码，犔３ 处 的 分 支 条 件 ｆａｌｓｅ表示犔５是不会被执行到的，得到变换后的程序 ＯＰ′为 犔１：狓··＝？→犔２；犔２：狔··＝１→犔３； 犔３：ｔｒｕｅ→犔４；犔４：狔··＝狔狓→犔ｅｘｉｔ； 犔３：ｆａｌｓｅ→犔５；犔５：狓··＝１→犔ｅｘｉｔ． 到达定值分析的目的是分析程序中的赋值信 息［１１］，我们将看到死代码插入会导致分析结果精度 的下降． 针对程序点 犔ｅｘｉｔ入口处，来分析比较变换前程 序 ＯＰ和变换后程序 ＯＰ′的分析结果： 对于程序 ＯＰ，分析得到的集合为 犔ｅｘｉｔ｛（狓，犔１），（狔，犔２）｝， 其中，犔ｅｘｉｔ｛（狓，犔１）｝表示在程序点犔ｅｘｉｔ的入口处存在 着对狓的赋值，括号里的第二个元素表示赋值发生 的程序点． 对于变 换 后 程 序 ＯＰ′，分 析 得 到 的 集 合 增 大 为犔ｅｘｉｔ｛（狓，犔１），（狓，犔４），（狔，犔３）｝，是变换前在该程 序点分析集合的超集．而且进一步计算整个程序的 定值集合就能发现，变换后程序的分析集合也是变 换前程序的分析集合的超集．所以，死代码变换是一 种代码迷惑，死代码变换对于到达定值分析来说是 有效的． ３ 建立代码迷惑有效性比较框架 首先简要介绍抽象解释［９］ ．经典抽象解释是一 种针对计算机系统语义模型的近似理论．抽象解释 为不可计算语义建立了安全可靠的近似语义，通过 可计算的近似语义来达到描述不可计算的语义的目 的．主要思想是对给定的程序设计语言赋予具体和 抽象两种语义，将不可计算语义定义成具体语义，将 可计算的语义定义成抽象语义，然后建立二者间的 正确性联系，通过对可计算的抽象语义的求解来达 到保守地计算不可计算语义的目的．后面我们将会 给出不可计算语义和可计算语义的例子．下面给出 抽象解释的主要组成部分，抽象解释存在许多等价 描述，本文使用与程序分析联系比较紧密的伽罗瓦 联系来描述抽象解释框架． 定义２． 伽罗瓦联系．完全偏序集〈!，!〉与完 全偏序集〈!＃，!＃〉满足伽罗瓦联系（ＧａｌｏｉｓＣｏｎｎｅｃ ｔｉｏｎ），是指存在抽象函数α：! → !＃ 以及具体函数 γ：!＃ → !，犡∈!，犡＃∈!＃，满足关系： α（犡）｜＃ 犡＃犡｜γ（犡＃）． 伽罗瓦联系也记为 〈!，!〉←→ α γ 〈!＃，!＃〉． 对程序语言"中的程序#，给出组成抽象解释框 架两种语义的定义． 定义３． 具体语义．具体语义论域是由偏序集 合〈"，!犮〉构成，其中!犮是定义在集合"上的偏序， #∈#→ "，是基于语言"语法构造的到域"上的指 称，称为具体域"上的具体语义函数，具体语义函数 就构成了程序的具体语义． 定义４． 抽象语义．抽象语义论域是由偏序集 合〈$，!犪〉构成，其中!犪 是定义在集合$ 上的偏序， #犪 ∈#→ $ 是基于语言"语法构造的到域$ 上的指 称，称为抽象域$ 上的抽象语义函数，抽象语义函数 就构成了程序的抽象语义． 通常，为保证求解终止性，具体域和抽象域需要 具有比偏序集更强的性质．下面提到的语义论域都 是指完全偏序或是完全格．通过寻找伽罗瓦联系，建 立具体域和抽象域间的联系： 〈"，!犮〉←→ α γ 〈$ ，!犪〉 （１） 在建立了论域间的伽罗瓦联系后，抽象语义通 过式子#犪 ＝α#建立了对具体语义的抽象． 这样就建立了抽象解释框架，抽象解释框架只 考虑语义之间的正确性联系，而忽略语义定义的细 节，因此具体语义和抽象语义是通用的概念，需要根 据不同的应用对二者进行实例化，下面给出几组需 要用到的抽象解释框架下的实例． 定义５． 标准语义．它是指定义语言的动态语 义，通常是指对语言的标准指称解释，其中标准语义 论域由偏序集〈"犛，!犛〉组成，#犛：# → "犛为标准语 义函数． 定义６． 可观察语义．它是指程序中针对某些 ８０８ 计 算 机 学 报 ２００７年