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. 压平后的控制流图 图 ４ 压平算法变换示意图 图５给出压平算法的形式描述．其中κΩ：" # " 是变换前的分支映射函数，映射对Ω＝｛犾１ #犾２；…； 犾狀－１ #犾狀｝．为简化流图语言语法，我们给出的压平 算法没有使用复杂数据结构来构造控制变量，这与 Ｗａｎｇ［２］的压平算法不同，但是简单表达式也是一种 常用的构造迟钝谓词的方法［１］，因此这样的变化并 不影响对原算法的说明． Ｉｎｐｕｔ：程序犘（狆１；狆２；…；狆狀）． 犉犔（犘）＝ （犆ｓｗｉｔｃｈ↓狆犻↓犆ｐｈｉ）， 犻＝１ ｛（犆ｓｗｉｔｃｈ↓狆犻↓犆ｐｈｉ↓犆ｓｋｉｐ）‖犉犔（犘－狆犻），犻＞１ 其中， （１）犆ｓｗｉｔｃｈ＝（犾ｓｗｉｔｃｈ：｛狊狑犞犪狉＝犞犾｝→犾）∧犾＝犾犪犫!狆犻" （２）犆ｐｈｉ＝（狊狌犮（狆犻）：｛狊狑犞犪狉··＝犞犾｝→犾｝）∧（犾＝狀犲狓狋（狆犻）） （３）犆ｓｋｉｐ＝犾ｐｈｉ：狊犽犻狆→犾ｓｗｉｔｃｈ； （４）犉犔（犘－狆犻）＝犘（狆１；…；狆犻－１；狆犻＋１；狆狀） （５）狀犲狓狋（犆）＝κΩ（犾犪犫!犆"） 图 ５ 压平算法的描述 ８１２ 计 算 机 学 报 ２００７年