张健等:程序分析研究进展 用中 Reps等人的后续进一步扩展了该框架,通过已有抽象域为环境而计算得到新的属性用于过程间常数传播 等应用中,并形式化定义了上述图可达问题为上下文无关文法图可达问题上下文无关文法图可达问题对图中 的边进行标号,图中任意两点可达需要两点间的一条路径上的标号串满足事先定义的上下文无关文法多种不 同程序分析问题均可表示为对上下文无关文法图可达问题的求解近年来,包括指针分析68,69、并行程序分 析m,m等多种分析技术均通过求解上下文无关文法图可达问题来有效地加以实现 2)基于值流图的稀疏数据流分析方法 传统的数据流分析在程序控制流图上将所需计算的状态信息在每个程序点传播得到最终分析结果此过 程通常存在较多冗余操作,对效率,特别是过程间数据流分析效率会有很大影响为了进一步提高数据流分析的 效率,近年来,研究者们提出了多种稀疏的分析方法从而无需计算状态信息在每个程序点的传播即可得到与数 据流分析相同的结果该类分析技术D通过一个稀疏的值流图 alue flow graph)直接表示程序变量的依赖关 系,从而使得状态信息可以有效地在该稀疏的值流图上传播该值流图保证了状态信息可以有效地传播到其 要使用该信息的程序点并避免了在无效程序点的冗余传播,可大幅度提高效率 2.3基于摘要的过程间分析 摘要 summary)是可复用的程序模块分析结果,能够简要地刻画模块的外部行为创建摘要和利用摘要开展 分析的过程称为摘要分析在编写程序的过程中,一个程序模块往往需要调用其他程序模块对主调( caller)模块 的分析必然涉及到对被调模块(cale的分析与复用被调模块代码可提高软件生产效率类似,摘要分析期望复 用被调模块的分析结果也能提高分析主调模块的效率通过基于摘要的程序分析技术我们将被复用模块的分 析结果被构造成为摘要,并在分析主调模块时对其实例化以加快分析速度 传统摘要分析的研究主要关注模块化( modular)分析,即:在分析过程中将软件划分为多个模块,对各个模块 分别分析和创建摘要,然后合并摘要获得整体的分析结果这样在分析过程中创建摘要的技术也称为在线摘要 技术摘要分析在最近10年的主要进展是离线摘要技术,即在程序分析之前对常用代码库生成摘要,从而加快 使用这些代码库的客户端的分析速度离线摘要根据其自动化程度的不同,可以分成人工编写摘要和自动生成 摘要,分别在接下来的两小节中加以介绍 1)人工编写摘要 对于程序中一些难以分析的代码,例如第三方的库和系统代码等,可采用人工编写摘要的方式近似代码的 行为这种技术原先应用于程序验证中,比如ESC/Java通过用户提供的前置条件和后置条件来对程序进行模块 化验证 Flow!∽在处理调用系统代码和调用其他组件时,采用由人工来编写的近似摘要这样的摘要能够 模拟被调模块中的常见数据流路径这种方式没有考虑到用户编写的代码对被调模块的影响Ali和 Hotan7,8 提出了一种对库建立轻量级的上近似摘要这种摘要的建立,需要代码库满足分离编译假设( separate compilation assumption),无需应用代码即可编译代码库Java代码库普遍满足这项假设.在该假设约束下的Java 标准库被简化为一个人工编写的占位库而这个占位库的文件仅有80KB大小,远小于Java标准库的原本大小 Ali和 Hotak:3的方法改造了现有的全程序调用图构造算法,以占位库作为所有库函数的替代品,所有应用代 与库函数代码间的调用关系被简化为应用代码与占位库间的调用关系该方法既提升了效率(10倍以上),又 保证了正确性,并且有足够的精确度 2)自动生成摘要 在程序分析过程前创建摘要,通常是对程序常用的模块(如Java代码库)进行摘要分析,随后加速客户代码 的分析诸多的未知信息和代码库太大造成算法难以扩展 cousot从理论上总结了创建模块摘要的各种方 式该工作首先分析了创建模块摘要的主要问题是处理模块间的环形依赖在没有环形依赖时,我们可以按照依 赖关系给模块排一个顺序,每个模块只依赖于之前的模块,然后按顺序依次分析但是,由于环形依赖的存在, 有环形依赖的模块就只能被当作一个模块分析使得创建模块的摘要无法进行.文献「80]针对环形依赖给出了3 种解决方案
张健 等:程序分析研究进展 85 用中. Reps 等人[67]后续进一步扩展了该框架,通过已有抽象域为环境而计算得到新的属性,用于过程间常数传播 等应用中,并形式化定义了上述图可达问题为上下文无关文法图可达问题.上下文无关文法图可达问题对图中 的边进行标号,图中任意两点可达需要两点间的一条路径上的标号串满足事先定义的上下文无关文法.多种不 同程序分析问题均可表示为对上下文无关文法图可达问题的求解.近年来,包括指针分析[68,69]、并行程序分 析[70,71]等多种分析技术均通过求解上下文无关文法图可达问题来有效地加以实现. 2) 基于值流图的稀疏数据流分析方法 传统的数据流分析在程序控制流图上将所需计算的状态信息在每个程序点传播得到最终分析结果.此过 程通常存在较多冗余操作,对效率,特别是过程间数据流分析效率会有很大影响.为了进一步提高数据流分析的 效率,近年来,研究者们提出了多种稀疏的分析方法,从而无需计算状态信息在每个程序点的传播即可得到与数 据流分析相同的结果.该类分析技术[7276]通过一个稀疏的值流图(value flow graph)直接表示程序变量的依赖关 系,从而使得状态信息可以有效地在该稀疏的值流图上传播.该值流图保证了状态信息可以有效地传播到其需 要使用该信息的程序点,并避免了在无效程序点的冗余传播,可大幅度提高效率. 2.3 基于摘要的过程间分析 摘要(summary)是可复用的程序模块分析结果,能够简要地刻画模块的外部行为.创建摘要和利用摘要开展 分析的过程称为摘要分析.在编写程序的过程中,一个程序模块往往需要调用其他程序模块.对主调(caller)模块 的分析必然涉及到对被调模块(callee)的分析.与复用被调模块代码可提高软件生产效率类似,摘要分析期望复 用被调模块的分析结果也能提高分析主调模块的效率.通过基于摘要的程序分析技术,我们将被复用模块的分 析结果被构造成为摘要,并在分析主调模块时对其实例化,以加快分析速度. 传统摘要分析的研究主要关注模块化(modular)分析,即:在分析过程中将软件划分为多个模块,对各个模块 分别分析和创建摘要,然后合并摘要获得整体的分析结果.这样,在分析过程中创建摘要的技术也称为在线摘要 技术.摘要分析在最近 10 年的主要进展是离线摘要技术,即:在程序分析之前对常用代码库生成摘要,从而加快 使用这些代码库的客户端的分析速度.离线摘要根据其自动化程度的不同,可以分成人工编写摘要和自动生成 摘要,分别在接下来的两小节中加以介绍. 1) 人工编写摘要 对于程序中一些难以分析的代码,例如第三方的库和系统代码等,可采用人工编写摘要的方式近似代码的 行为.这种技术原先应用于程序验证中,比如 ESC/Java 通过用户提供的前置条件和后置条件来对程序进行模块 化验证.FlowDroid[66]在处理调用系统代码和调用其他组件时,采用由人工来编写的近似摘要.这样的摘要能够 模拟被调模块中的常见数据流路径.这种方式没有考虑到用户编写的代码对被调模块的影响.Ali 和 Lhoták[77,78] 提出了一种对库建立轻量级的上近似摘要.这种摘要的建立,需要代码库满足分离编译假设(separate compilation assumption),无需应用代码即可编译代码库.Java 代码库普遍满足这项假设.在该假设约束下的 Java 标准库被简化为一个人工编写的占位库,而这个占位库的文件仅有 80KB 大小,远小于 Java 标准库的原本大小. Ali 和 Lhoták[77,78]的方法改造了现有的全程序调用图构造算法,以占位库作为所有库函数的替代品,所有应用代 码与库函数代码间的调用关系被简化为应用代码与占位库间的调用关系.该方法既提升了效率(10 倍以上),又 保证了正确性,并且有足够的精确度. 2) 自动生成摘要 在程序分析过程前创建摘要,通常是对程序常用的模块(如 Java 代码库)进行摘要分析,随后加速客户代码 的分析.诸多的未知信息[79]和代码库太大造成算法难以扩展.Cousot[80]从理论上总结了创建模块摘要的各种方 式.该工作首先分析了创建模块摘要的主要问题是处理模块间的环形依赖.在没有环形依赖时,我们可以按照依 赖关系给模块排一个顺序,每个模块只依赖于之前的模块,然后按顺序依次分析.但是,由于环形依赖的存在,所 有环形依赖的模块就只能被当作一个模块分析,使得创建模块的摘要无法进行.文献[80]针对环形依赖给出了 3 种解决方案
Journal of software软件学报Vol.30,No.1, January2019 ·基于简化的分析:这个方案的思路是针对环形依赖导致的大模块上的分析通过标准的编译技术(如 partial evaluation)进行化简提高分析速度每个模块上的分析程序可以被当成是一个函数,然后,把这 些函数看成是标准程序之后就可以应用普通的程序分析进行化简了; ·最坏情况分析:每个模块分别分析,对于该模块所依赖的其他模块作最坏情况假设.这样的分析会导致 不精确,并且在多数情况下严重不精确; ·符号化关系型分析:把未知的信息做成符号化信息,然后把程序分析转变成符号化分析所有与符号化 相关的部分不进行计算 Smaragdakis等人提出了针对所有流不敏感指针分析的代码库预处理技术,属于基于简化的分析该工作 发现:当代码中存在符合图代码模式时,将模式中的冗余语句删除,进而避免冗余运算,加速代码分析 Rountev和 yder2提出了另一种代码库的简化方式,对库的摘要就是把库里面所有的赋值语句提取出来这个摘要本身 只是省掉了语法分析的时间然后在摘要上进行了两个优化 a)对于连续赋值,比如a=b,c=a,去掉中间变量,替换成c=b b)去掉与客户端无关的赋值语句 这两个优化能省掉4%69%的时间该方法仅支持上下文不敏感且流不敏感的分析 Rountev等人3提出的构件级别分析( (component-level analysis)对代码库的IFDS/DE框架进行了摘要分 析该方法采用 Sharir和 Pnueli提出的函数型分析方法,为过程内的数据流和过程间的部分数据流建立了摘 要对于过程间边相关的未知量,即虚函数调用( virtual function)和回调点( callback site),该方法在计算过程中不 予考虑该方法只考虑了函数中的局部变量 tubEroid在 FlowDroid的基础上采用了构件级别分析对库进行 了自动分析,支持多层字段敏感性无需手动编写摘要 Tang等人提出了条件可达性解决了传统摘要无法描述的回调函数问题具体而言该工作考虑了过程 间的数据依赖分析当代码库存在回调函数时,部分信息缺失导致已有方法难以为代码库建立有效的摘要.为了 处理回调函数带来的影响该工作提出了基于树邻接语言的可达性的摘要分析技术注意到包含回调函数信息 的可达性关系(称为“条件可达性关系”)可用于加速用户代码的分析为描述条件可达性关系该工作引入了原 本用于描述自然语言语法的形式语言一一树-邻接语言提出了树邻接语言的可达性分析技术树邻接语言可 性扩展了表达两点间可达关系的传统上下文无关语言可达性,具有表达4个点之间的可达关系的能力,从 更自然地描述了上述条件可达性关系实验结果表明:建立基于树-邻接语言的可达性摘要可以在合理的时间内 完成该技术所建立的摘要可以使得对用户代码分析的效率平均提高约8倍在后续工作中,ang等人进一步 将该方法扩展到了 Dyck-CFL可达性分析上该方法通过直接在较为通用的CFL可达性分析过程中引入带 条件边,使得大量基于CFL可达性的分析就可以直接支持条件摘要同时,该方法引入桥接边来避免条件组合爆 炸的问题通过这些处理,该方法避免了原有的Dyck-CFL分析中摘要不完整和分析效率不高的问题实验结果 表明,其分析速度相比树-邻接语言进一步提升了3倍多 由于模块含有大量的未知量,建立考虑所有情况的摘要在许多分析任务中非常困难所以,一些工作通过动 态程序分析或训练的方式建立了部分摘要 Palepu等人例提出了加速程序分析速度的动态依赖摘要技术 ynamic dependence summary),提前创建软件库的摘要用来快速创建程序切片尽管得到的是不充分的摘要, 导致生成的程序切片并不保证完全正确,然而在程序测试的实践中能够找到大部分的错误 Kulkarni等人采 用跨程序的训练办法为代码库建立不完整的摘要,以提高客户代码的分析速度该方法基于 Datalog语言,有效 地对中间计算过程进行剪枝并将剪枝结果记录于摘要中同时该方法还对 Datalog语言进行改造,使得利用摘 要进行分析时可以跳过中间计算过程该方法保证正确性的方式是人工编写时间复杂度较低的规则判断训练 得到的摘要是否能够保证正确:如果不能保证正确性,则不采用摘要来进行计算 上述工作都是针对整个代码库进行摘要分析当精度要求较高时分析完整的代码库比较困难部分工作只 对单个函数进行分析 Yorsh等人提出的框架可以为函数建立精确而简练的函数摘要在不同上下文环境中 采用函数摘要与重新分析函数所得到的最终结果相同,从而保证精确性框架中采用有限显式输入输出表来表
86 Journal of Software 软件学报 Vol.30, No.1, January 2019 基于简化的分析:这个方案的思路是针对环形依赖导致的大模块上的分析通过标准的编译技术(如 partial evaluation)进行化简,提高分析速度.每个模块上的分析程序可以被当成是一个函数,然后,把这 些函数看成是标准程序之后就可以应用普通的程序分析进行化简了; 最坏情况分析:每个模块分别分析,对于该模块所依赖的其他模块作最坏情况假设.这样的分析会导致 不精确,并且在多数情况下严重不精确; 符号化关系型分析:把未知的信息做成符号化信息,然后把程序分析转变成符号化分析.所有与符号化 相关的部分不进行计算. Smaragdakis 等人[81]提出了针对所有流不敏感指针分析的代码库预处理技术,属于基于简化的分析.该工作 发现:当代码中存在符合图代码模式时,将模式中的冗余语句删除,进而避免冗余运算,加速代码分析.Rountev 和 Ryder[82]提出了另一种代码库的简化方式,对库的摘要就是把库里面所有的赋值语句提取出来.这个摘要本身 只是省掉了语法分析的时间.然后在摘要上进行了两个优化. a) 对于连续赋值,比如 a=b;c=a;去掉中间变量,替换成 c=b; b) 去掉与客户端无关的赋值语句. 这两个优化能省掉 4%~69%的时间.该方法仅支持上下文不敏感且流不敏感的分析. Rountev 等人[83,84]提出的构件级别分析(component-level analysis)对代码库的 IFDS/IDE 框架进行了摘要分 析.该方法采用 Sharir 和 Pnueli[85]提出的函数型分析方法,为过程内的数据流和过程间的部分数据流建立了摘 要.对于过程间边相关的未知量,即虚函数调用(virtual function)和回调点(callback site),该方法在计算过程中不 予考虑.该方法只考虑了函数中的局部变量.StubDroid[86]在 FlowDroid 的基础上采用了构件级别分析对库进行 了自动分析,支持多层字段敏感性,无需手动编写摘要. Tang 等人[87]提出了条件可达性,解决了传统摘要无法描述的回调函数问题.具体而言,该工作考虑了过程 间的数据依赖分析.当代码库存在回调函数时,部分信息缺失导致已有方法难以为代码库建立有效的摘要.为了 处理回调函数带来的影响,该工作提出了基于树-邻接语言的可达性的摘要分析技术.注意到包含回调函数信息 的可达性关系(称为“条件可达性关系”)可用于加速用户代码的分析.为描述条件可达性关系,该工作引入了原 本用于描述自然语言语法的形式语言——树-邻接语言,提出了树-邻接语言的可达性分析技术.树-邻接语言可 达性扩展了表达两点间可达关系的传统上下文无关语言可达性,具有表达 4 个点之间的可达关系的能力,从而 更自然地描述了上述条件可达性关系.实验结果表明:建立基于树-邻接语言的可达性摘要可以在合理的时间内 完成,该技术所建立的摘要可以使得对用户代码分析的效率平均提高约 8 倍.在后续工作中[88],Tang 等人进一步 将该方法扩展到了 Dyck-CFL 可达性分析上.该方法通过直接在较为通用的 CFL 可达性分析过程[67]中引入带 条件边,使得大量基于 CFL 可达性的分析就可以直接支持条件摘要.同时,该方法引入桥接边来避免条件组合爆 炸的问题.通过这些处理,该方法避免了原有的 Dyck-CFL 分析中摘要不完整和分析效率不高的问题.实验结果 表明,其分析速度相比树-邻接语言进一步提升了 3 倍多. 由于模块含有大量的未知量,建立考虑所有情况的摘要在许多分析任务中非常困难.所以,一些工作通过动 态程序分析或训练的方式建立了部分摘要.Palepu 等人[89]提出了加速程序分析速度的动态依赖摘要技术 (dynamic dependence summary),提前创建软件库的摘要,用来快速创建程序切片.尽管得到的是不充分的摘要, 导致生成的程序切片并不保证完全正确,然而在程序测试的实践中能够找到大部分的错误.Kulkarni 等人[90]采 用跨程序的训练办法为代码库建立不完整的摘要,以提高客户代码的分析速度.该方法基于 Datalog 语言,有效 地对中间计算过程进行剪枝,并将剪枝结果记录于摘要中.同时,该方法还对 Datalog 语言进行改造,使得利用摘 要进行分析时可以跳过中间计算过程.该方法保证正确性的方式是人工编写时间复杂度较低的规则,判断训练 得到的摘要是否能够保证正确:如果不能保证正确性,则不采用摘要来进行计算. 上述工作都是针对整个代码库进行摘要分析.当精度要求较高时,分析完整的代码库比较困难.部分工作只 对单个函数进行分析.Yorsh 等人[91]提出的框架可以为函数建立精确而简练的函数摘要.在不同上下文环境中, 采用函数摘要与重新分析函数所得到的最终结果相同,从而保证精确性.框架中采用有限显式输入输出表来表
张健等:程序分析研究进展 示摘要并通过摘要组合操作,使得不同上下文之下分析过程的相似之处得以合并为更加简练的形式,从而利用 有限的数据结构表达无限可能的函数行为该框架采用了微转换子,微转换子可以编码的问题包括 IFDS/IDE问 题该框架还可以解决模块的线性常量传播问题和模块的类型状态叼检验问题 Dlig等人的工作是针对C的上下文敏感、流敏感、不考虑字段的函数指向分析核心问题是分析一个 函数时如何考虑所有可能的调用上下文解决方案是将函数参数所有可能的别名关系编码到一个二部图上 边是参数另一边是符号化的位置,表示彼此不交的内存地址集合,中间连上带约束的边,编码了不同的别名关 系当遇到语句的转移函数时则采用图上再加一层的方法来保证流敏感性,这样可以做到强更新函数调用处理 方面需要计算出被调函数的别名情况,实例化主调函数的摘要,再把调用函数的图和被调函数实例化的图拼起 来通过不动点算法计算出一个上近似的结果. 24符号执行 符号执行明是一种相对精确的程序分析技术传统的符号执行技术使用符号化输入代替实际输入以模 拟执行(不实际执行)被分析程序程序中的操作被转化为相应的符号表达式操作在遇到条件语句时,程序的执 行也相应地分叉以探索每个分支,分支条件则被加入到当前路径的路径条件( path condition)中通过调用SAT/ SMT求解器对路径条件的可满足性进行求解来加以判断:如果判定结果为可满足,则说明路径实际可行(存在 具体输入能够让程序产生此路径)如果判定结果为不可满足,则表明此路径不可行,终止对该路径的分析 在约束条件可被判定的情况下,符号执行提供了一种系统遍历程序路径空间的手段符号执行中的程序路 径精确刻画了程序路径上的信息,可基于路径信息开展多种软件验证确认阶段的活动,包括自动测试、缺陷查 找以及部分的程序验证等理论上相比于需要固定程序输入的分析方法符号执行通过符号分析可覆盖更 多的程序行为另一方面符号执行技术依赖于 SAT/SMT技术,求解器的能力是决定符号执行效果的关键因素 符号执行中,程序路径空间大小随着程序规模的扩大而呈指数级增长例如:单就串行程序而言,一个具有n个条 件语句的程序段就有可能包含2”条路径这也是制约符号执行能力的关键因 最初符号执行主要用于程序自动测试但受制于当时的计算能力和求解技术与工具的能力,符号执行技术 并没有得到实际的应用近年来随着计算能力的提高、 SAT/SMT技术和工具的蓬勃发展-10,号执行技术 得到了长足的进步,出现了以动态符号执行( concolic testing0210为代表的一批新的符号执行方法或技术,以 及以SAGE0、KLEE0、SP10、Pex10、S2E108为代表的符号执行工具 不同于传统的符号执行,动态符号执行0210实际运行被分析的程序在实际运行的同时收集运行路径上 的路径条件然后翻转路径条件得到新的路径条件通过对新的路径条件进行求解得到新的程序输入以再一次 运行被分析程序,从而探索与之前运行不同的程序路径由于在实际运行程序过程中动态符号执行在碰到复 杂或不可解的路径条件时,可以使用实际值来简化路径条件在碰到外部调用时,也可以通过实际执行来缓解外 部调用的问题因此在方法层面动态符号执行通过牺牲部分分析的可靠性来提高方法的可扩展性和可行性 目前符号执行技术仍然面临提高可扩展性( scalability)与可行性( feasibility)这两方面的挑战可扩展性挑 战是指如何在有限资源(比如时间、内存)的前提下提高符号执行的效率,更快地达成分析目标;可行性挑战是指 如何支持不同类型分析目标的符号执行权衡分析的可靠性与精确性已有的研究工作基本都是围绕这两个方 面展开 在可扩展性方面路径空间爆炸和约束求解是主要的两大难题在缓解路径空间爆炸方面,目前己有的工作 基本分为两个思路:(1)在具体目标下提供高效的搜索策略,使符号执行分析更快地达到目标,包括提高程序的 覆盖率10.09-11判断某个程序点是否可达1产生满足正规性质的程序路径11、探索程序不同版本的差 异部分14等,(2)通过约束输入范围、削减或合并路径来减小程序的路径空间,包括基于输入模版61n、程 序切片1-1.程序抽象(包括摘要技术}219、偏序约减,3、条件合并13213以及等价路径约减121 等一些方法在约束求解方面已有的工作也可分为两个方面(1)在调用求解器之前对路径条件的查询进行优 化,以减少求解器的调用次数或缩短求解时间包括查询缓存和重用01319、基于约束独立性的优化10,10、 增量式求解10,14等(2)支持复杂程序特征的高效编码,包括对机器数100、数组00浮点1145、字符
张健 等:程序分析研究进展 87 示摘要,并通过摘要组合操作,使得不同上下文之下分析过程的相似之处得以合并为更加简练的形式,从而利用 有限的数据结构表达无限可能的函数行为.该框架采用了微转换子,微转换子可以编码的问题包括 IFDS/IDE 问 题.该框架还可以解决模块的线性常量传播问题和模块的类型状态[92]检验问题. Dillig 等人[93]的工作是针对 C 的上下文敏感、流敏感、不考虑字段的函数指向分析.核心问题是分析一个 函数时,如何考虑所有可能的调用上下文.解决方案是将函数参数所有可能的别名关系编码到一个二部图上,一 边是参数,另一边是符号化的位置,表示彼此不交的内存地址集合,中间连上带约束的边,编码了不同的别名关 系.当遇到语句的转移函数时则采用图上再加一层的方法来保证流敏感性,这样可以做到强更新.函数调用处理 方面,需要计算出被调函数的别名情况,实例化主调函数的摘要,再把调用函数的图和被调函数实例化的图拼起 来.通过不动点算法计算出一个上近似的结果. 2.4 符号执行 符号执行[9497]是一种相对精确的程序分析技术.传统的符号执行技术使用符号化输入代替实际输入以模 拟执行(不实际执行)被分析程序,程序中的操作被转化为相应的符号表达式操作.在遇到条件语句时,程序的执 行也相应地分叉以探索每个分支,分支条件则被加入到当前路径的路径条件(path condition)中.通过调用 SAT/ SMT 求解器,对路径条件的可满足性进行求解来加以判断:如果判定结果为可满足,则说明路径实际可行(存在 具体输入能够让程序产生此路径);如果判定结果为不可满足,则表明此路径不可行,终止对该路径的分析. 在约束条件可被判定的情况下,符号执行提供了一种系统遍历程序路径空间的手段.符号执行中的程序路 径精确刻画了程序路径上的信息,可基于路径信息开展多种软件验证确认阶段的活动,包括自动测试、缺陷查 找以及部分的程序验证等[98].理论上,相比于需要固定程序输入的分析方法,符号执行通过符号分析,可覆盖更 多的程序行为.另一方面,符号执行技术依赖于 SAT/SMT 技术,求解器的能力是决定符号执行效果的关键因素. 符号执行中,程序路径空间大小随着程序规模的扩大而呈指数级增长.例如:单就串行程序而言,一个具有 n 个条 件语句的程序段就有可能包含 2n 条路径,这也是制约符号执行能力的关键因素. 最初,符号执行主要用于程序自动测试,但受制于当时的计算能力和求解技术与工具的能力,符号执行技术 并没有得到实际的应用.近年来,随着计算能力的提高、SAT/SMT 技术和工具的蓬勃发展[99101],符号执行技术 得到了长足的进步,出现了以动态符号执行(concolic testing)[102,103]为代表的一批新的符号执行方法或技术,以 及以 SAGE[104]、KLEE[105]、SPF[106]、Pex[107]、S2E[108]为代表的符号执行工具. 不同于传统的符号执行,动态符号执行[102,103]实际运行被分析的程序,在实际运行的同时收集运行路径上 的路径条件,然后翻转路径条件得到新的路径条件,通过对新的路径条件进行求解得到新的程序输入以再一次 地运行被分析程序,从而探索与之前运行不同的程序路径.由于在实际运行程序过程中,动态符号执行在碰到复 杂或不可解的路径条件时,可以使用实际值来简化路径条件.在碰到外部调用时,也可以通过实际执行来缓解外 部调用的问题.因此,在方法层面,动态符号执行通过牺牲部分分析的可靠性来提高方法的可扩展性和可行性. 目前,符号执行技术仍然面临提高可扩展性(scalability)与可行性(feasibility)这两方面的挑战:可扩展性挑 战是指如何在有限资源(比如时间、内存)的前提下提高符号执行的效率,更快地达成分析目标;可行性挑战是指 如何支持不同类型分析目标的符号执行,权衡分析的可靠性与精确性.已有的研究工作基本都是围绕这两个方 面展开. 在可扩展性方面,路径空间爆炸和约束求解是主要的两大难题.在缓解路径空间爆炸方面,目前已有的工作 基本分为两个思路:(1) 在具体目标下提供高效的搜索策略,使符号执行分析更快地达到目标,包括提高程序的 覆盖率[105,109111]、判断某个程序点是否可达[112]、产生满足正规性质的程序路径[113]、探索程序不同版本的差 异部分[114,115]等;(2) 通过约束输入范围、削减或合并路径来减小程序的路径空间,包括基于输入模版[116,117]、程 序切片[118121]、程序抽象(包括摘要技术) [122129]、偏序约减[130,131]、条件合并[132,133]以及等价路径约减[121,134136] 等一些方法.在约束求解方面,已有的工作也可分为两个方面:(1) 在调用求解器之前对路径条件的查询进行优 化,以减少求解器的调用次数或缩短求解时间,包括查询缓存和重用[105,137139]、基于约束独立性的优化[103,105]、 增量式求解[105,140]等;(2) 支持复杂程序特征的高效编码,包括对机器数[104,105]、数组[100,105]、浮点[141145]、字符
Journal of software软件学报Vol.30,No.1, January2019 串4、动态数据结构14-14等方面的支持 在可行性方面环境建模和多形态分析目标的支持是目前的主要问题在环境建模方面,已有的工作基本都 是在分析的精确性、可靠性、建模工作量以及可扩展性之间进行权衡和折中,包括手工建模030、自动合 成1、动态执行1、全栈执行108等在多形态分析目标方面主要是应对多语言和多应用领域的复杂性包括 二进制程序10815.2、脚本语言程序、分布式程序、数据库操作程序15、无线传感器网络程序156、 并发或并行程序35158、嵌入式程序19、PLC程序1等符号执行方法 同时,面向新的分析需求,也有一些新的符号执行技术出现,其中比较有代表性的是概率符号执行技 术16-16,其基本思想是通过符号执行来得到程序的路径,然后使用SMT解空间体积计算技术来计算每条路径 的路径条件的解的个数,通过每条路径对应的解的个数,可以计算每条路径的概率基于此可以开展包括低概 率缺陷查找、低概率路径的测试用例生成、生成程序的性能分布6、刻画代码变迁16等活动 随着符号执行技术近些年的发展符号执行技术在工业界也得到了实际的采纳和应用,其中有代表性的工 作有微软公司把自己开发的二进制动态符号执行工具SAGE用于Win7的测试发现了文件模糊测试中1/3的 16由于SAGE通常是微软公司最后使用的缺陷检测工具,因此这些由SAGE发现的缺陷,很多都没有被 之前在开发过程中使用的静态分析工具、黑盒测试工具所发现微软公司多个开发小组已把SAGE作为日常 具在使用,SAGE目前也被商业化为微软公司的安全风险检测( microsoft security risk detection)服务微软公司在 Visual studio2015中正式发布了基于动态符号执行的C#自动单元测试工具 IntelliTestl6,可大幅度提高C#程 序单元的测试效率C程序符号执行工具KLEE0对 GnU Coreutils程序集进行了自动测试可自动达到94%的 语句覆盖率并发现3个程序崩溃问题 analyze6s在开源软件中发现数百个真实缺陷并在工业界嵌入式系统 中发现两个缺陷2016年8月,在美国 DARPA举办的网络空间安全竞赛(CGC中最终排名前三的参赛队伍全 部使用了符号执行技术,用于自动发现并利用二进制程序中的漏洞美国 GrammaTech公司开发的商业程序分 析工具 Codesonar中也使用了符号执行技术,用以发现程序中的深层缺陷 未来,符号执行技术将进一步在软件工程、安全、系统、网络等相关领域的实际需求驱动下不断发展面 向大规模软件的高效符号执行方法、技术和工具将是下一步研究所面临的挑战和重点同时符号执行搜索策 略的更加智能化1也将是下一步的研究重点此外,与其他技术在不同层面的密切结合1013,以进一步提高 件分析效果,也将成为符号执行后续的研究趋势之 2.5动态分析 动态分析是指通过在指定测试用例下运行给定的程序,并分析程序运行过程或结果用于缺陷检测等与静 态分析相比,动态分析能够更好地处理编程语言中的动态属性例如指针、动态绑定、面向对象语言中的多态 与继承、线程交替等动态分析在一定程度上弥补了静态分析的不足之处 基本的程序动态分析可以简单地分为在线 online)动态分析与离线( Offline)动态分析在线动态分析是指 在程序的运行过程中分析当前程序行为;而离线动态分析需要记录程序的运行行为在程序运行结束后再进行 分析两者的基本思想都是通过对程序运行过程或者结果的分析,查找定位缺陷.具体来说,一方面可以将程序 运行结果和预知结果对比确定程序中是否含有缺陷;另一方面,可以通过插桩或其他监控技术分析程序的运行 行为,查找错误的行为前者很直观但是对于被触发了却没有反映在输出中的缺陷无法检测后者则可以直 观察到程序中缺陷的触发,即使该次触发并没有导致错误的输出但是后者需要提前定义错误的行为,其对于非 常见的缺陷无法检测已有文献中有大量这方面的介绍174 程序动态分析,从报告缺陷的准确性出发也可以分为(1)缺陷动态检测、(2)缺陷动态预测.一般所指的缺 陷动态査找方法是缺陷动态检测,是指在程序的运行过程中某个缺陷已经发生了之后的检测,即,缺陷已经反映 在程序行为中或者运行结果中其关注点是:如何设计检测算法等保证将所有己经发生的缺陷检测出来然而 程序中的不同缺陷不会都在有限的若干测试用例中被触发因此,为了提高缺陷动态检测的有效性需要从程序 若干次运行中预测出该程序潜在的某些行为,并判断这些潜在行为是否会触发缺陷这种方法称为缺陷的动态 预测例如:某个程序中存在一个缓冲区溢出缺陷,该缺陷只有在输入 Input大于128时发生那么,如果我们可以
88 Journal of Software 软件学报 Vol.30, No.1, January 2019 串[146]、动态数据结构[147149]等方面的支持. 在可行性方面,环境建模和多形态分析目标的支持是目前的主要问题.在环境建模方面,已有的工作基本都 是在分析的精确性、可靠性、建模工作量以及可扩展性之间进行权衡和折中,包括手工建模[105,106]、自动合 成[150]、动态执行[102]、全栈执行[108]等.在多形态分析目标方面,主要是应对多语言和多应用领域的复杂性,包括 二进制程序[108,151,152]、脚本语言程序[153]、分布式程序[154]、数据库操作程序[155]、无线传感器网络程序[156]、 并发或并行程序[135,157,158]、嵌入式程序[159]、PLC 程序[160]等符号执行方法. 同时,面向新的分析需求,也有一些新的符号执行技术出现,其中比较有代表性的是概率符号执行技 术[161163],其基本思想是:通过符号执行来得到程序的路径,然后使用 SMT 解空间体积计算技术来计算每条路径 的路径条件的解的个数,通过每条路径对应的解的个数,可以计算每条路径的概率.基于此,可以开展包括低概 率缺陷查找、低概率路径的测试用例生成、生成程序的性能分布[164]、刻画代码变迁[165]等活动. 随着符号执行技术近些年的发展,符号执行技术在工业界也得到了实际的采纳和应用,其中有代表性的工 作有:微软公司把自己开发的二进制动态符号执行工具 SAGE 用于 Win 7 的测试,发现了文件模糊测试中 1/3 的 缺陷[166].由于 SAGE 通常是微软公司最后使用的缺陷检测工具,因此,这些由 SAGE 发现的缺陷,很多都没有被 之前在开发过程中使用的静态分析工具、黑盒测试工具所发现.微软公司多个开发小组已把 SAGE 作为日常工 具在使用,SAGE 目前也被商业化为微软公司的安全风险检测(microsoft security risk detection)服务.微软公司在 Visual Studio 2015 中正式发布了基于动态符号执行的 C#自动单元测试工具 IntelliTest[167],可大幅度提高 C#程 序单元的测试效率.C 程序符号执行工具 KLEE[105]对 GNU Coreutils 程序集进行了自动测试,可自动达到 94%的 语句覆盖率,并发现 3 个程序崩溃问题;Canalyze[168]在开源软件中发现数百个真实缺陷,并在工业界嵌入式系统 中发现两个缺陷.2016 年 8 月,在美国 DARPA 举办的网络空间安全竞赛(CGC)中,最终排名前三的参赛队伍全 部使用了符号执行技术,用于自动发现并利用二进制程序中的漏洞.美国 GrammaTech 公司开发的商业程序分 析工具 CodeSonar 中也使用了符号执行技术,用以发现程序中的深层缺陷. 未来,符号执行技术将进一步在软件工程、安全、系统、网络等相关领域的实际需求驱动下不断发展.面 向大规模软件的高效符号执行方法、技术和工具将是下一步研究所面临的挑战和重点.同时,符号执行搜索策 略的更加智能化[169]也将是下一步的研究重点.此外,与其他技术在不同层面的密切结合[170173],以进一步提高 软件分析效果,也将成为符号执行后续的研究趋势之一. 2.5 动态分析 动态分析是指通过在指定测试用例下运行给定的程序,并分析程序运行过程或结果,用于缺陷检测等.与静 态分析相比,动态分析能够更好地处理编程语言中的动态属性,例如指针、动态绑定、面向对象语言中的多态 与继承、线程交替等.动态分析在一定程度上弥补了静态分析的不足之处. 基本的程序动态分析可以简单地分为在线(online)动态分析与离线(offline)动态分析[1].在线动态分析是指 在程序的运行过程中分析当前程序行为;而离线动态分析需要记录程序的运行行为,在程序运行结束后再进行 分析.两者的基本思想都是通过对程序运行过程或者结果的分析,查找定位缺陷.具体来说,一方面可以将程序 运行结果和预知结果对比,确定程序中是否含有缺陷;另一方面,可以通过插桩或其他监控技术分析程序的运行 行为,查找错误的行为.前者很直观,但是对于被触发了却没有反映在输出中的缺陷无法检测;后者则可以直接 观察到程序中缺陷的触发,即使该次触发并没有导致错误的输出.但是后者需要提前定义错误的行为,其对于非 常见的缺陷无法检测.已有文献中有大量这方面的介绍[174]. 程序动态分析,从报告缺陷的准确性出发,也可以分为:(1) 缺陷动态检测;(2) 缺陷动态预测.一般所指的缺 陷动态查找方法是缺陷动态检测,是指在程序的运行过程中某个缺陷已经发生了之后的检测,即,缺陷已经反映 在程序行为中或者运行结果中.其关注点是:如何设计检测算法等,保证将所有已经发生的缺陷检测出来.然而, 程序中的不同缺陷不会都在有限的若干测试用例中被触发.因此,为了提高缺陷动态检测的有效性,需要从程序 若干次运行中预测出该程序潜在的某些行为,并判断这些潜在行为是否会触发缺陷.这种方法称为缺陷的动态 预测.例如:某个程序中存在一个缓冲区溢出缺陷,该缺陷只有在输入 input 大于 128 时发生.那么,如果我们可以
张健等:程序分析研究进展 从某个 Input不大于128的输入下预测对应行为是一个潜在缺陷,其可能会在 Input大于128时发生进一步地, 我们可以构造一个满足预测条件的输入,再次运行程序去触发(验证)缺陷缺陷的动态预测在并发程序的动态 分析中经常用到,主要原因之一是:并发程序的运行除了与输入有关外,还与程序中线程之间的调度有关程序 缺陷的动态预测还会涉及到一些其他技术,例如,测试用例生成、约束求解、缺陷重现、线程调度等,其分析过 程与缺陷动态检测相比更为复杂 2.6基于机器学习的程序分析 经典的程序分析技术提供相对精确的分析结果,但同时也带来了包括路径组合爆炸、误报率较高等一系列 在实践中不可避免却难以应对的问题随着近年来通用计算设备能力的提高,海量的程序执行数据被存储和管 研究者采用机器学习、统计分析等系列技术提升现有的程序分析能力 现有的程序分析技术依赖于一定的启发式策略,如符号执行技术中的深度(或广度)优先搜索在动态分析 技术中,为了达到分析精度,这些策略可能带来较高的计算成本基于现有的标记数据(即已知分析结果的程序) 建立学习模型,机器学习技术可以学习新的可自适应的策略,减少启发式策略带来的成本消耗Li等人4为了 解决符号执行中的路径可达性问题,以最小化不满足性为目标,建立机器学习模型MLB,以减少经典的约束求 解方案在求解非线性约束及函数调用时的不足Kong等人面向自动机验证,研究了多个随机测试与符号执 行技术的整合策略通过调整状态转移概率优化动态符号执行Wang等人12提出了基于马尔可夫过程的动态 符号执行方法,以达到应用符号执行获得精确分析结果和应用随机测试覆盖搜索空间的平衡该方法采用贪心 算法获得优化模型的解,以期找到对应于近似最优性能的策略Chen等人1针对信息物理系统( cyber-physical system)的攻防模型,设计了基于程序变异的方案获得具有植入错误的模型训练数据以避免人工建立模型的巨 大成本Xong等人1提出了基于概率程序合成框架L2S该框架整合了包括程序合成的搜索空间、路径和潜 在解的概率估计方案能够按需地构建程序合成和修复技术,研究者可基于该框架深度定制和设计相关方法 在静态分析技术中,分析工具在获得较高的分析精度的同时,往往带来过高的误报率研究者建立了机器学 习模型,以剔除潜在的误报并减少静态分析的成本Heo等人1提出了基于异常点检测技术来滤除静态分析结 果中的误报该方法提取代码循环和函数调用中的特征,基于训练数据建立学习模型,识别潜在的误报并提升静 态分析的实用性Chae等人针对上下文敏感的指针分析,提出了基于分类器的自动特征抽取方案该方案可 有效提升现有的静态分析技术Oh等人8针对静态分析的精度和计算成本提出了基于贝叶斯优化的自适 应学习方案,并以此建立面向数据流和上下文的部分静态分析工具 Jeong等人设计了数据驱动的上下文敏 感的指针分析方案该方案通过非线性的上下文选择建立了识别上下文敏感函数的学习方法 3面向特定软件的程序分析技术 本节介绍程序分析技术在一些重点领域软件的应用,包括移动应用软件、并发软件、分布式系统、二进制 代码等方面的重要应用 3.1移动应用软件 近10年来,以智能手机为代表的智能终端以惊人的速度得以普及目前,以 Android和苹果iOS系统为代表 的智能手机数量和使用频度已远超个人计算机成为最流行的个人电子设备通过移动支付、购物和社交等各 式各样的移动应用,智能手机已经深度渗透进了人们的日常活动中相应地这些应用的运行状态和广大用户的 日常生活和工作有着直接的关系,也在很大程度上影响到了整个互联网的运转为此研究人员通过对移动应用 软件的程序分析,来检测其是否具有所期望的以安全性为核心的各种特性 1)污点分析技术 H于智能手机的使用特点移动应用的安全性分析常常可以归结为应用代码上跟踪敏感数据流的动态/静 态污点分析( taint analysis问题 动态污点分析最具代表性的 Android应用动态污点分析技术是 Taint Droid82,其通过修改的 Dalvik
张健 等:程序分析研究进展 89 从某个 input 不大于 128 的输入下预测对应行为是一个潜在缺陷,其可能会在 input 大于 128 时发生.进一步地, 我们可以构造一个满足预测条件的输入,再次运行程序去触发(验证)缺陷.缺陷的动态预测在并发程序的动态 分析中经常用到,主要原因之一是:并发程序的运行除了与输入有关外,还与程序中线程之间的调度有关.程序 缺陷的动态预测还会涉及到一些其他技术,例如,测试用例生成、约束求解、缺陷重现、线程调度等,其分析过 程与缺陷动态检测相比更为复杂. 2.6 基于机器学习的程序分析 经典的程序分析技术提供相对精确的分析结果,但同时也带来了包括路径组合爆炸、误报率较高等一系列 在实践中不可避免却难以应对的问题.随着近年来通用计算设备能力的提高,海量的程序执行数据被存储和管 理;研究者采用机器学习、统计分析等系列技术提升现有的程序分析能力. 现有的程序分析技术依赖于一定的启发式策略,如符号执行技术中的深度(或广度)优先搜索.在动态分析 技术中,为了达到分析精度,这些策略可能带来较高的计算成本.基于现有的标记数据(即已知分析结果的程序) 建立学习模型,机器学习技术可以学习新的可自适应的策略,减少启发式策略带来的成本消耗.Li 等人[144]为了 解决符号执行中的路径可达性问题,以最小化不满足性为目标,建立机器学习模型 MLB,以减少经典的约束求 解方案在求解非线性约束及函数调用时的不足.Kong 等人[175]面向自动机验证,研究了多个随机测试与符号执 行技术的整合策略,通过调整状态转移概率优化动态符号执行.Wang 等人[172]提出了基于马尔可夫过程的动态 符号执行方法,以达到应用符号执行获得精确分析结果和应用随机测试覆盖搜索空间的平衡.该方法采用贪心 算法获得优化模型的解,以期找到对应于近似最优性能的策略.Chen 等人[176]针对信息物理系统(cyber-physical system)的攻防模型,设计了基于程序变异的方案,获得具有植入错误的模型训练数据以避免人工建立模型的巨 大成本.Xiong 等人[177]提出了基于概率程序合成框架 L2S.该框架整合了包括程序合成的搜索空间、路径和潜 在解的概率估计方案,能够按需地构建程序合成和修复技术,研究者可基于该框架深度定制和设计相关方法. 在静态分析技术中,分析工具在获得较高的分析精度的同时,往往带来过高的误报率.研究者建立了机器学 习模型,以剔除潜在的误报并减少静态分析的成本.Heo 等人[178]提出了基于异常点检测技术来滤除静态分析结 果中的误报.该方法提取代码循环和函数调用中的特征,基于训练数据建立学习模型,识别潜在的误报并提升静 态分析的实用性.Chae 等人[59]针对上下文敏感的指针分析,提出了基于分类器的自动特征抽取方案.该方案可 有效提升现有的静态分析技术.Oh 等人[179,180]针对静态分析的精度和计算成本,提出了基于贝叶斯优化的自适 应学习方案,并以此建立面向数据流和上下文的部分静态分析工具.Jeong 等人[181]设计了数据驱动的上下文敏 感的指针分析方案.该方案通过非线性的上下文选择,建立了识别上下文敏感函数的学习方法. 3 面向特定软件的程序分析技术 本节介绍程序分析技术在一些重点领域软件的应用,包括移动应用软件、并发软件、分布式系统、二进制 代码等方面的重要应用. 3.1 移动应用软件 近 10 年来,以智能手机为代表的智能终端以惊人的速度得以普及.目前,以 Android 和苹果 iOS 系统为代表 的智能手机数量和使用频度已远超个人计算机,成为最流行的个人电子设备.通过移动支付、购物和社交等各 式各样的移动应用,智能手机已经深度渗透进了人们的日常活动中.相应地,这些应用的运行状态和广大用户的 日常生活和工作有着直接的关系,也在很大程度上影响到了整个互联网的运转.为此,研究人员通过对移动应用 软件的程序分析,来检测其是否具有所期望的以安全性为核心的各种特性. 1) 污点分析技术 由于智能手机的使用特点,移动应用的安全性分析常常可以归结为应用代码上跟踪敏感数据流的动态/静 态污点分析(taint analysis)问题. 动态污点分析:最具代表性的 Android 应用动态污点分析技术是 TaintDroid[182],其通过修改的 Dalvik