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

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

找到了 16 行的 s.arr[i]应满足 i<15 的边界检查,第 16 行的 s.arr[i]将从待检查数组集合中移除.也就是说,Block4
的 InState 是 16 行的 tmp[i]中的,i<3.然后继续向上分析 Block5,在 Block5 中遇到 for 语句时,16 行的 tmp[i]中的
i 恰好为循环变量,转换为循环越界问题处理,即在循环上方检测循环上界 n 是否会超出数组 tmp 的长度,即检测
n<4.Block6 中的待检测数组信息 OutState 为 16 行的 tmp[i]中的 n<4,11 行的 s.noisy[n]中的 n<12.当遇到 Block6
中的赋值语句时,待检测数组信息将更新为 16 行的 tmp[i]中 m<4,11 行的 s.noisy[n]中的 m<12.因此,当遇到函数
f 的入口时,待检测数组信息不为空.如果配置的检测深度为 1,那么将报告数组越界警告.否则,将执行过程间的
后向数据流分析.
在函数 main 中,根据实参更新待检测数组信息为 16 行的 tmp[i]中的 argc<5,11 行的 s.noisy[n]中的 argc<13.
if 语句的条件为 argc+2<15,使用简单匹配方法,则 11 行的 p.noisy[n]的数组边界检查条件 n<12 可以被满足,因
此,简单匹配方法中的警报“test.c,line 11,p.noisy[n],n<12”为误报.但是 12 行的循环上界 n 应小于 11 才可以保证
15 行的 arr[i]中的 i<10,因此,简单匹配方法和约束求解方法中的警报“test.c,line 12,arr[i],n<11”为真警报.
因此,当使用简单匹配方法进行判断时,无法匹配可以处理的模式,将会报告:
test.c,line 11,s.noisy[n],n<12;
test.c,line 16,tmp[i],i<3;
当使用约束求解方法进行判断时,可得!((argc+2<15)→(argc<13))≡UNSAT,!((argc+2<15)→(argc<5))≡
SAT,因此将会报告:
test.c,line 16,tmp[i],i<3;

3 实现和实验评估

本文扩展了我们的前期工作 [16,17] ,实现了一个面向数组越界缺陷检测的全自动跨平台的静态分析工具
Carraybound,优化了按需污点分析,并增加了按需指针分析,从而以此来分析数组长度的区间,引入了定理证明
器 Z3 [15] ,在数组越界检测过程中用以解决约束求解问题,工具的架构如图 6 所示.该工具可以在 Linux 和
Windows 系统上运行,底层依赖于 Clang 3.6 和约束求解器 Z3,由数组长度区间分析、按需污点分析和数组越界
缺陷检测共 3 个模块组成.提供了可配置的功能实现用户按需调节检测精度,用户可以配置函数层数来控制执
行过程间数据流分析的深度,并通过内存优化、求解优化等措施提升了工具的效率.

Fig.6 Architecture of Carraybound
图 6 Carraybound 工具架构
3.1 实现优化
内存优化.大规模程序总是包含大量 AST 文件.如果一次性读入所有 AST 文件,包含 AST 文件的所有内容,
将会消耗大量内存.这将会严重制约 Carraybound 对大规模程序的支持.比如,PHP-5.6.16 包含 25 万行源代码和
211 个 AST 文件,当我们尝试一次性读入所有 AST 文件时,在 2GB 内存的机器上将无法运行.为了支持在有限