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节给出属性组成的属性 属性关系表示了具体属性和抽象属性的联系，属性在语义域上的感兴趣的取值，其中"狅是可观察 语义论域，一般与标准语义域〈"犛，!犛〉相同．%：# → "犛为可观察语义函数． 标准语义提供了程序动态运行行为的精确定 义，是其它一切语义模型建立抽象的起点，所有其它 的语义都是对标准语义的抽象．而可观察语义正是 对标准语义某个方面的抽象．若建立了标准语义域 到可观察语义域之间的伽罗瓦联系： 〈"犛，!犛〉→ α ← ０ γ０ 〈"狅，!狅〉 （２） 又因为抽象语义可以通过式子#犪 ＝α# 建立了 对具体语义的抽象，在建立了论域间的伽罗瓦联系 后，可观察语义就可由% ＝α狅#犛 定义． 抽象解释框架应用到静态程序分析时，具体语 义和抽象语义分别实例化成收集语义和分析语义． 定义７． 收集语义．它是指可到达程序动态运行 行为的并集．收集语义论域〈"犮狅犾，!犮狅犾〉，"犮狅犾 !（" 犛），由标准语义论域的幂集组成，#犮狅犾：# → "犮狅犾为收 集语义函数． 定义８． 分析语义．它是指静态分析时基于收 集语义得到的保守语义信息．分析语义论域由偏序 集〈$φ，!φ〉组成，#φ：# → $φ为分析语义函数． 对于静 态 分 析 算 法φ，可 以 建 立 收 集 语 义 域 〈"犮狅犾，!犮狅犾〉到分析语义域〈$φ，!φ〉间的伽罗瓦联系： 〈"犮狅犾，!犮狅犾〉→ α ← φ γφ 〈$φ，!φ〉 （３） 同样，根据论域间建立的伽罗瓦联系，分析语义 可由#φ＝αφ#犮狅犾定义． 对于例子中提到的到达定值分析，我们来看基 于抽象解释框架是如何定义程序分析算法的．首先 是实例化具体语义得到收集语义，通常是到达程序 点的所有状态的并．对于程序 ＯＰ，进入程序点犔３的 状态为｛狓··＝？，狔··＝ ？，狕··＝１｝，这里的状态只包含 了环境中值的映射，因为狓 取值的不确定性，使得 程序点犔３处狔值是不可解的，因此这里的收集语义 是不可计算的．然后是实例化抽象语义得到分析语 义，是通过定义到达定值分析的抽象函数αφ："犮狅犾 → $φ，由收集语义构造得到．限于篇幅，这里不再给出 αφ的形式定义．对于程序 ＯＰ进入程序点犔３的分析 语义是：｛（狓，？），（狔，犔１），（狕，犔２）｝，表示所有到达程 序点犔３的定值信息．分析语义中关心的是定值信 息，程序点犔３处狔 的定值信息是可解的，因此狓 定 值信息的分析是可计算的． 本节主要内容是基于抽象解释框架，建立代码 迷惑有效性比较框架．３．１节给出属性组成的属性 空间的定义．属性是形式化代码迷惑定义所需的， 只有 定 义 了 属 性 才 能 定 义 程 序 理 解 难 度 的 增 加； ３．２节在给出的属性定义的基础上，形式化代码迷 惑组成的迷惑空间；３．３节基于程序分析框架，建立 有效性度量的标准，为比较代码迷惑的有效性提供 语义上的度量． ３１ 建立属性空间 程序在具体域上的取值称为具体属性，在抽象 域上的取值称为抽象属性，通常具体属性都是不可 计算的，需要使用对应的可计算抽象属性来描述具体 属性．具体属性和抽象属性间的联系称为属性关系． 首先给出定义属性空间所需的上界闭包的定义． 定义９． 上界闭包．对于偏序集〈&，!〉，算子 ρ：& → &是上界闭包算子，是指具备以下性质： （１）单 调 的 （ｍｏｎｏｔｏｎｅ）．犘，犙∈ &，犘 !犙， ρ（犘）!ρ（犙）； （２）幂等的（ｉｄｅｍｐｏｔｅｎｔ）．ρρ＝ρ； （３）外延的（ｅｘｔｅｎｓｉｖｅ）．犘∈&，ρ（犘）$犘． 那么，ρ（&）就称为是偏序集 &关于闭包算子ρ 的一个上界闭包．狌犮狅（&）表示偏序集&上的全部上 界闭包算子集合．需要注意的是，许多研究并不区分 上界闭包算子和上界闭包的使用．本文需要区分二者 作为属性关系和属性的定义，所以，又引入犝犆犗（&） 表示偏序集&上的全部上界闭包集合． 抽象域可以使用上界闭包等价地刻画［９］ ．本文 的抽象解释框架是使用伽罗瓦联系定义，因此下面 给出基于伽罗瓦联系的上界闭包算子定义．由伽罗 瓦联系（１），可定义ρ犃＝γα，ρ犃 ∈" → "，得到的ρ犃 就是与抽象域$ 相关的上界闭包算子．对于抽象域 〈$，!犪〉，根据定义的ρ犃，存在关系ρ犃 （"）$，即 ρ犃（"）与$ 具有相同的逻辑含义，具体域的上界闭 包ρ犃（"）是抽象域$ 的同构刻画． 使用上界闭包表示抽象域的好处是，在推导抽 象域上的属性时，无需得到抽象域上的对象，因为对 于抽象域〈$，!犪〉，〈ρ犃（"），!犮〉能同构地反映它的 元素，而ρ犃（"）的构造与抽象域$ 的定义是无关的． 程序的属性空间是由全体具体属性和抽象属性 组成．抽象域可由上界闭包等价刻画，具体域"上所 有抽象域组成的偏序集"犮（"）＝〈犝犆犗（"），!犮〉．由 上界闭包算子的外延性可知："犝犆犗（"），即具体 域"上的元素也属于犝犆犗（"），因此，偏序集"犮就组 成了具体域"的属性空间．犝犆犗（"）上的偏序关系 !犮可以比较属性之间的语义的精度． 属性关系表示了具体属性和抽象属性的联系， ５ 期 高 鹰等：基于抽象解释的代码迷惑有效性比较框架 ８０９