一种基于程序功能标签切片的制导符号执行分析方法∗

甘水滔 , 王林章 , 谢向辉 , 秦晓军 , 周 林 , 陈左宁

1(数学工程与先进计算国家重点实验室,江苏 无锡 214083)

2(计算机软件新技术国家重点实验室(南京大学),江苏 南京 210023)

大多数应用软件中存在多个功能选项.在Linux 系统下,目录“/bin”和“/usr/bin”下的绝大多数应用程序包含多个功能选项,表 1 中列举了从Linux 系统下随机挑选的应用程序,并且统计了各自的功能选项数量,如coreutils8.22 中的ls 程序包含54 个选项,who 程序中包含14 个选项,mkdir 程序中包含6 个选项,diffutils3.2 中diff 程序包含46 个选项等.可以发现,每个功能选项或几个功能选项组合,对应程序中一部分独立的执行路径.图1 给出了一个典型的示例程序.该程序从命令行可输入a,b,c,d,e,f等选项,每个选项的输入将执行其对应的功能函数,如a选项对应exe_a函数等,选项e和选项f必须在选项c使用之后有效.本文把程序的命令行选项开关称为功能标签.

Table 1 Parts of applications containing function label random relected in Linux system表1 Linux 系统下的随机挑选的部分包含功能标签的应用程序

Fig.1 Sample program图1 示例程序

针对这种带功能标签的应用软件,其测试手段主要依赖于静态分析和动态分析两大类方法.静态分析可以通过控制流、数据流分析等方法[1]获取功能标签、程序路径及程序缺陷的相关信息,但由于不能构造测试用例,无法验证其分析结果的真实性.动态分析方法主要分为基于输入数据变异的动态分析方法[2]和符号执行分析方法[3]:基于输入数据变异的动态分析方法在不知道功能标签信息的情况下,难以自动生成功能标签信息,因而在测试的过程中极其容易陷入只对部分或极少数的功能路径进行分析,具有很强的随机性;符号执行方法把程序的外部输入数据视为符号变量,运行并分析程序路径上的所有语句,对数据依赖于外部输入的变量进行符号化,不断收集条件分支语句的条件约束建立相应的约束系统,再利用约束求解器判定并求解执行路径对应的约束集,能够自动生成可行路径的测试例.通过精确地模拟程序的执行、跟踪变量的所有取值,理论上,符号执行可以做到对任意可执行路径的覆盖,实现对所有功能标签相关路径的测试例求解.因此,与其他测试方法相比,在功能覆盖及全局路径的覆盖效果上,符号执行方法更能适应于该类带功能标签的应用软件.但程序路径爆炸和求解开销过大,一直是限制符号执行分析效率的主要难题,尤其是在不知道程序执行路径片段和各个功能标签关系的前提下,利用符号执行进行程序分析会面临以下3 个问题.

•问题1:对于给定的可能存在缺陷的执行路径片段,难以确定较优的路径搜索策略进行动态目标制导.

如图1 和后文图3,假设需要制导的路径位置处于功能标签c和e的相关路径中,当选择采用深度优先搜索策略(DFS)时,必须遍历所有和功能标签a和b相关的路径;当采用广度优先搜索策略(BFS)进行路径制导时,如果目标点较深,也将遍历与功能标签c和e之外的功能标签相关路径;当选择采用随机搜索策略时,将会以极小的概率制导该路径片段.

•问题2:难以对某功能标签的所有相关路径进行正确性验证.

如图1 和后文图3,假设只需要验证功能标签e相关的执行路径,和问题1 类似,在不知道功能标签信息前提下,不论采用何种路径搜索策略,无法只选择某功能标签相关路径.如果采取种子模式,即构造一个带选项e的测试例进行混合执行,由于不知道功能标签之间的关系,难以构造测试例成功到达功能标签e相关的执行路径中.

•问题3:容易卡在某个包含多层循环的功能标签代码片段上.

如果某块功能代码中包含多层循环结构,一旦符号执行分析进入该代码中,容易导致过度的时间消耗,难以执行到其他的功能代码上,这样不利于对程序的全局覆盖测试.

针对以上3 个问题,本文提出一种基于程序功能标签切片的制导符号执行分析方法(OPT-SSE),根据程序的功能文档建立相应的功能标签集合,利用静态分析方法对程序进行不同功能划分,在程序依赖图上生成不同功能标签的切片,把执行路径有序的映射到不同功能上,对于给定需要制导的目标点,提取与目标点相关的切片,通过对切片相关节点进行标记,为符号执行的路径选择提供制导信息.利用预定义的功能标签流制导规则裁剪无关路径,不仅可以加速目标点制导过程以及提升特定功能模块的覆盖率,通过功能切片的制导信息分离,还提升了对整个程序的覆盖率.

本文第1 节描述OPT-SSE 的基本实现框架和流程,简要分析该模型如何对图1 给出的示例程序进行制导加速及全局覆盖率提升,并给出模型后面算法和规则描述的基本定义.第2 节描述功能标签流排序算法.第3 节描述基于符号执行的功能标签流制导规则.第4 节描述测试与分析.第5 节对符号执行相关工作进行总结.第6节对本文主要工作进行总结.

1 基于程序功能标签切片的制导符号执行分析模型

1.1 模型概述

图2 给出了功能切片符号执行模型OPT-SSE(OPT-sliced symbolic execution)的主要执行流程,具体如下.

(1)获取功能标签.分析软件的功能文档,获取功能标签集合,如命令行功能选项集合.

(2)静态控制流分析与制导规则生成.首先,生成软件代码的中间代码,生成每个基本块的相关信息,再利用控制流分析生成控制流图CFG;其次,遍历该程序控制流图,确定每个和功能标签相关的基本块,生成功能标签控制流图OPT-CFG;最后,在功能标签控制流图基础上,遍历生成功能标签路径OPT-Path,并利用排序规则进行排序.

(3)制导符号执行.

➢将特定功能或特定代码目标点映射到对应的一条或多条功能标签路径.

➢在符号执行分析过程中,引入针对功能标签路径的制导规则.制导规则包括两种:一种为不带功能标签路径排序信息的制导规则,另一种是带功能标签路径排序信息的制导规则.

➢针对特定功能对应的功能标签路径,生成相应的测试例集合,并进行缺陷分析.

➢针对特定代码目标点进行制导分析,需要生成相应的可达测试例集合.

Fig.2 Guided symbolic execution model based on program function label slice (OPT-SSE)图2 基于程序功能标签切片的制导符号执行模型(OPT-SSE)

以图1 的程序为示例,图3 和图4 展示了OPT-SSE 模型的优化思想.

Fig.3 OPT-SSESpeeding up goal-guided process图3 OPT-SSE加速目标点制导

Fig.4 OPT-SSEImproving whole coverage图4 OPT-SSE提升全局覆盖率

图3 描述了OPT-SSE 模型加速目标点制导过程:通过静态分析目标点和各个功能标签的隶属关系,为符号执行过程提供特定功能代码分析的制导信息,在符号执行框架下,定义针对不同指令的制导语义规则,尽早地裁剪无关的路径分支,以加速动态符号执行的目标制导过程.其中,实线箭头指向的路径是需要制导的目标路径,斜杠表示的是分支裁剪操作.图4 描述了OPT-SSE 模型提升全局覆盖率过程:通过对不同的功能代码进行有效分割,可对整个程序进行并行化符号执行;同时,采用多个客户端对不同的功能代码块进行分析,可避免卡在对某个功能代码块的分析上,以提升全局覆盖率.即同时采用多个符号,执行客户端对不同的实线箭头指向的路径进行制导分析.

1.2 模型基本定义

定义1(程序功能标签).一个测试程序的功能文档中可获取有限个功能标签,构成一张功能标签符号表OPT={option0,option1,…,optionnum},num为功能标签的个数,optioni表示为程序的第i个功能标签(0＜i＜num).

定义2(功能类型分支判定条件).对于功能标签符号表OPT={option0,option1,…,optionnum}的程序,其功能类型分支判定条件集用OPTcondition描述.用树结构描述程序中任一分支判定条件condition对应的表达式,操作符operators为中间节点,操作数operands为叶子节点,判定分支判定条件condition是否为功能类型分支判定条件,根据以下等价关系:

定义3(程序控制流图).程序控制流图CFG用四元组〈N,E,entry,exit〉表示,其中,N表示该过程的节点集合,E是边的集合,entry表示入口节点,exit表示退出节点.任一节点表示为一组连续顺序执行语句的基本块,其中,N和entry节点包含的最后一条语句为分支语句.每条边是一个表示从节点ni到节点nj可能存在控制流转移的有序节点对〈ni,nj〉,并满足:ni是nj的直接前驱,nj是ni的直接后继.每个节点可以有多个直接前驱节点,但至多有两个直接后继节点.entry是一个没有前驱的节点,exit出是一个没有后继的节点.

定义4(程序执行路径).对于一个程序控制流图CFG,任意存在控制流转移的有序节点对〈ni,ni+1〉,从节点ni执行到节点ni+1必须满足分支条件conditioni,定义为,那么对于程序执行路径集合Path,其任一条路径用有限个有序节点〈n1,…,nj〉表示,定义为,并满足:

定义5(程序执行路径片段).对于一个程序控制流图CFG,其生成的路径片段集合为PathSeg,一条执行路径片段用有限个有序节点〈n1,…,nj〉表示,定义为

定义6(功能标签控制流图).一个功能标签控制流图OPT-CFG可由程序控制流图CFG遍历生成,用四元组〈N′,E′,entry,exit〉表示,其中:N′表示该过程的节点集合,每个过程节点表示某个功能标签激活后直接到达的基本块;E′是边的集合;entry表示入口节点;exit表示退出节点.每条边用有序节点对描述,表示从节点到节点之间存在并且只存在一条功能标签控制流.节点到节点之间存在一条功能标签控制流边的充要条件为:程序存在一条从的语句到达的语句的执行路径

定义7(功能标签执行流).对于一个功能标签控制流图OPT-CFG,功能标签执行路径集合用OPT-Path表示,对于任意控制流,从节点执行到节点必须满足约束集合constrainti定义为,其任一条路径用有限个有序节点表示,并满足:

性质1(功能标签执行流约束集).对于节点执行到节点的约束集合constrainti,一定满足:

性质2(用OPT-Path 对Path 进行分类).存在一个函数Ψ,实现Path到OPT-Path的映射关系:

证明:由定义可知:对于给定的程序,其程序控制流图CFG生成执行路径集合Path;功能标签控制流图OPTCFG生成功能标签执行路径集合OPT-Path.对于任意一条可执行路径X=〈n1,…,nj〉∈Path,通过删除其中的与功能类型分支判定条件语句无关的过程节点,得到节点有序序列,一定满足:,由根据定义6 可知,.因此,任意一条可执行路径X可通过函数Ψ映射到唯一的一条功能标签执行流Y.□

定义8(偏序关系算子).偏序算子⊙={≺,≻}用来描述分支节点的后续节点的大小关系或者同一程序下任一两条执行路径的大小关系,对于节点n(分支条件为condition)的true 后续节点nt和false 后续节点nf,则定义为或者〈n,nt〉≻〈n,nf〉.

定义9(程序控制流执行路径的偏序关系).程序控制流中两条不同执行路径〈n11,…,n1i〉和〈n21,…,n2j〉,偏序关系的判定定义如下:

定义9 表明,对于一个程序中任意两条不同路径,一定存在某个分叉节点,使得一条路径执行true 分支,另一条路径执行false 分支.那么执行true 分支的路径大于执行false 分支的路径,这样可对一个程序中所有不同的可执行路径进行大小关系排序.

定义10(功能标签执行流的偏序关系).如果程序中任意映射到两条功能标签执行流〈〈n11,…,n1i〉〉,〈〈n21,…,n2j〉〉的执行路径存在相同的偏序关系,那么这两条功能标签执行流也存在类似的偏序关系,即满足:

性质3.同一程序下,任意不同功能标签执行流存在偏序关系:

证明:设存在〈n1,…,nk〉,〈nx1,…,nxp〉,,满足:当时,根据假设,一定存在n2y(1＜y≤j)或者n1d(1＜d≤i),n2y和n1d其中至少有一个节点具有两个相同的功能标签控制流前驱节点,这样与定义6 相矛盾,假设不成立.所以,任意不同功能标签执行流之间存在偏序关系.□

定义11(带制导信息的符号执行状态).符号执行环境下生成的程序状态集合为S,任一状态S∈S用五元组〈s,ρ,σ,g,f〉表示,其中,s表示状态S下一步执行的语句序列,ρ表示状态S的约束条件集合,σ表示状态S的符号变量到符号值的映射关系,g表示状态S下一步需要制导的基本块信息,f表示状态S需要制导的功能标签流.

2 功能标签流排序算法

功能标签路径生成和排序算法OptPathGenerationAndSorting第1 行～第8 行通过对每个过程内控制流图进行线性扫描,获取包含功能标签分支语句的基本块,再通过控制流分析确定满足功能标签分支条件的后继基本块,加入到功能标签节点集合OptNode中;第9 行通过调用OptCfgGeneration函数生成过程控制流图对应的功能标签控制流图OptCfg;第10 行、第11 行对第1 条功能标签路径的节点数量初始化;第12 行通过调用OptPathSorting生成排序好的功能标签路径集合.

功能标签路径生成和排序算法.OptPathGenerationAndSorting.

功能标签控制流图生成算法OptCfgGeneration利用两遍遍历从程序控制流图生成功能标签控制流图,算法第1 行～第13 行第1 遍深度遍历生成功能标签控制流图的中间图,该图会出现某个功能标签节点可能出现多个相同的前驱节点;算法第14 行～第23 行通过对每个功能标签节点进行检查,对于出现多个相同的前驱节点的功能标签节点,复制一个别名功能标签节点,并建立和功能标签节点的映射关系,这样就能确立功能标签路径的唯一性.图5 给出了一个样例.

功能标签控制流图生成算法.OptCfgGeneration.

Fig.5 Uniqueness generation for function label path图5 功能标签路径唯一性确立

功能标签流排序算法OptPathSorting对功能标签控制流图深度遍历生成功能标签路径集合,根据路径生成的先后次序正好确定了功能标签路径的偏序关系.

功能标签流排序.OptPathSorting.

3 基于符号执行的功能标签流制导规则

以下定义了两种功能标签流制导规则:无排序信息的功能标签流制导规则和带序信息的功能标签流制导规则.每种制导规则都实现了3 种指令处理语义规则:调用指令处理语义规则、分支指令处理语义规则、其他指令处理语义规则.由于分支指令处理语义涉及的情况多,表2 定义了规则中使用的部分基本符号,作为任意语义描述的前提条件,使用真值表(表3 和表4)对前置条件的取值进行描述,并对应不同的语义情况,表5 为表3、表4 中前置条件对应的输出集合.

Table 2 Basic symbol definition of rule (as precondition for any semantic description)表2 规则基本符号定义(作为任意语义描述的前提条件)

Table 3 Precondition truth Table 2 on branch instruction processing semantics of function label flow guided rule without ordering information表3 无排序信息的功能标签流制导规则中分支指令处理相关语义前置条件真值表2

Table 4 Precondition truth Table 3 on branch instruction processing semantics of function label flow guided rule without ordering information表4 无排序信息的功能标签流制导规则中分支指令处理相关语义前置条件真值表3

Table 5 Precondition and related output assemble表5 前置条件和对应的输出集合

Fig.6 Finite state machine model for guided symbolic state information conversion图6 符号状态制导信息转换的有限状态机模型

无排序信息的功能标签流制导规则：

调用指令处理语义规则：

调用指令处理语义1 描述的是当调用一个函数时的制导符号状态的变化情况,调用指令处理语义2 描述的是当从一个函数返回时的制导符号状态的变化情况.

分支指令处理语义规则：

图7 对应了分支指令处理语义规则的各种语义:语义1 和语义2 表示只有一个条件分支可满足,并且直接跳转到目标功能标签流对应的相关节点;语义3 和语义4 表示只有一个条件分支可满足,并且直接跳转到非功能标签节点;语义5 和语义6 表示只有一个条件分支可满足,并且直接跳转到与目标功能标签流不相关的功能标签节点;语义7～语义19 表示两个条件分支均可满足,分别跳转到与目标功能标签流不相关的功能标签节点、与目标功能标签流相关的功能标签节点、非功能标签节点的各种组合情况;语义20 表示当制导符号状态下一步需要制导的基本块信息g=ε时,直接删除该制导符号状态.

Fig.7 Branch instruction processing semantics of function label flow guided rule without ordering information图7 无排序信息的功能标签流制导规则中分支指令处理相关语义

其他指令处理语义规则:

调用指令处理语义规则和其他指令处理语义规则与无排序信息的功能标签流制导规则中各条语义的前置条件、输入、输出完全一样;分支指令处理语义规则与无排序信息的功能标签流制导规则下第1 条～第7 条和第10 条～第20 条共18 条语义的前置条件、输入、输出完全一样;第8 条和第9 条语义更改为以下4 条语义操作:前两条语义实现图8 中的裁剪策略1,后两条语义实现了图8 中的裁剪策略2.裁剪策略1 表示当制导的两个分支中,其中一个基本块属于制导的特定功能标签之外的功能标签时,另一个基本块属于非特定功能标签,并满足属于制导的特定功能标签之外的功能标签的基本块在外侧.由于内侧的基本块或后续基本块仍然可能属于特定功能标签,所以只能裁剪掉包含属于制导的特定功能标签之外的功能标签的分支.裁剪策略2 表示当制导的两个分支中的一个基本块属于制导的特定功能标签之外的功能标签时,另一个基本块属于制导的特定功能标签,并且属于制导的特定功能标签之外的功能标签基本块处于内侧.如果根据排序信息知道特定功能标签流处于这两侧功能标签流之间,那么可以裁剪掉这两个分支.

Fig.8 Differece between branch instruction processing semantics of function label flow guided rule without ordering information and that with ordering information图8 有排序信息的功能标签流制导规则中分支指令处理语义规则与无排序信息的功能标签流制导规则中分支指令处理语义规则区别

有排序信息的功能标签流制导规则:

根据上述对各种指令的制导语义规则的描述,相对于KLEE 而言,OPT-SSE 在整个符号执行过程中只会增加分支指令解释执行时的时间开销,这个时间开销主要是判定跳转到的下一个基本块是否包含特定功能标签的分支语句带来的,OPT-SSE 在静态分析环节可以标记任意基本块是否包含功能标签类分支,因此在制导过程中可直接判定某节点是否为功能标签相关节点,不会有额外的时间开销,但需要判定某功能标签节点是否为特定功能标签相关节点的时间开销上限为|f|倍(即功能标签流f包含功能标签的个数).对于整个程序而言,功能标签相关节点数量只占所有节点数量的极小比例,因此对比KLEE,OPT-SSE 制导时间增加的时间开销可以忽略.

4 测试与分析

OPT-SSE 实验平台在以下环境实现:处理器:Intel(R)Xeon(R)CPU E7-4830 2.13GHz;内存:64GB;操作系统:Ubuntu 12.04.

OPT-SSE 包括静态分析和动态分析两个模块:原型系统在llvm 上实现静态分析环节,包括生成控制流图、标记关键指令、生成程序功能标签流等工作,为动态分析提供辅助信息;整个动态分析环节在klee 上实现,包括对上述各条制导规则的实现.

本文从开源库中选择了wla_dx、Vim、Unrtf、Binutils、Sed、Wdiff、which、Findutils、Gzip、Coreutils这10 个不同的开源软件作为测试对象,并挑选这些软件中的20 个不同目标进行测试,基本信息见表6.

表6 描述了各个软件对象的版本和功能、测试目标以及对应llvm IR 静态指令数量等信息.实验主要针对OPT-SSE 的指令覆盖率、分支覆盖率、代码目标制导效率等方面的性能进行测试,并且将其与klee 进行横向比较,体现本文工作的优化能力.

表7 给出了wla-gb 等20 个软件目标的详细实验数据,实验设置每次对目标的测试时间上限为10h.在OPT-SSE 上设置程序功能标签流的最大数量为8;在klee 上对每个目标分别进行宽度、深度、随机这3 种路径搜索策略的测试,选取其中覆盖率最优的一组数据.

Table 6 Basic information of subjects表6 测试软件对象基本信息

Table 7 Experimental data for each subject表7 对各个软件目标测试的实验数据

表7 分别统计了各个目标在KLEE 和OPT-SSE 上的MinTestCaseNum、MinExeInstrNum、MaxInstrCoverage、MaxBrCoverage等指标数据,其中,

•MaxInstrCoverage表示测试10h 中取得的最大指令覆盖率.

•MaxBrCoverage表示测试10h 中取得的最大分支覆盖率.

•MinTestCaseNum表示测试的10h 中,达到最大指令覆盖率和最大分支覆盖率的最小测试例生成数量.

•MinExeInstrNum表示测试10h 中,达到最大指令覆盖率和最大分支覆盖率的最小执行指令数量.

图9 描述了各个测试目标KLEE 和OPT-SSE 的MaxInstrCoverage指标对比情况,图10 描述了各个测试目标KLEE 和OPT-SSE 的MaxBrCoverage指标对比情况.

Fig.9 Instruction coverage comparison between OPT-SSE and KLEE on different subjects图9 OPT-SSE 和KLEE 对不同目标的指令覆盖率比较

Fig.10 Comparison of branch coverage between OPT-SSE and KLEE on different subjects图10 OPT-SSE 和KLEE 对不同目标的分支覆盖率比较

可以发现,与KLEE 相比,OPT-SSE 在指令覆盖率和分支覆盖率上得到了一定程度的优化,其中,expr、unrtf、locate、vim 等目标在指令覆盖率和分支覆盖率提升最为显著,大约为KLEE 的1.5 倍～3.5 倍.另外可以发现,在wdiff、which、dircolors 等多个目标上,出现了OPT-SSE 的MinExeInstrNum指标比KLEE 要小的情况.其原因可能是,OPT-SSE 在不同程序功能标签流上更早遇见较深的循环结构,使得MaxInstrCoverage和MaxBrCoverage两个指标一直得不到改善.但在整体覆盖率上,仍然比KLEE 有所提升.

图11 和图12 分别给出了wla-gb 在测试过程中指令覆盖率和分支覆盖率的实时变化情况.可以发现,指令覆盖率和分支覆盖率从测试开始到最后,OPT-SSE 比KLEE 的优化效果明显.

Fig.11 Comparison of instruction coverage and time overhead between OPT-SSE and KLEE when analyzing wla-gb图11 OPT-SSE 和KLEE 分析wla-gb 时的指令覆盖率和执行时间对比

Fig.12 Comparison of branch coverage and time overhead between OPT-SSE and KLEE when analyzing wla-gb图12 OPT-SSE 和KLEE 分析wla-gb 时的分支覆盖率和执行时间对比

表8 给出了OPT-SSE 和KLEE 在代码目标制导能力方面的对比情况.

Table 8 Comparison between OPT-SSE and KLEE on code goal-guided capability表8 OPT-SSE 和KLEE 在代码目标制导能力上的对比

图13 描述了OPT-SSE 与KLEE 相比,在代码目标制导速度和成功率上的提升情况.针对各个测试目标,本文利用静态分析[4-6]获取初步脆弱性可疑点集合,然后从集合中筛选20 个脆弱点作为代码目标集,分别利用OPT-SSE 和KLEE 进行1h 的制导分析.设置1h 的时间上限,是考虑多个目标在1h 后指令覆盖率变化很小.表中统计了各个目标分别在KLEE 和OPT-SSE 上的代码目标制导时间开销、代码目标制导加速比、制导成功数量以及成功率提升等指标的详细数据,其中,代码目标制导时间开销为KLEE 和OPT-SSE 都能成功制导的代码目标时间开销平均值.选择KLEE 和OPT-SSE 都能成功制导的代码目标,是为了更好地比较代码目标制导加速情况.本文设定:代码目标制导加速比=KLEE 的代码目标制导时间开销/OPT-SSE 的代码目标制导时间开销,成功率提升比例=(OPT-SSE 的制导成功数量-KLEE 的制导成功数量)/20.通过数据观察可以发现,在代码目标制导加速比方面,OPT-SSE 在每个目标上都有所提升;在成功率提升比例方面,除which 外,其他目标都有显著的提升.

Fig.13 Improvement of OPT-SSE on code goal-guided speed and success rate compared with KLEE图13 OPT-SSE 与KLEE 相比在代码目标制导速度和成功率上的提升情况

5 相关工作

近年来,符号执行在程序的正确性验证、缺陷的发现和重现、复用代码的检测、自动调试能力增强等方向产生了良好的应用,但由于存在程序路径爆炸增长和约束求解时间开销过大问题,制约其通用能力的发展.学术界和工业界一直把如何拓展符号执行的应用面和提升符号执行效率作为软件程序分析领域的基础性课题[7].符号执行在程序分析上的应用能力主要体现在以下几点.

(1)不同程序语言上的应用

陆续产生了具备分析c/c++、JAVA、JAVAscript、python 等语言能力的符号执行原型系统.如,斯坦福大学Cadar 等人先后开发了EXE[8]和KLEE[9],这两个系统都应用于c/c++程序对象.KLEE 重写了EXE 的符号执行分析引擎,通过分析c/c++程序目标的llvm 字节码,提升了路径覆盖率和缺陷发现能力.NASA 的Robust 软件工程开发小组开发了JAVA pathfinder[10,11],通过分析JAVA 程序的字节码,具备应用于并发性JAVA 程序分析的能力.伯克利大学的Saxena 等人设计了一种适用于字符串求解的约束语言Kaluza[12],适用于求解各种事件空间以及数值空间,在此基础上,构建一个适用于JAVAscript 语言的符号执行框架,具备检测命令注入缺陷的能力.洛桑联邦理工大学的Bucur 等人开发了Chef[13],通过对python 解释器的相关包裹函数进行符号插桩处理,对python 语言对象和解释器进行不同层次的符号执行,构建了适应于python 语言的符号执行引擎.

(2)不同系统平台上的应用

主要是针对Linux 平台及windows 平台,直接对二进制程序进行分析,通过把二进制翻译成符号执行引擎可识别的中间语言,可以消除不同程序语言的影响,并且适应于闭源程序对象.如,微软研究院的Godefroid 等人开发了DART[14]和SAGE[15],专门用于windows 平台的应用程序分析,展现了显著的效果.洛桑联邦理工大学的Vitaly 等人开发了S2E[16,17].该系统利用qemu translator[18]将Linux 二进制程序翻译成llvm 字节码,再结合KLEE实现对Linux 二进制程序的分析.卡耐基梅隆大学的Sang 等人开发了Mayhem[19],通过使用Bap 平台[20],将Linux二进制转换成BIL 语言,再结合符号执行引擎后端进行分析,在debian 系统上发现大量的缺陷.

(3)不同功能程序对象上的应用

包括对应用级程序、内核级程序、设备驱动级程序、固件级程序等不同功能程序的符号执行分析.如,经典符号执行引擎[4,5,10,14,21-23]只适应于应用级程序分析,S2E 通过对操作系统插桩处理并添加特权指令的支持,具备分析内核级程序的能力.洛桑联邦理工大学的Kuznetsov 等人在S2E 基础上构建了DDT[24],通过对设备驱动程序相关接口进行有效配置,成功应用于设备驱动程序的分析.后来,康斯威星大学的Matthew 等人开发了symdrive[25].该系统对分析的设备中各种I/O 操作、DMA 操作、中断操作进行符号化,并结合静态分析裁剪设备驱动程序的无关路径,提升了设备驱动级程序分析的有效路径覆盖能力.康斯威星大学Davidson 等人开发的FIE[26]以及EURECOM 大学Zaddach 等人开发的Avatar[27],这些系统通过对符号执行引擎支持的运行环境对固件代码建模,成功地用于嵌入式系统上的固件代码的缺陷分析.

从符号执行技术应用发展趋势[28]可看出,符号执行应用的程序语言对象多元化,从支持高级语言到二进制语言,再到解释型语言,中间语言翻译平台[20,29-34]的不断发展,逐渐加强了符号执行在程序语言上的通用性.但是符号执行对于各种程序语言的分析效率仍然具有较大的提升空间,尤其是复杂、大规模程序对象的应用效果一直受制于路径空间爆炸和约束求解开销过大,在一定程度上,通过以下方法得以优化或缓解.

(1)路径搜索策略的提升

符号执行需要采用特定的路径搜索策略进行状态遍历,一般经典符号执行引擎集成多个路径搜索策略.如,KLEE[9]中实现了深度优先、宽度优先、随机选择、多策略交替选择等路径搜索策略.深度优先选择策略容易搜索到完整的执行路径,但对程序的整体覆盖率较低;宽度优先选择策略会产生很多路径片断,很难分析到较深的路径;随机选择选择策略可以避免类似动态分析过程中由于碰见复杂外部库无法跳出来的情况;多策略交替选择策略通过采用交替地采用深度优先、宽度优先、随机选择策略分析一段固定的时间,结合了各自的优势.PEX 定义了一种适应度函数,用来评估待选择的分支离未覆盖过分支的距离,通过这个度量值选择最佳分支,取得的较高的覆盖率[35].SAGE 中采用一种约束产生式的状态遍历方法(generational-based),先否定所有的路径条件,然后逐渐将最深的路径条件反转回来,可以优先遍历到不同的深度路径[21].Li 等人[36]提出了优先选择路径分支执行重复频率最低的分支,可以在某些代码场景产生更高的覆盖率.

(2)约束求解优化

KLEE 在求解模块采用路径预判断、约束表达式简化、约束集简化、反例缓存机制等技术降低求解开销.Romano 等人[37]建立了表达式匹配规则系统,尽量利用历史约束集信息确定新约束集是否可解,在一定程度上降低了对求解器的查询次数.S2PF[38]提出,避免一遇见条件分支就调用约束求解器,而是通过累积多个条件分支后再进行求解:如果约束集可解,则说明该执行路径上之前的约束集都可解,避免了之前的求解开销;如果约束集不可解,则回溯到之前没有求解的条件分支再次执行,从一定概率上节省了总的约束求解开销.秦晓军等人[39]提出了一种基于懒符号执行的约束求解算法,自动识别循环结构.通过推迟变量实例化等方法,有效地缓解了循环结构的路径组合爆炸问题,降低了求解次数.

(3)冗余状态归约

Li 等人针对符号状态定义弱等价关系[40],如果一组状态满足该关系,那么可以用一个状态替代该组状态.例如,某循环体中的判定条件与符号变量有关,并且某个变量依赖于外部库的符号返回值,那么对于每次循环,都会产生一个新的符号变量,这样会出现大量呈弱等价关系的状态.这种方法在一定程度上加速了符号执行过程.Bugrara 等人[41]提出,如果一组约束覆盖的代码行和另一组约束相同,则认为这组约束对应的状态是多余的,可以消除,并利用动态切片方法[42]确定不同约束集是否覆盖相同代码行.该方法提升了代码覆盖率.

(4)状态合并方法

如果两条路径在某个代码点交汇,那么可以把两个状态的约束集合并成一个状态的约束集.这样可以大量削减状态的总数量,但有可能出现对合并后约束集的求解开销大于合并之前分别求解的总开销,尤其容易发生在大规模程序中[43].针对这一情况,出现了相应的折中方法,如,

•Boonstoppel 等人[44]提出,如果两个状态效果相同,并且约束集中取值不同的变量与的后续路径选择无关,那么这两个状态合并后约束集在后续求解中带来的额外开销会降低,可以选择合并符合该条件的状态集合.

•Kuznetsov 等人[45]提出,针对每次状态合并之前,评估合并后约束集中新增符号变量所增加的求解器查询次数,以此确定潜在的合并点.

(5)执行分段和合成方法

Le 利用静态分析根据循环体、外部库等代码特征将程序片段化,再通过动态执行获取各个片段的相关接口信息以及自动合成各个片段,可以更好地处理程序循环结构和动态库带来的符号化问题[46].Ramos 等人[47,48]提出,分别对各个用户定义函数体进行符号执行,再对触发函数体缺陷的输入进行合成,避免直接从主函数分析时出现的深度路径不可达情况,可产生更高的语句覆盖率.Sinha 等人[49]提出,通过对并发性程序进行分阶段执行,有效分离线程的过程内和过程间操作.第1 阶段获取线程全局变量信息,对线程序列进行有效分割;第2 阶段利用执行序列的一致性把路径片段组合成完整线程,具备并发性缺陷发现能力.Zamfir 等人[50]提出,对并发性程序的序列路径合成和线程调度合成,可准确地重现并发性缺陷.

(6)Concolic 执行方法

该方法需要使用种子数据,即初始测试例,在对种子数据进行具体执行的过程中,收集执行路径的其他分支相关符号约束,构造后续状态集合,并在具体执行完种子数据后,采用特定状态选择策略进行符号执行.Concolic执行方法可以借助具体执行特定的测试例快速制导具有一定深度的代码,可解决纯符号执行不适应复杂目标的深度路径可达问题,在多个符号执行引擎[8,9,14,15]中得到了体现.如,KLEE 中利用种子数据进行符号执行,一旦执行完种子数据,就利用特定搜索策略对种子数据的分支状态进行遍历;CUTE 采用不断随机生成测试例进行具体执行,一旦生成的测试例不能覆盖新的分支,将切换到符号执行[51],这种Concolic 执行方法提升了4 倍以上的覆盖能力;DASE[52]构造特定输入种子,并确定其中固定字段,在种子模式执行分析过程中,可避免对这些固定数据的约束求解,提高了分析效率.

(7)并行化方法

Cloud9[53]在KLEE 的基础上、MergePoint[54]在Mayhem 的基础上分别构建了并行符号执行框架.他们采用在集群的某个节点上启动符号执行,动态地选择当前节点上产生的不同状态,并分离到集群上的其个节点上继续执行,实时保持不同节点上的负载均衡,取得了良好的效果.Junaid 等人[55]提出利用不同测试例划分程序路径范围,对不同程序路径范围进行并行性测试,大幅度提升覆盖率.

大部分符号执行性能优化方法只适应于特定的程序场景,需要结合多种优势才能应对程序对象多样性、复杂性的通用测试需求.针对一个路径数量过多的程序,不管采用何种路径选择策略,如果要做到全局覆盖,很难达到理想的效果,需要其他优化能力的不断提升.基于符号执行面临的现状,近几年出现了一种实用性较强的应用——制导符号执行分析方法.该方法不以程序的全局覆盖为目标,只对程序中感兴趣的程序片段或性质进行验证,适用于补丁程序的可靠性分析、特定场景的测试例生成、特定缺陷发现等应用方向.制导符号执行一般通过静态分析或附加的限制条件信息增强其分析的导向性,利用预定义好的制导规则指导符号执行如何进行更好的路径搜索达到制导目的,其效果更易于提升不同代码规模程序对象的应用.制导符号执行分析方法出现了一系列应用,如,Kin 等人[56]提出一种快速的程序行可达性判定和测试例生成算法,在静态控制流图上计算每个程序分支和目标代码行的距离值,每执行分支时,选择离目标代码最近的程序分支,能够快速到达目标代码行;Paul 等人[57]通过优先选择程序分支到敏感指令(读和写)的距离最近的分支进行制导分析,发现很多读写相关的缺陷;Zhang 等人[58]提出通过有限状态机模型对正规性质进行定义,利用符号执行对程序正规性质进行制导分析,有效地验证程序中内存泄漏等路径敏感缺陷;DiSE[59]先通过静态分析检查某软件系统不同版本间的差异,并利用制导符号执行产生差异代码可达路径条件,可以检查程序更改后带来的影响;Taneja 等人[60]通过构建程序控制流图,确定与修改代码区域无关的条件分支,在符号执行过程中裁剪这些无关分支,能够更快地产生回归测试例,已验证程序修补后的正确性;Marinescu 等人[61,62]利用制导符号执行实现对已知补丁集合的进行覆盖测试,通过计算每条指令到补丁代码的条件数量作为度量距离值,采用最弱前置条件分析[63]确定目标不可达的基本块,最后对多个初始种子中选择出离补丁代码最近的种子数据,可以为后续符号执行制导补丁代码提供距离最近的状态;Domagoj 等人[64]先运用静态分析确定二进制程序中的脆弱点,再借助事先在控制流边上标记到达脆弱点的静态跳转次数信息对这些脆弱点集合进行制导符号执行分析;Ge 等人[65]利用制导符号执行分析方法对静态分析得到的缺陷报告进行动态验证,提高了静态分析的准确性;Guo 等人[66]通过静态分析确定程序正确的部分,在符号执行过程中对这些不包含缺陷的路径分支进行实时的裁剪,提升了分析速度.

6 结 论

本文提出了一种基于程序功能切片的符号执行制导分析方法OPT-SSE.该方法参考程序的功能文档,在控制流图上把提取控制功能执行路径的关键基本块,并标识成相应的功能标签.OPT-SSE 利用功能标签流对程序进行有序划分,对于给定的代码目标点,提取与之相关的功能标签切片,然后根据预定义的制导规则对该切片进行制导分析.实验结果表明,该方法能够显著加速代码目标制导速度和成功率;并且通过并行的方式制导分析不同的程序功能切片,能够避免符号执行卡在某个循环结构体上,从而提升对整个程序的分支和指令覆盖率.

OPT-SSE 在下一步工作中需要对以下不足进行优化.

(1)采取静态切片提取功能标签受影响的基本块.可能会分析出部分可能执行不到的代码片段,从而影响后续的符号执行制导效果,在下一步工作中需要借助动态切片进一步优化.

(2)本文把程序的选项定义为功能标签,在今后的工作中,可以对功能标签进行更宽泛的应用,例如,把程序中所有不可变性质归纳为相应的功能标签,如固定输入格式和结构.利用更多的功能标签信息,可以进一步提升符号执行制导效率.