0 引言

随着软件系统功能和结构的日趋复杂,软件系统的正确性正变得越来越重要,如何保障软件系统的正确性,已成为了工业界和学术界关注的焦点问题^[1-2]。软件验证对于保证软件的正确性有着重要的作用^[3],软件验证的重点是对程序的属性进行分析,例如程序语句是否可达,程序中是否存在数组越界、内存溢出等,以期找出软件中存在的漏洞,并对其进行改正。

路径验证是软件验证中的一个重要问题^[4],通过对程序的每条分支执行路径进行分析验证,可以减少错误误报和漏报的数量,提高验证的准确率。但是在实际验证过程中,往往无法准确获取到程序的每条执行路径,尤其对于路径条数过多或者存在复杂循环路径的程序,由于其路径搜索空间过大,如果直接进行路径遍历,可能会导致路径爆炸问题的出现,影响路径验证的效率和准确率。因此,如何有效减少程序的路径搜索空间,同时保证路径验证的效率和准确率,是进行路径验证时需要解决的关键问题。目前,将路径合并、路径抽象、循环有限次展开等路径处理技术和约束求解器(如布尔可满足问题(Boolean Satisfiability,SAT)求解器和可满足性模理论(Satisfiability Modulo Theory,SMT)求解器)相结合的方法是对这个问题的一种有效的解决方法。如文献^[5]提出对程序进行增量式的分析,利用测试组件来鉴别控制流图(Control Flow Graph,CFG)中在当前程序版本中有过修改的路径,避免对路径进行重复分析；文献^[6]利用路径抽象的方法,将程序中的不同路径抽象成一个约束集,约束集里的约束条件被编码成布尔公式,

并将其输入SAT求解器进行求解；文献^[7]对控制流图进行抽象与细化,通过重用已验证边的条件,结合SMT求解器,从控制流图中提取出满足条件的边,同时剔除干扰边；文献^[8]提出一种路径集中的分析验证方法,首先利用中间语言(Internal Representation,IR)来对程序进行表示,并以此构造控制流图,随后利用抽象解释的方法对控制流节点进行抽象简化,并对循环进行有限次数的展开,最后利用SMT求解器来进行验证；文献^[9]通过对控制流图进行切片和压缩处理,并利用抽象解释的方法对循环部分进行不变式提取,以此来去掉循环路径,最后利用SMT求解器对路径进行编码和验证。

本文在文献^[8]利用IR语言对源程序进行表示和文献^[9]对循环路径提取循环不变式的基础上,考虑到现有方法工具中采用的路径合并和路径抽象等处理方法可能会造成部分路径信息丢失的问题,提出一种基于SMT求解器的程序路径验证方法。方法利用基本路径法来进行路径遍历,通过分析程序控制流图的环形复杂性,将覆盖的路径数压缩到一定范围内,从而降低测试的路径数。由于基本路径法不考虑循环路径,在实际分析过程中,对于循环体只执行零次或一次,这样可能会导致遍历的路径结果无法准确表述整个循环路径的性质。因此,本文方法在进行路径遍历前先对循环路径提取不变式,与文献^[9]中采用的抽象解释方法不同,本文采用决策树方法进行不变式的提取,相对于抽象解释,决策树方法进行不变式提取的速度更快,同时提取不变式的准确率也更高^[10]。对于基本路径的验证,本文利用SMT求解器来进行。SMT求解器是对SAT求解器的扩展,SAT求解器的基础是命题逻辑,而SMT求解器的基础是一阶逻辑,一阶逻辑与命题逻辑的区别在于命题逻辑只考虑逻辑连接词的逻辑特性,不考虑命题本身,而一阶逻辑则是两者兼顾,因此与SAT求解器相比,SMT求解器的求解能力更强。本文先对基本路径信息进行符号执行,提取路径中的约束条件并组成路径的约束条件集合,然后利用SMT求解器进行求解验证。

1 基于SMT求解器的程序路径验证方法

本文方法的主要执行过程如图 1所示。

方法的执行过程分为三部分:

1) 程序预处理。利用底层虚拟机(Low Level Virtual Machine,LLVM)编译器,先将源程序转化为LLVM中间表示(LLVM Internal Representation,LLVM IR)文件,进而对IR文件进行转化,得到源程序对应的控制流图。

2) 对控制流图进行处理。从中提取出程序的基本路径信息。在实际验证过程中,控制流图的边数通常会有几十或几百条,甚至更多,对应的程序路径的数量也会急剧上升,直接造成程序的路径搜索空间过大,影响验证的效率和准确率。为了解决这个问题,本文采用两种手段来进行处理:

①对控制流图中的循环节点进行处理。首先利用决策树的方法对其提取循环不变式,随后利用不变式替换循环节点,构造控制流图对应的无循环控制流图(No-Loop Control Flow Graph,NLCFG),使得因循环导致的复杂路径空间变成简单路径空间。

②利用基本路径法对控制流图进行遍历。通过计算控制流图的环形复杂度,确定程序控制流图的基本路径条数,进而从控制流图中提取出基本路径信息。利用基本路径法缩小测试路径的规模,并减少重复测试的次数。

3)基本路径的验证。首先对基本路径信息进行转化,得到路径信息对应的一阶逻辑公式集合;随后对公式集进行符号执行,从中提取约束条件集合;最后将约束条件转化为SMT-LIB输入,利用SMT求解器进行求解验证,得到最终的路径验证结果。

2 决策树方法提取循环不变式 2.1 循环不变式

循环不变式(loop invariant)由Floyd首次引入^[11],随后Djikstra等^[12]作了更深入的研究,同时给出了算法逻辑上比较严格的定义:循环不变式是指在循环体每次执行前后均为真的断言。

定义1 循环不变式。 在证明循环程序S₀:while B do S时,若有一断言M满足{M∧B}S{M},则称M为循环程序S₀的循环不变式。

循环不变式有三个基本属性:

1) 初始化(Initialization):循环不变式在循环开始前保持正确;

2) 循环执行(Maintenance):循环不变式在循环体每次迭代前保持正确;

3) 循环结束(Termination):循环结束时,循环不变式保持正确。

循环不变式是程序设计理论中的一种重要概念,是对程序的一种抽象表示形式。循环不变式不仅可以用于分析程序的特性,而且可以用于程序验证中,证明循环结构的正确性。

现阶段在循环不变式提取研究中用的较多的是基于迭代不动点计算的方法,如抽象解释^[13]。方法的基本思想是将具体程序变量投影到抽象域,并根据程序描述的具体语义抽象为高层的抽象运算,对抽象域进行不动点的迭代计算,最终对抽象计算出的不动点进行性质判定,判断是否符合要求。这种方法在一定程度上简化了分析过程,但是其本质上属于牺牲精度换取时间,因为不动点计算过程的收敛性是不可判定的,需要采取如放大算子、提高抽象粒度等措施来保证收敛过程,而这些措施会造成一定程度的精度损失。

2.2 基于决策树的循环不变式提取

本文提取循环不变式采用的是决策树方法^[14],将不变式求取问题转化为二元分类问题,有效避免了迭代不动点计算方法过程中由于保证收敛过程而导致的精度损失问题；同时决策树方法属于机器学习方法中的一种分类预测方法,相对于抽象解释方法来说,对于不变式提取的自动化程度更高,相应的提取速度也更快。决策树方法的基本思想是:首先将程序中的循环路径部分提取出来,对其进行输入输出采样和分类;随后对样本点进行主成分分析(Principal Component Analysis,PCA),并选择合适的抽象域来对可能的循环不变式中的变量关系进行抽象表示;接着利用决策树分类方法来对处理过后的样本数据进行分类,并构造对应的决策树模型,通过遍历决策树模型,得到分离样本点的最佳分类表达式,即为候选的不变式;最后,利用循环不变式的三个基本属性对候选不变式进行验证,若满足则候选不变式为所求的循环不变式,若不满足则表示不变式求取失败。基本算法如算法1所示。

算法1 利用决策树方法生成循环不变式。

输入 源程序P。

输出 提取的循环不变式L_p。

begin

1) matrix, flag=Sampler(P)

2) feaVector =PCA( matrix )

3) newMatrix = matrix·feaVector ^T

4) tree=DTTree( newMatrix ) 5) Lp=Formula( tree )

6) if isInvariant( L_p )

7) then Output( L_p )

8) else fail

end

决策树提取不变式算法可概括为三步:

1) 数据样本初始化:主要是输入数据样本的采集与处理(算法第1)~3)行)。首先利用Sampler()方法进行样本点采集及分类,通过执行循环部分代码,得到执行过程中和执行后的变量的值,根据输入输出条件,满足的则将这些值划分到可达点集,不满足的则划分到不可达点集,matrix表示变量值组成的矩阵,flag表示对应的分类标记(0表示不可达点集,1表示可达点集);随后通过PCA()方法求取样本点的特征向量,进行主成分分析前先选取合适的抽象域,这个域中的约束形式能表示不变式中的变量关系,根据选择的抽象域,利用PCA方法求得满足抽象域约束的特征向量。PCA是一种降维分析方法,其基本思想是通过分析找到在原n维空间中的一些特定方向,样本主要集中在这些方向上,特征值的大小反映了样本集在该方向上的集中程度,基于此,删掉特征值小的方向,保留主要的方向,达到降维的目的。这里主要是利用主成分分析方法来获取样本点分布的最主要方向并求得对应的特征向量feaVetor,结合抽象域中的表达式,可以得到分割样本点的最佳表达式;最后将输入数据矩阵matrix与特征向量feaVetor相乘,得到候选不变式的值矩阵newMatrix。

2) 决策树分类:通过对初始化阶段得到的数据矩阵进行决策树模型构造,从中得到分类表达式(算法第4)~5)行)。首先通过DTTree()方法对样本点集构造决策树模型,方法利用分类回归树(Classification And Regression Tree,CART)的算法和思想,将样本点集划分开,并生成对应的分类树tree,分类树的内部节点是每个最佳分类对应的表达式,叶子节点为样本点集所属的类别(0或1);随后利用Formula()方法遍历分类树,得到候选不变式,方法从根节点开始对分类树进行深度优先遍历,将能抵达可达点集对应的叶子节点(即为1)的路径信息添加到队列中,最后得到的队列中的信息即为候选不变式 L_p

3) 不变式验证:对求得的候选不变式进行验证,判断不变式的正确性(算法第6)~8)行)。通过isInvariant()方法检查所求得的不变式是否为正确的不变式,判断标准为2.1节中描述的循环不变式的三个基本属性,满足的则为正确的不变式,不满足则表示不变式求取失败。

3 路径验证 3.1 基本路径的转化

路径验证的第一步是对每条路径信息进行转化,即将路径节点信息从IR表示转化为对应的一阶逻辑表示,为后续的符号执行和约束求解操作作准备。本文对控制流图基本路径信息的转化是基于dot文件进行的,dot文件^[15]中描述了图表的组成元素以及它们之间的关系,可以很方便地利用dot文件得到对应的图形化表示。基本路径的转化算法如算法2所示。

算法2 基本路径转化。

输入 基本路径的节点集合P_n。

输出 基本路径信息对应的一阶逻辑公式集合F_n。

begin

1) nodeMsg=NodeToIR(Pn)

2) symbols=Symbol(nodeMsg)

3) statement=MatchSymbol(symbols)

4) fol=IRToFol(statement)

5) Fn.add(fol)

6) if (matchLoop(fol))

7) Fn.add(Lp)

8) Output(Fn)

end

基本路径转化算法分为两部分进行描述。

节点标记与语句分类:这一步主要是对路径节点进行标记和分类(算法第1)~3)行)。首先通过NodeToIR()方法获取节点内容nodeMsg,方法根据dot文件中的节点对应关系,获取节点名对应的节点内容;随后利用Symbol()方法对路径集中的语句所包含的关键词进行标记,这里利用巴克斯范式(Backus-Naur Form,BNF)^[16]的形式来进行标记操作。BNF范式是一种以形式化符号来描述给定语言的语法,BNF语法定义的对象是一个字符串集合,可以按照下面的规则来书写:

symbol :=alternative1 | alternative2…

根据上述规则,可以利用BNF范式来描述关键词,例如一个标识符,通常由字母或下划线开头,后续字符可以为数字、字母或下划线。因此,可以描述一个标识符为:

letter::="a" | "b" | … "z" | "A" | "B" | …"Z"

first::=letter | "_"

digit::="0" | "1" | … | "9"

rest::= first | digit

identifier ::= first rest*

标记完后开始对每条语句进行关键词匹配,通过MatchSymbol()方法,根据匹配到的关键词将语句划分为不同的类别。

语句转化:对匹配分类后的IR语句进行转化,得到路径对应的一阶逻辑公式集合(算法第4)~8)行)。利用IRToFol()方法,根据语句所属的类别和LLVM IR的语法规则,将语句从IR表示转化为对应的一阶逻辑公式,随后将一阶逻辑公式添加到公式集合中,当遇到循环语句时,则将对应的循环不变式添加到公式集合中,最后输出每条路径对应的一阶逻辑公式集合。

3.2 基本路径的验证

本文方法对基本路径的验证分为两步进行,首先通过对基本路径的一阶逻辑公式集合进行符号执行,得到路径的约束条件;随后利用SMT求解器对约束条件进行求解,得到路径的验证结果。

3.2.1 符号执行

符号执行^[17]是一种常见的静态分析技术,与执行程序时需要使用具体输入不一样,符号执行将程序的输入当作符号值,对程序的每条语句进行模拟执行,并进行约束收集。本文方法对基本路径集中的每条路径进行符号执行,通过定义路径输入为符号值,将路径中的表达式替换为符号表达式,同时收集程序中给出的判定条件(如assume语句和assert语句等)以及程序分支条件表达式对应的符号表达式,形成路径的约束集。

3.2.2 约束求解

约束求解^[18]是判断约束集是否满足的过程。约束满足问题可能有一个、多个或者没有解,如果一个约束满足问题至少有一个解,那么其就是可满足的或者是可行的；否则是不满足或不可行的。在本文方法中,约束满足问题就是判断基本路径约束是否有解的问题,利用SMT求解器作为约束求解器,将基本路径的约束集转化为SMT求解器标准输入格式即SMT-LIB语言格式,输入SMT求解器进行求解:若能找到解,则说明约束条件可满足；否则,说明约束条件不可满足。

4 实验与结果分析

本文利用LLVM+GraphViz工具实现了对程序的前期处理,同时利用Python语言实现了一个控制流图处理和路径提取工具,路径验证所需的符号执行工具为KLEE^[19],SMT求解器使用的是z3求解器,验证的属性包括缓冲区溢出、空指针引用、内存泄漏等。实验平台使用的CPU为AMD Phenom Ⅱ N830 2.1 GHz,内存大小为3 GB,操作系统为Ubuntu 14.04。

为保证对比实验结果的有效性,本文与同样基于SMT求解器的两个验证工具进行实验对比,一个是文献^[9]中实现的FSoft-SMT工具,另一个是采用边界模型检测技术的SMT-CBMC^[20]工具。本文直接从文献^[9]所选用的基准测试包中选择部分典型的测试用例来进行对比分析,测试程序中SelectionSort和BubbleSort分别实现了选择排序和冒泡排序,程序BellmanFord实现了带权图的最短路径算法,程序StrCmp、SumArray、MinMax分别实现了字符串的比较、数组的求和以及最大最小值的求取算法,这六个程序来自SMT-CBMC工具的基准测试包^[21]。程序InsertionSort和Fibonacci分别实现了插入排序和斐波那契数列算法,这两个程序选自SNU-RT基准包^[22]。

由表 1~2可知,本文方法能很好地解决路径验证过程中由于程序路径条数过多或复杂循环路径存在而导致的路径搜索空间过大问题。

从表 1可看出，本文方法在运行时间上比边界模型检测工具SMT-CBMC降低了25%以上,比FSoft-SMT工具降低了15%以上,这是因为SMT-CBMC对程序循环部分采用的处理方法是循环有限次展开,循环展开本身就是比较耗时的操作;而FSoft-SMT工具和本文实现的工具都是利用提取循环不变式的方法来进行循环结构的处理,这在一定程度上简化了验证过程。同时本文提取循环不变式采用的是决策树方法,相对于FSoft-SMT工具的抽象解释方法,决策树方法基于数据进行操作,自动化程度更高,提取速度更快;此外本文采用的基本路径法有效降低了测试路径的数量,减少了验证所需的时间。

从表 2可看出，本文实现的工具在运行精度上较SMT-CBMC和FSoft-SMT工具有较大提升,这是因为对循环结构进行有限次展开会丢失部分路径信息,同时抽象解释方法在不动点计算过程中会带来精度的损失,而决策树方法是二元分类方法,有效避免了因不动点计算带来的精度损失问题。

5 结语

针对路径验证过程中由于路径过多或存在复杂循环路径而造成路径搜索空间过大,影响验证的效率和准确率的问题,本文提出一种基于SMT求解器的程序路径验证方法。考虑到现有路径验证技术中存在的精度丢失问题,本文利用决策树方法对循环路径提取不变式,同时采用基本路径法对控制流图进行路径遍历,减少需要验证的路径数量。与同类型的两个工具相比,本文方法在验证的效率和准确率上有明显的提升。由于本文方法是基于LLVM IR这一中间语言进行分析的,因此本文方法可以对多种语言编写的程序进行路径验证。

本文方法也还存在一些不足之处,比如本文采用的决策树方法需要结合抽象域表示来进行,因此在不变式提取精度方面还有很大的改进空间,本文方法目前在对复杂程序的验证能力上还有所欠缺。后续研究将对本文提出的程序路径验证方法进行改善,重点针对循环不变式提取方法和策略的优化,以及提升对复杂程序的验证能力。