随着软件规模的日益扩大,在软件调试和测试阶段所投入的成本已经上升到总投入的60%以上^[1],其中,对程序执行路径的分析是软件调试和测试阶段的重要内容.为了能够高效地分析程序行为特征等信息,研究人员通过生成测试用例的方式来对程序的执行路径进行分析;同时,对执行路径进行比较,以识别不可行的近邻路径条件、构建代码的行为特征和轮廓.近邻路径的生成方法已经成为程序动态分析领域的重点和难点问题.

近邻路径的生成方法主要包括静态分析方法和动态分析方法.

静态分析方法通过构造程序的控制流图(control flow graph,简称CFG)分析程序执行路径在CFG中所经过的节点来生成近邻的路径集合.文献^[2]使用静态反汇编的分析方法,以程序的基本块(basic block)为单位进行分析,该方法通过记录数据的起始地址和访问地址来进行路径的相似性比对.由于该方法需要进行反汇编分析,故对反汇编的准确性提出了较高的要求;同时,程序中的循环结构在CFG中的表示方法也会对静态分析的精度产生直接的影响.静态分析需要对程序的执行语义进行抽象,其抽象语义是完整程序语义的近似,导致抽象过程具有较大的计算开销,故在实际分析过程中具有较多的限制.

动态分析方法通过分析程序的执行序列来生成近邻的执行路径,主要方法为计算序列的编辑距离,代表性的工作为Bayer等人提出的可伸缩的程序分析方法^[3],该方法采用污点跟踪技术提取程序的执行序列,通过与执行路径关联的输入数据进行路径的相似性比对.现有的动态分析方法虽然比静态分析方法有明显的优势,但在实际分析过程中,传统的符号执行(symbolic execution,简称SE)^[4]等路径生成方法仅仅通过改变路径谓词的方法来改变路径的执行轨迹,对于因路径分支增加而出现的程序状态空间爆炸问题缺乏有效的分析手段,故在针对目标路径所生成的近邻路径集合中,由于缺乏路径引导信息而包含了较多的冗余路径或无关的路径.

针对以上问题,本文提出一种基于协同式逆向分析的k近邻路径生成方法,通过使用后向符号分析方法分析CFG语句中变量的取值范围,以生成程序的输入集合.最弱前置条件(weakest precondition,简称WP)^[5]作为一种后向符号分析方法,可以对程序结构进行建模并分析其执行语义,通过对程序中每条语句的后置断言和该语句表达式的计算,生成该语句的最弱前置条件,即,当前语句的输入集合.符号执行工具在最弱前置条件信息的引导下,可以有效地减少因枚举CFG所有路径而出现的无效路径过多的问题,生成与目标路径近邻的可行路径集合.为了量化路径之间的近邻程度,通过引入因子k来计算路径之间的距离.通过调整k的取值,可以生成与目标路径的编辑距离不超过设定值的路径集合.在最弱前置条件计算过程中,循环结构的分析对计算结果有直接的影响,在一定程度上,CFG中循环结构的执行次数可以通过因子k来表示.故,本文的方法相对于传统的最弱前置条件方法有较好的适应性.

本文的第1节介绍国内外相关的研究进展.第2节介绍与本文相关的概念,着重分析最弱前置条件的性质.第3节讨论k近邻路径的生成方法.第4节为实验结果与分析.最后总结全文.

程序分析的目标是验证程序所具有的性质,例如指定语句的可达性、多线程程序中的变量之间是否存在互斥或竞争等.传统的人工分析方法要求研究人员理解程序的功能、结构、语义,并采用合理的研究方法,故分析效率较低.目前的程序分析都采用自动化或半自动化的分析方法,如定理证明^[6]、模型检测^[7]、约束求解^[8]等.程序分析中的一个重要问题就是近邻路径的生成问题,通过分析程序输入变量的取值范围,使用改变路径谓词的方法,使程序沿着指定的路径执行.

目前的近邻路径分析方法主要有静态的程序结构比较方法和动态的程序行为比较方法.

静态的程序结构分析方法通常采用反汇编等方法对程序进行分析,常用的反汇编分析工具有IDA Pro,Objdump等.文献^[9]通过比较程序中系统调用的地址的方法来分析路径的相似性.文献^[10]从程序中的函数与调用图的角度来判断程序的相似性.文献^[2]以基本块为单位来比较代码的相似性,然后通过分析操作数据的地址以及访问长度的方法进行扩展,该方法对于有较大范围改动的代码的分析效率较低.文献^[11]也以基本块为单位进行分析,通过分析程序的控制流图,并采用符号执行的方法对程序的执行语义进行分析,但是由于缺乏对循环变量等关键数据结构的处理,从而使分析的结果不够精确.由于静态的分析方法在处理复杂数据结构方面效率较低,且缺乏对程序的执行语义和程序上下文逻辑关系的分析,在代码相似性分析和近邻路径生成方面有较大的局限性.

动态的程序行为比较方法相对于静态的分析方法有明显的优势,它通过监控程序中敏感数据的状态信息和可能的流动来对程序的行为进行相似性比较,可以对更加复杂的程序数据结构和行为特征进行有效的分析(例如路径混淆或者代码加壳等).文献^[12]通过分析程序状态的变化来描述程序的执行语义,同时提取执行序列以比较执行的相似程度.PSE^[13]通过程序过程间的后向符号分析来对程序中的路径条件进行计算,但该方法产生的路径条件并不完备,对执行路径的生成有一定的影响.ESC/Java^[14]通过定理证明的方法分析执行语句的前置条件和后置条件对当前语句的影响,但该方法需要通过手动插桩的方法来引导路径的分析.DSD-Crasher^[15]从生成程序反例的角度分析路径的相似性,但该方法在生成最弱前置条件过程中可能受到其他变量的影响而导致路径条件不可解.文献^[16]使用符号执行和最弱前置条件相结合的分析方法引导相似执行路径的生成,但是缺乏对最弱前置条件的约简分析.相对于以上方法,本文的方法通过对程序中循环变量谓词等关键数据结构的分析,使用后置条件和语句的语义信息生成对应的最弱前置条件,并逐步逆向分析到程序的起始位置,获得程序输入变量的有效输入域;再以最弱前置条件为引导信息,采用符号执行的方法生成与指定路径近邻的路径集合,同时通过距离因子k来调整生成的近邻路径与目标路径的编辑距离.与传统的符号执行方法相比,本文的方法有更好的灵活性,且生成的路径集合的冗余度和可行路径的比例有明显的优势.

定义1(控制流图(control flow graph,简称CFG)). 程序的控制流图可以形式化地表示为(N,E,s,f),它是由若干节点和边组成的有向图,其中,N为节点的集合,E为边的集合,s为起始节点,f为出口节点.控制流图是程序执行序列的抽象表示,每个节点nÎN代表一个基本块,包含了顺序语句、循环语句、条件语句等;边的集合E=NxN反映了基本块之间的控制流关系,每一个控制流图均有唯一的起始节点s和出口节点f.

定义2(关联变量(related variable)). 记控制流图中与节点n相关联的节点集合为N_r={n_i|án_i,nñÎE,án,n_iñÎ E},其中,N_r所包含的语句集合记为Stmt(N_r).Stmt(N_r)中的变量组成的集合即为节点n的关联变量,记为Rel(n).

定义3(路径条件(path condition,简称PC)). 在控制流图中,通过改变条件语句和循环语句的关键谓词可以产生新的路径,故路径条件是控制流在迭代操作过程中所产生的数据流值.条件语句集合S或循环语句集合L在判定节点n处的路径条件定义为PC(n)={v|vÎRel(n)ÙStmt(n)ÎS,vÎRel(n)ÙStmt(n)ÎL},故路径条件实际上是由路径变量所组成的一阶逻辑公式.

定义4(静态单赋值(static single assignment,简称SSA)). 静态单赋值通过修改变量a在每次定义时的下标(a₀,a₁,…)以使得程序中的每个变量都有唯一的一处定义,可以提高数据流分析和程序优化的效率和精度.在控制流图中,通过加入j函数节点:a=j(a₀,a₁,…)来实现变量的定义和使用,即“定义-使用链(use-define chain)”,能够更加精确地描述变量的定义和使用之间的关系.在对程序的符号变量进行分析的过程中,通过使用静态单赋值的分析方法,可以消除控制流图中冗余的依赖关系,并区分关联变量的定义、使用和在内存中的地址.在对循环语句等复杂数据结构进行分析的过程中,由于控制流图具有单一的起始节点和出口节点,故当循环结构出现异常情况时,则在控制流图中有一条指向出口节点的边,以提高符号分析处理异常退出情况的能力.

定义5(最弱前置条件(weakest precondition,简称WP)). 在验证程序所具有的属性过程中,每一条语句的前后都有一个由变量的逻辑表达式所组成的约束条件,语句中的变量依据执行语义必须满足对应的约束条件.其中,语句前面的谓词是程序在当前语句中变量的约束条件,即前置条件;相应地,语句后面的谓词是语句执行后所满足的新的约束条件,即后置条件.在后向符号分析过程中,通过已知的后置条件来推理当前语句的前置条件,其中,最弱前置条件是确保一条语句在正常执行后能够使得后置条件有效的最小前提条件.在实际分析过程中,最后一条执行语句的后置条件是程序变量在执行完时的输出域.通过该后置条件和程序最后一条执行语句来计算其最弱前置条件,该前置条件又作为上一条语句的后置条件.通过这样的迭代计算,一直到控制流图的起始节点.

下面通过对程序中最常见的语句形式:赋值语句、顺序语句、分支语句和循环语句的诠释来分析最弱前置条件的表示形式.对于赋值语句x=E,设Q是其后置条件,则前置条件P可以定义为P=Q_x®E,表示为{Q_x®E}x=E{Q}.在计算过程中,使用E来替换所有x的实例,即,使用函数j[x/E]来表示该替换过程.在控制流图中,若一个节点有出边,则会使用相应的j函数来执行替换操作.在实际分析过程中,往往会出现已知的前置条件和经过计算所得出的前置条件不一致的情况,故对于断言P和P¢,若P¢逻辑蕴含P:P¢P,可以使用以下形式来表示推理的过程:

({P}S{Q},P¢P,QQ¢)({P¢}S{Q¢}).

对于相邻的顺序语句S₁和S₂,设S₁和S₂的前置条件和后置条件具有如下形式:{P₁}S₁{P₂},{P₂}S₂{P₃},则顺

序语句的推理规则为({P₁}S₁{P₂},{P₂}S₂{P₃})({P₁}S₁,S₂{P₃}).该规则表明:经计算所得到的第2条语句的前置

条件可以作为第1条语句的后置条件,从而得到第1条语句的前置条件.具体地,对于赋值语句序列S₁:x₁=E₁,S₂:x₂=E₂,其前置条件和后置条件按照计算的顺序可以表示为

即,语句序列S₁和S₂在后置条件P₃的作用下得到的最弱前置条件为

分支语句的形式可以表示为if Exp then S₁ else S₂,由于布尔表达式Exp的真值可能为True或False,故需要分析then和else两个分支条件,其推理规则为

({ExpÙP}S₁{Q},{ØExpÙP}S₂{Q})({P} if Exp then S₁ else S₂{Q}).

由于循环语句循环体的执行次数受制于循环条件的取值,故循环体执行的次数决定了不同的执行路径.循环语句中的最弱前置条件是通过循环不变式的计算来获得的,循环不变式的取值不受循环条件和循环体中语句的影响.循环语句的语义可以表示为{P} while Exp do S end {Q},前置条件P使得循环体在结束循环时,后置条件Q是可满足的.对于循环不变式I,循环语句的推理规则为({IÙExp}S{I})({I} while Exp do S end {IÙØExp}),循环语句的最弱前置条件必须使得循环不变式I为真,同时,I必须使得后置条件是可满足的.循环结构需要以下条件是可满足的:PI,{IÙExp}S{I},(IÙØExp)Q.在实际分析过程中,通过循环体的执行来计算前置条件, 由于循环不变式I往往需要通过归纳法来获得,通常情况下,前置条件P可以作为循环不变式I,故I需要对后置条件进行弱化,同时使得控制流图中循环体的起始节点在循环开始时是可满足的,且在退出循环体时,循环体出口节点的后置条件也是可满足的.

在最弱前置条件的计算过程中,谓词转换函数wp用来将当前语句和谓词转换为另一个谓词,即wp(Stmt,Q)=P.当程序中出现赋值语句时,则在最弱前置条件计算过程中需要使用j函数来实现相应的转换.由于最弱前置条件是一种后向符号分析方法,需要将控制流图的出口节点语句和后置条件作为转换函数wp的参数,通过计算来获得其前置条件.该算法从出口基本块开始逐步迭代到入口基本块,所经过的节点的后置条件均转换为可以求解的最弱前置条件.算法中使用变量List来表示待求解的后置条件集合,当迭代求解到起始节点时,List集合里面的后置条件均经过转换函数wp处理为对应的最弱前置条件,故该循环的终止条件是List集合为空.其中,simplify函数的作用是对约束条件集合进行约简操作,将不可解的谓词条件从集合中排除.常见的约简有:

· (x≤y)Ù(x¹y)®x<y;

· (typeOf(x)=T)Ù(x=null)®false;

· subType(a,t₁)ÙsubType(a,t₂)ÙsubType(t₁,t₂)®subType(a,t₁).

传统的程序调用图(call graph)在构建过程中直接通过分析过程调用来实现,但不可避免地会分析大量重复的过程调用,导致调用图中存在冗余的边.故在最弱前置条件计算过程中,本文以待分析的控制流图中的节点为驱动,通过最弱前置条件分析的结果为引导,生成与待分析节点相关的精简的程序调用图.算法1为加入后向符号分析的程序调用图的生成算法.

算法1. 带过程间最弱前置条件的程序调用图生成算法.

Input: CFG,j_post;

Output: Call graph under wp.

callGraphWithWP(CFG,j_post)

1. var CG¬wp(CFG,j_post);

2. var CG¢¬{cgÎCG|cg can be solved};

3. if CG¢=Æ

4. foreach mÎCG do

5. select one method from m;

6. select sÏsubroutines in methodÙ(mÙmethod=s can be solved);

7. if s does not exist

8. continue;

9. endif

10. CFG¢¬CFG+s;

11. return callGraphWithWP(CFG¢,j_post);

12. endfor

13. else

14. return CG¢;

最弱前置条件在计算过程中所遵守的语法为:

Program::=Block+

Block::=BlockId:Stmt; goto BlockId*

Stmt::=Stmt; Stmt|VarId:=Exp|assert Exp|assume Exp|skip

程序由若干个控制流图中的基本块组成,每个基本块由若干条语句组成,每个基本块有唯一的基本块号BlockId以快速定位基本块中的语句.assert用来判断表达式Exp是否成立,assume用来判断当前语句Exp是否可达.在控制流图中,记起始节点为s,出口节点为f,则程序中的语句可以使用定义的语法进行表示.例如,对于分支语句if Exp then S₁ else S₂,可以转换为:

start: skip; goto then,else

then: assume Exp; S₁; goto End

else: assume ØExp; S₂; goto End

end

对于语句S,其前置条件P和后置条件Q、最弱前置条件的计算可以通过转换函数wp(S,Q)来获得,在最弱前置条件所遵守的语法中,前置条件的计算为:

wp(assert P,Q)=PÙQ

wp(assume P,Q)=PÙQ

wp(S₁;S₂,Q)=wp(S₁,wp(S₂,Q))

对于分支语句,有wp(S₁ or S₂,Q)=wp(S₁,Q)Ùwp(S₂,Q)^[17].在实际分析过程中,最弱前置条件通过当前语句及其后置条件经转换函数wp计算获得,即wp(Stmt,post-condition)=precondition,故后置条件是前置条件计算过程中的重要参数,图 1为程序的控制流图以及对应语句的后置条件.

为体现分支语句可能的执行路径,图 1(a)中省略了条件语句的判断条件.程序经过静态单赋值(SSA)操作后,每个变量在对其进行定义的语句中,通过增加下标的方式进行改名.这样,每个变量均有唯一的一处定义.在图 1(b)中,若语句10是可满足的,即存在约束S₀=0ÙS₁=S₀+1ÙS₂=S₁+1ÙS₂>8,其中,每个节点的左侧标记了对应的后置条件t₁:s₀≤0;t₂:s₀≤0;t₅:s₁≤1;t₆:s₁≤1;t₉:s₂≤2.在图 1(c)中,通过改变节点5的取值,使得路径约束条件为S₀=0ÙS₁=S₀+1ÙS₂=S₁+2,通过判断该符号状态与后置条件t₉:s₂≤2的逻辑包含关系,来判断程序的路径可行性.同理,在图 1(d)中,通过改变节点1的取值来进行程序性质的验证.

图 1

Fig. 1

Fig. 1 Control flow graph with post-condition图 1 带后置条件的控制流图

在符号分析过程中,对循环结构的分析精度会直接影响到执行路径生成的效率,由于符号执行的方法在分析过程中可能会出现状态空间爆炸的问题,故通常使用抽象的方法来计算循环不变式I,使得符号执行具有一个有限的状态空间,并通过循环不变式和循环表达式的析取操作来产生新的循环控制条件.在控制流图中,循环体的出口节点有一条指向循环体入口节点的回边,即存在由循环体中的节点所组成的环结构.

图 2为对一个带循环的程序进行符号分析以及对循环结构的处理过程.

图 2

Fig. 2

Fig. 2 Example of loop structurepost-condition图 2 循环结构分析示例

图 2(b)为程序的部分控制流图,其中,语句1和语句2以及语句4和语句5均用同一个节点标记.当程序执行图 2(b)所示的执行轨迹时,经静态单赋值操作后,路径条件为

lock₀=0Ùnew₀=old₀+1Ù(new₀!=old₀)Ùlock₁=1Ùold₁=new₀.

注意到图 2(b)上部的节点3处的变量状态为lock₀=0,new₀=old₀+1,当循环体完成第1次迭代时,变量状态为lock₁=1Ùold₁=new₀.此时,可以对变量状态进行抽象操作,即:

D(lock₀=0flock₁=1)=true,D(new₀=old₀+1fold₁=new₀)=true.

其中,Δ为抽象函数.这样,图 2(b)下部的节点3有一条指向上部节点3的回边.此时,由于old₁=new₀,故循环条件不可满足.此时的路径条件为lock₀=0Ùnew₀=old₀+1Ùnew₀=old₀,由于其不可解,故在图 2(d)中在下部的节点3处继续对循环体进行迭代分析.

程序中的循环结构分析主要有线性循环分析和非线性循环分析,本文主要针对非线性循环的执行条件进行研究.对于具有n维非线性多项式约束条件的循环结构,有如下定理.

定理1. 对于n维空间中的一个集合A,映射XaF(X),XÎA.对于循环体中的赋值语句X=F(X),若条件

k||X-F(X)||≥||F(X)-F²(X)||,0<k<10是可满足的^[18],则对于循环结构存在输入X,使得程序循环条件恒为真的充要条件是F(X)在A上存在不动点.

证明:

· 首先对必要性进行证明.

当程序循环判断条件恒为真时,对于循环体存在如下无穷迭代序列:

s={X₀,X₁,X₂,…,X_n,…}={F(X₀),F²(X₀),F³(X₀),…}ÍA.

设i>j,

由于,故存在不动点x,使得故:

· 证明充分性.

若F(X)在A上存在不动点x,由于F ⁱ(x)=xÎA对于任意的i均成立,即循环判断条件恒为真.证毕.

定义6(编辑距离(edit distance)). 对于两个字符串S和T,若其中一个字符串经过一系列插入、删除、替换操作可以转换为另一个字符串,其操作次数最少的数值用来定义这两个字符串的编辑距离.实际分析过程中,使用动态规划的方法来对编辑距离进行计算,其动态规划公式为:

· i==0 && j==0,edit(i,j)=0;

· i==0 && j>0,edit(i,j)=j;

· i>0 && j==0,edit(i,j)=i;

· i>0 && j>0,edit(i,j)=min(edit(i-1,j)+1,edit(i,j-1)+1,edit(i-1,j-1)+f(i,j)).

其中,

· 函数edit(i,j)用来计算S的子串[0...i]与T的子串[0...j]之间的编辑距离;

· 函数f(i,j)用来计算S[i]转换到T[j]所需要的操作次数,若S[i]!=T[j],则f(i,j)=1;否则,f(i,j)=0.

为了对所生成路径的相似程度进行量化分析,通过计算编辑距离的方法分析两条执行路径之间的相似程度,因子k用来记录编辑距离的值.对于路径l和与其编辑距离不超过k的路径集合L:

L={e|eÎPathsÙΔ(l,e)≤k},

其中,算子Δ用来计算编辑距离.WP的定义如下:WP:{(s,pc,path,k)ÎProgxPCxPathsxk→PC},其中,(s,pc,path,k)为经过后向符号分析后所生成的新的路径条件.通过SMT求解器,可以得到路径l所对应的输入变量的近似值,其中,s为目标路径,pc为与s对应的路径条件.当k的取值为0时,本文方法分析当前路径的最弱前置条件,用来生成目标路径的最弱前置条件,表示为WP(Prog,PC,Paths,k)=WP(s,pc,path);当对k的取值没有限制,即k→¥时,由于取消了距离因子的限制,本文的方法即为传统的最弱前置条件分析方法,用来生成从该节点开始进行逆向分析以生成所有节点的最弱前置条件,表示为.一般情况下,当kÎ(0,¥)时,在距离因子k的作用下生成与当前路径的距离不超过k的路径集合表示为

WP(Prog,PC,Paths,k)=Ú_lÎLWP(l,j).

经过最弱前置条件分析后,可以生成变量的输入域I^WP.但依据该变量所生成的近邻路径集合中可能存在不可行的路径,即,执行路径不包含控制流图的出口节点.对于程序Prog,其运行过程可以表示为输入集合I到输出结合O上的映射:I→O.设程序的后置条件为Q,Prog在输入i(iÎI)上的执行过程可以表示为Prog(i)Q.为了分析输入域与程序执行语义间的依赖问题,我们引入如下定义.

定义7(无效输入域I^infea={i|iÎI,Prog(i)ØQ}). 它表示程序Prog在输入域I上的所有可行的路径均不能使后置条件Q得以满足.对于该无效的输入域,需要从最弱前置条件所生成的输入域中删除.相应地,经过删除操作后所生成的有效输入域I^infea可以表示为I^fea={i|iÎI^wp\I^infea,Prog(i)Q}.在距离因子k的作用下,经后向符号分析所得的变量的输入域I^wp与输入集合I的关系为之间的关系如图 3所示,其中,

I^feaÈI^infea=I^wp.

图 3

Fig. 3

Fig. 3 Relationship between the input areas图 3 几种输入域之间的关系

对于不同的距离因子k₁和k₂,使用后向符号分析所生成的输入域为I₁和I₂,符号执行工具在该输入域上所生成的路径在程序控制流图的出口节点处对应的后置条件为Q₁和Q₂,称k₁比k₂更优当且仅当如下条件成立:

(k₁fk₂)Û(Q₁®Q₂ÙI₁ÍI₂).

在最优距离因子k的计算过程中,不同k的取值会使得控制流图中每个节点的最弱前置条件可能有所不同,控制流图的规模随着程序规模的扩大而扩大,故在实际分析过程中,往往需要对控制流图进行必要的压缩.本文依据控制流图节点的最弱前置条件对控制流图中的节点进行等价类划分,将具有相同的最弱前置条件的节点合并为压缩的控制流图中的一个节点,同时删除这些节点之间的边.下面给出控制流图中节点的等价关系的定义.

定义8. 控制流图G上的等价关系是节点集合V上的二元关系,若节点u和v是等价的:uºv,当且仅当P(u)= P(v)且Q(u)=Q(v),其中,P和Q分别为节点的前置条件和后置条件.等价关系满足传递性、对称性、自反性,故符号º描述了节点集合V上的等价关系.

如图 4所示,图 4(a)为原始的符号分析树,图 4(b)和图 4(c)为经压缩操作后的控制流图,具体的压缩规则为:对于控制流图G(V,E)中的节点u和v,其中,u,vÎE,áu,vñÎE,节点2和节点4由于有相同的前驱节点(节点1)和后继节点(节点6和节点7),故节点2和节点4可以合并为同一个节点,同时删除节点中重复的边.由于在最弱前置条件计算过程中已经对循环结构进行了相应的预处理,故删除从节点7到节点5的边,如图 4(b)所示.同理,节点6和节点7具备合并的条件,从而压缩后的控制流图如图 4(c)所示.故G中不存在环结构.

图 4

Fig. 4

Fig. 4 Example of the compression of CFG图 4 控制流图的压缩示例

对于节点u,设与其有相同前置条件和后置条件的节点集合为U={x|xÎV,uºx},即,U为包含节点u的等价类节点.设经过压缩的控制流图为G¢(V¢,E¢),在G¢的基础上所生成的近邻路径集合S(G¢)与在原始的控制流图G上生成的近邻路径集合S(G)是等价的,即,S(G¢)=S(G).下面将对其正确性进行证明.

定理2. 在G¢中,节点u,v的等价类节点分别为U与V,其中,UÌU¢,VÌV¢,若áu,vñÎE¢成立,当且仅当对于任意的节点u,v,有áu,vñÎE成立,其中,{áu,vñ|uÎU,vÎV}.

证明:该定理的充分性是显然的,下面对必要性进行证明.

对于节点uÎU,vÎV,因U中任意两个节点的后置条件是相同的,故对于节点u_iÎU,有áu_i,vñÎE;因V中任意两个节点的前置条件是相同的,故对于节点u_iÎU,v_iÎV,有áu_i,v_iñÎE,从而有áu,vñÎE成立.证毕.

定理3. 在原始的控制流图G中,记节点u和v之间的最短距离为D,在压缩的控制流图G¢中,节点u和v的等价类节点分别为U和V,对于u_iÎU,v_iÎV,有D(G,u,v)=D(G¢,u_i,v_i).

证明:记节点u和v之间的路径l:u®n₁®n₂®…®n_D-1®v,对于路径l中的任意两个节点n_i和n_j,记其对应的在G¢中的等价类节点分别为N_i和N_j,都有N_i¹N_j,则l¢:U®N_i®N_i+1®…®N_i+(D-1)®V是一条u和v之间长度为D的路径,其中,N_i+1为n_i的后继节点对应的等价类集合.因为若不成立,则存在节点N_i和N_j使得N_i=N_j.从而,节点N_i和N_j有相同的后置条件.故从节点u开始,有一条路径u®n₁®…®n_i®n_j+1®…®n_D-1®v到达v.故该路径不是节点u和v之间的最短路径,与假设相矛盾.故在G¢中也存在一条U和V之间长度为D的路径.假设G¢中在节点U和V中存在一条路径U®K₁®K₂®…®K_k®V,其中,k为该路径的长度,使得k<D,对于áK₁,…,K_kñ中的某一分量ák₁,…,k_kñ,根据定理2,有ák_i,k_i+1ñÎE,0<i<k,从而在G中的节点u和v之间存在一条长度为k的路径.这是错误的,故l¢为G¢中节点u和v之间的最短路径.证毕.

通过构建程序的控制流图,并使用后向符号分析方法对当前节点的执行语义和后置条件进行计算,获得对应的最弱前置条件,并逐渐迭代到控制流图的起始节点.在该过程中,距离因子k的取值作用于循环结构和分支结构,从而对最弱前置条件的结果产生影响.本节通过实验来讨论本文方法的有效性,我们使用WALA作为实验开发平台,通过对平台提供的T.J.Watson Libraries工具进行修改,使其具备后向符号分析功能.符号分析工具采用Java PathFinder,约束求解器使用CVC3.Java PathFinder从控制流图的起始节点,在最弱前置条件的作用下生成与出口节点后置条件相关的近邻路径集合;CVC3在最弱前置条件和Java PathFinder分析过程中,能实时计算各循环节点和分支节点处的由路径谓词组成的约束条件,通过计算约束条件的可解性来分析当前路径的可行性.本文的整体分析流程如图 5所示.

图 5

Fig. 5

Fig. 5 Procedure of the analysis图 5 整体分析流程

图 5中,前端(front end)对程序进行预处理,使用GCC作为程序的编译器,通过修改配置文件中的预处理选项编译生成中间文件(.I文件),并将该中间文件作为程序分析工具T.J.Watson Libraries的输入.通过对GCC中语法扫描器parse.y中语义动作的修改,生成程序的抽象语法树(AST),在AST的基础上对程序以基本块为单位进行划分,最后构建程序的控制流图.后端(rear end)主要实现对程序中分支结构和循环结构的处理,在距离因子的作用下,通过最弱前置条件的计算来获得程序对应的输入域,并通过符号执行工具和约束求解器来生成基本路径集合,最后,通过判断计算获得的后置条件和设定的后置条件之间的逻辑蕴含关系来判断路径的可行性.本文的实验基于Intel Core i7 3.5GHz的处理器,内存大小为8G,操作系统为Ubuntu 13.10,内核版本为3.11.6.测试基准程序(benchmark)使用DaCapo和常见的开源Java程序,其中,hedc是一款网络爬虫软件,weblech是一款下载工具,lusearch为一款文件索引工具,sunflow是一款照片处理程序,avrora是一款仿真工具,hsqldb为关系数据库的引擎,antlr是一款扫描器生成工具,batik是一款浏览器软件.由于其中有大量的分支语句、循环语句,可以较好地满足方法的使用条件.

ESC/Java是目前路径分析和验证过程中一种最具代表性的方法,它是一种静态Java程序分析器,通过对程序的前置条件和后置条件进行计算分析来获得程序的可行路径,本文将其作为进行对比分析的方法.为了比较ESC/ Java和本文的方法在近邻路径生成方面的性能与耗费,设计了如下实验.

· 实验1:循环结构分析

ESC/Java通过设定循环体执行次数(设为k次)作为上界来生成执行路径,通过对控制流图中的循环体结构进行展开并将其转换为非循环结构,通过在循环展开的节点处插桩相应的引导信息,使得对于不同的k值有不同的路径编码,满足该条件的路径称为k次迭代路径.ESC/Java需要在运行之前就设置k的取值,对于超过k的路径,可能会出现遗漏的现象.在k的不同取值的情况下,测试基准程序中k次迭代路径的数目.表 1为测试基准程序的基本信息以及对循环结构处理后路径条件数量的对比,其中,圈复杂度(cyclomatic complexity,简称CC)用来对程序的复杂程度进行衡量,它的值可以用来表示基本路径的条数,在基本路径集合中通过验证程序后置条件来筛选出可行的路径集合.圈复杂度的值越大,则程序的结构也越复杂,其计算方法为CC(G)=e-n+2,其中,e为CFG中边的个数,n为CFG中节点的个数.路径条件数用来记录在经过预处理后程序中循环节点和分支节点的数目,由于加入了最弱前置条件作为路径生成的引导信息,从而能够及时地对不可解的路径谓词进行分析.从表中可以看出,本文方法在路径条件规模方面比ESC/Java有明显的约简.在时间开销方面,ESC/Java和本文的方法都需要对控制流图中节点的入边进行分析,该过程的时间消耗与控制流图中边的数量呈线性关系.由于本文对控制流图使用邻接表的形式存储,各节点的后继节点按顺序存储,故将最弱条件加入到对应的节点信息中的时间开销与最弱前置条件个数成正比.本文方法在分析过程中将待分析的后置条件进行枚举,并建立待分析节点的后置条件与执行路径的对应关系,在路径执行后,可以通过后置条件来检索对应的执行路径,以提高后置节点到执行路径的转化效率.

表 1(Table 1)

Table 1 Basic information of the benchmark 表 1 测试基准程序的基本信息 测试基准程序 CFG中节点数 CFG中的边数 CFG中循环节点数 圈复杂度 ESC/Java路径条件数 本文方法路径条件数 hedc 392 567 31 177 238 163 weblech 238 314 27 78 125 52 lusearch 129 425 80 298 68 26 sunflow 451 715 192 266 83 67 avrora 96 159 43 65 53 41 hsqldb 181 491 15 312 241 105 antlr 356 636 39 282 152 89 batik 209 370 17 163 73 25

Table 1 Basic information of the benchmark 表 1 测试基准程序的基本信息

随着程序规模的扩大,路径条件也相应地增多,约束求解器在求解过程中不可避免地出现效率较低的情况,故有必要设置相应的溢出处理方法以缓解求解性能的降低.由于本文方法将循环结构进行展开,故一条执行路径中可能包含较多的重复路径片段,我们将这些重复的路径片段与路径条件加以映射,相同的路径条件可以采用编码的操作进行压缩.故本文方法在操作过程中设置了临界点机制,当路径条件出现溢出时,通过记录当前的路径条件和节点位置,同时将路径条件设置为前驱节点的路径条件,对路径条件进行求解、合并,以减少约束求解器运算的开销.图 6为距离因子k与临界点数量的对应关系,对于不同的k值,测试程序的临界点数量最多不超过9个.经实验分析可知,因子k的取值不超过20,因为若继续增大,可能会出现约束求解器资源耗尽或者路径条件分析时间过长等现象.从图中可以看出:临界点数量随着因子k的增长而出现增长幅度放缓的趋势;同时,在临界点数量较少的条件下,可以生成与目标路径的编辑距离最多为20的近邻路径集合.故对于复杂的程序,能够以较低的空间消耗来对近邻路径进行分析.

图 6

Fig. 6

Fig. 6 Relationship between the number of critical point and factor k图 6 临界点数量与因子k的关系

· 实验2:近邻路径生成

本文中,我们引入了加速比(speedup ration)的概念,它表示对于一条待分析的路径,使用ESC/Java的方法和本文的方法在生成可行路径集合时的时间开销的比值,图 7为具体的对比图.从图中可以看出:对于大部分程序,本文的方法在时间开销方面相对于ESC/Java有一定程度的提高;但是对于antlr,出现了时间开销有较大幅度提高的情况,antlr的加速比约为1.17.其原因是:该程序中有较多的赋值语句,导致在预处理阶段中,静态单赋值(SSA)在分析过程中给变量在不同定义处加入下标并构建程序的“定义-使用链”,同时,由于大量赋值语句存在于循环结构当中,导致该过程有较大的时间耗费.另外,该程序的循环结构和分支结构的条件语句中存在较多的全局变量,对程序控制流结构有较大的影响.而在ESC/Java中,由于没有类似的“定义-使用链”,从而其路径敏感程度要弱于本文的方法.虽然在特殊情况下有一定的优势,但在分析精度方面不及本文的方法.

图 7

Fig. 7

Fig. 7 Time consumption comparison图 7 时间耗费对比

在生成的基本路径中,由于有约束求解器的使用,可以将不可解的路径条件进行删除.但受制于约束求解器的求解能力,符号执行工具仍然会生成一部分不可行的路径.图 8显示了ESC/Java和本文的方法在生成可行路径方面的精度对比,从图中可以看出:本文方法由于有后向符号分析所生成的最弱前置条件作为符号执行工具生成近邻路径的引导信息,可以有针对性地生成基本路径集合,在此基础上,通过分析程序在控制流图出口节点处变量的取值,并分析与设定的后置条件的逻辑包含关系来判断该路径的可满足行.测试集中,sunflow的可行相似路径百分比提升的幅度最大,其值为21.9%,测试集的平均提升幅度为14.1%.

图 8

Fig. 8

Fig. 8 Comparison of the analysis precision图 8 分析精度对比

近邻路径生成是程序分析和验证中的主要问题,现有的分析方法直接使用符号执行等方法生成执行路径,但是这种粗粒度的方法由于缺乏必要的路径引导信息而生成较多的冗余路径和无效路径.本文提出一种后向符号分析方法,通过对程序控制流图中循环节点的处理,并使用静态单赋值的方法进行数据流敏感的分析,在此基础上,从控制流图的出口节点开始,使用后置条件和节点的执行语义计算其最弱前置条件,逐步迭代到起始节点,从而获得程序变量的输入域.在此基础上,使用符号执行和约束求解器,在最弱前置条件信息的引导下生成与目标后置条件近邻的路径集合.实验结果表明:本文的方法可以有效减少路径条件的数量,并使用较少的临界点对程序的多次迭代进行有效的分析;同时,对于大部分程序,本文的方法比ESC/Java方法在时间开销方面有一定优势,但是对于有较多赋值语句的程序,由于静态单赋值分析导致在构建“定义-使用链”时有较多的时间耗费,这也是将来工作中需要改进的内容之一.在分析精度方面,由于加入了路径引导信息,本文方法生成的可行路径百分比相对于ESC/Java方法均有较大幅度的提高.

将来的主要工作有:结合目前恶意程序在执行过程中采用代码加壳、路径变换等混淆手段对分析工具进行干扰,故我们可以在本文方法的基础上通过对程序行为轮廓的构建,并使用控制流图比较的方法来对程序的行为特征进行分析,使本文的方法具有更好的适应性.