Page 23 - 《软件学报》2020年第10期

高凤娟 等:基于污点分析的数组越界缺陷的静态检测方法 2999

算的表达式,将会导致判定准则中的约束更为复杂,从而无法在指定时间内求解,进而导致误报.

4 相关工作
4.1 污点分析

动态污点分析是一种当前流行的软件分析方法.当前有很多工作通过进行动态污点分析来追踪软件中的
隐藏漏洞 [10,21−23] .污点分析将可能包含恶意数据的外部输入作为污点源,比如网络数据包;然后,跟踪这些污点
数据如何在整个程序执行过程中传播;当敏感数据(如堆栈中的返回地址或用户特权设置)被污点数据污染时执
行相应的处理操作.
与动态污点分析相比,静态污点分析以静态方式追踪源码或二进制文件中的污点信息.STILL [24] 是一个基
于静态污染和初始化分析的防御机制,可以在各种互联网服务中(例如 Web 服务),检测嵌入在数据流中的恶意
[9]
代码.为了减少污点分析的开销,TaintPipe 借助轻量级的运行时日志记录来生成紧凑的控制流信息,并产生多
个线程,以流水线的方式并行地执行符号化污点分析.静态污点分析面对的另一个问题是耗费人力.大多数现有
的静态污点分析工具会在潜在的易受攻击的程序位置报错.这会导致需要开发者人工确认报告,为此需要耗费
大量的人工成本.Ceara 等人 [25] 提出了一种污点依赖序列算子,主要基于细粒度的数据流和控制流污点分析,为
程序员提供需要被分析的路径的一些相关信息.

4.2 指针分析
Andersen 算法 [26] 和 Steensgaard 算法 [27] 是最具代表性的流不敏感的指针分析算法.Andersen 指针分析方
法 [26] 是一种基于包含的经典的 C 语言指针指向分析算法,该算法被认为是最精确的流不敏感、上下文不敏感
的指针指向分析算法.该算法将程序中的直接指向关系描述为变量与对象之间的约束关系集合,再通过求解约
束关系集合的传递闭包,计算得到间接的指向关系,从而获得所有变量的、完整的指向关系集合.这种基于包含
的思想被广泛应用在后续的指针指向分析工作中 [28] .Steensgaard 算法 [27] 是一种基于等价的指针分析算法,其复
杂度接近于线性复杂度.但是流不敏感的指针分析将会影响后续静态分析的精度.目前也有一些流敏感的指针
分析算法,这些方法通常是基于数据流分析 [29] ,比如 Emami 算法 [30] 、Lam 算法 [31] 、Chase 算法 [32] 等.本文的流敏
感、上下文敏感指针分析是按需分析,即只针对所关心的数组名进行指针分析.

4.3 数组越界检查
Xu 等人 [33] 提出了一种可以直接在不受信任的机器码上进行分析的方法,该方法依赖于这些程序的初始输
入的类型状态信息和线性约束.Detlefs 等人 [34] 提出了一种针对常见程序错误的静态检查器,包括数组下标越
界、空指针解引用和多线程程序中的并发类错误.该方法利用线性约束,自动合成循环不变量用于边界检查.
Leroy 和 Rouaix [35] 提出了一个理论模型,系统地把基于类型的运行时检查放入主机代码的接口程序中.Kellogg
等人 [36] 提出了一种在编译时检测数组越界的轻量级验证方法,但是为了达到线性验证时间,该方法需要开发者
预先注释相关信息,例如程序边界信息.相比之下,我们的方法能够分析出程序边界.ABCD [37] 用于按需消除无用
的数组边界检查.它平均能够删除 45%的动态边界检查指令,有时可以实现接近理想化的优化.
[8]
当前也存在许多静态的数组越界检测工具 [38−40] .Chimdyalwar 对 5 种用于检查数组越界的静态分析工具
进行了评估.其中,商业工具包括 Polyspace 和 Coverity;学术工具为 ARCHER,其他两个是开源工具 UNO 和
CBMC.Polyspace 是唯一无漏报的工具,但是由于它是内存密集型分析,不能以同样的高精度扩展到大规模程序
上.相比之下,Coverity 可以支持百万行级别的代码分析,但存在大量误报.UNO 同时有误报和漏报,并且不能应
用在大规模程序上.ARCHER 宣称可以运行在百万行级别的代码上,但是分析并不完善.CBMC 模型检查器进行
了精确的分析,无法在大规模程序上达到相同精度.Nguyen 等人 [39] 提出了针对 Fortran 语言的数组越界静态检
查方法.Arnaud 等人 [38] 提出了针对嵌入式程序中数组越界检查的静态分析方法,该方法处理的程序规模为 20+
万行,我们的方法可以处理百万行程序.由于该文献提供的工具 CGS 是根据 NASA 程序定制的闭源工具,并且使
用了 NASA 闭源程序作为被测对象,因此,我们在实验中没有与该方法进行比较.