张健等:程序分析研究进展 示摘要并通过摘要组合操作,使得不同上下文之下分析过程的相似之处得以合并为更加简练的形式,从而利用 有限的数据结构表达无限可能的函数行为该框架采用了微转换子,微转换子可以编码的问题包括 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 符号执行 符号执行[9497]是一种相对精确的程序分析技术.传统的符号执行技术使用符号化输入代替实际输入以模 拟执行(不实际执行)被分析程序,程序中的操作被转化为相应的符号表达式操作.在遇到条件语句时,程序的执 行也相应地分叉以探索每个分支,分支条件则被加入到当前路径的路径条件(path condition)中.通过调用 SAT/ SMT 求解器,对路径条件的可满足性进行求解来加以判断:如果判定结果为可满足,则说明路径实际可行(存在 具体输入能够让程序产生此路径);如果判定结果为不可满足,则表明此路径不可行,终止对该路径的分析. 在约束条件可被判定的情况下,符号执行提供了一种系统遍历程序路径空间的手段.符号执行中的程序路 径精确刻画了程序路径上的信息,可基于路径信息开展多种软件验证确认阶段的活动,包括自动测试、缺陷查 找以及部分的程序验证等[98].理论上,相比于需要固定程序输入的分析方法,符号执行通过符号分析,可覆盖更 多的程序行为.另一方面,符号执行技术依赖于 SAT/SMT 技术,求解器的能力是决定符号执行效果的关键因素. 符号执行中,程序路径空间大小随着程序规模的扩大而呈指数级增长.例如:单就串行程序而言,一个具有 n 个条 件语句的程序段就有可能包含 2n 条路径,这也是制约符号执行能力的关键因素. 最初,符号执行主要用于程序自动测试,但受制于当时的计算能力和求解技术与工具的能力,符号执行技术 并没有得到实际的应用.近年来,随着计算能力的提高、SAT/SMT 技术和工具的蓬勃发展[99101],符号执行技术 得到了长足的进步,出现了以动态符号执行(concolic testing)[102,103]为代表的一批新的符号执行方法或技术,以 及以 SAGE[104]、KLEE[105]、SPF[106]、Pex[107]、S2E[108]为代表的符号执行工具. 不同于传统的符号执行,动态符号执行[102,103]实际运行被分析的程序,在实际运行的同时收集运行路径上 的路径条件,然后翻转路径条件得到新的路径条件,通过对新的路径条件进行求解得到新的程序输入以再一次 地运行被分析程序,从而探索与之前运行不同的程序路径.由于在实际运行程序过程中,动态符号执行在碰到复 杂或不可解的路径条件时,可以使用实际值来简化路径条件.在碰到外部调用时,也可以通过实际执行来缓解外 部调用的问题.因此,在方法层面,动态符号执行通过牺牲部分分析的可靠性来提高方法的可扩展性和可行性. 目前,符号执行技术仍然面临提高可扩展性(scalability)与可行性(feasibility)这两方面的挑战:可扩展性挑 战是指如何在有限资源(比如时间、内存)的前提下提高符号执行的效率,更快地达成分析目标;可行性挑战是指 如何支持不同类型分析目标的符号执行,权衡分析的可靠性与精确性.已有的研究工作基本都是围绕这两个方 面展开. 在可扩展性方面,路径空间爆炸和约束求解是主要的两大难题.在缓解路径空间爆炸方面,目前已有的工作 基本分为两个思路:(1) 在具体目标下提供高效的搜索策略,使符号执行分析更快地达到目标,包括提高程序的 覆盖率[105,109111]、判断某个程序点是否可达[112]、产生满足正规性质的程序路径[113]、探索程序不同版本的差 异部分[114,115]等;(2) 通过约束输入范围、削减或合并路径来减小程序的路径空间,包括基于输入模版[116,117]、程 序切片[118121]、程序抽象(包括摘要技术) [122129]、偏序约减[130,131]、条件合并[132,133]以及等价路径约减[121,134136] 等一些方法.在约束求解方面,已有的工作也可分为两个方面:(1) 在调用求解器之前对路径条件的查询进行优 化,以减少求解器的调用次数或缩短求解时间,包括查询缓存和重用[105,137139]、基于约束独立性的优化[103,105]、 增量式求解[105,140]等;(2) 支持复杂程序特征的高效编码,包括对机器数[104,105]、数组[100,105]、浮点[141145]、字符