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

2998 Journal of Software 软件学报 Vol.31, No.10, October 2020

Q3 与已有方法的比较.如表 2 和表 3 所示,有些工具无法指定只检测数组越界缺陷,会有更高的时间开销,
我们不与其进行效率比较,这里列出来仅供参考.
• Cppcheck:如图 3 所示的示例,Cppcheck 未报告任何数组越界相关的警报.而经过实验,类似于“char a[5];
a[5]=0;”这样简单的数组越界,该工具是可以报告的.这表明,该工具可能存在一些漏报.同时,针对表 2 所列的被
测程序,该工具均未报告数组越界警报.如表 3 所示,该工具由于不能指定单独检查越界问题,会消耗较长的时间
进行检查其所支持的缺陷类型.
• Checkmarx:如图 3 所示的示例,Checkmarx 未报告任何数组越界相关的警报.表 2 中所列的被测程序一共
报告了 617 个数组越界相关的警报,其中高风险警报 25 个,经人工确认有 1 个为可疑的数组越界缺陷,其余为低
风险警报,经人工确认有 4 个为可疑的数组越界缺陷.在人工确认其报告时,发现该工具无法处理和循环相关的
数组下标访问问题,即使数组下标为循环变量,当循环上界为数组上界时,仍然会误报数组越界.如表 3 所示,该
工具在只选定几个与数组越界相关的缺陷类型进行检测时,仍会消耗较长的时间.我们使用时发现,该工具会消
耗很长的时间对源码进行解析以生成该工具的一种中间表示,比如逻辑图,然后再在该图上进行查询以检查缺
陷.虽然我们只指定了数组越界相关的缺陷类型,但是该构建逻辑图的过程是针对所有类型的缺陷的,因此会消
耗较长时间.
• HP Fortify:如图 3 所示的示例,Fortify 只报告 test.c 中第 11 行 p.noisy[n]为缓冲区溢出警报点,而该警报实
际为误报;并且漏报了 test.c 中第 15 行 arr[i]会因为第 12 行的循环导致数组越界/缓冲区溢出.表 3 所示的被测
程序,该工具报告了大量缓冲区溢出警报,我们人工筛选出其中与数组越界相关的警报,经过人工确认发现多数
为误报,并且多数情况下,无法处理和循环相关的数组下标访问问题.
Q4 对已知 CVE 缺陷的报告比较.见表 4,Carraybound 可以对缺陷版本的程序报告相应的数组越界警报,而
对修复后的版本的程序将不再报告数组越界警报.Cppcheck 和 Checkmarx 对修复前后的版本均未报告相应的
数组越界警报.而 HP Fortify 对 Sendmail 程序的修复前后的版本的报告是正确的,对 file 程序的前后版本均未报
告,对 openjpeg 程序未检查出该缺陷已被修复.
3.3 实验讨论

上述实验结果表明,这些已有的开源和商业静态分析工具均不是专门针对数组越界检查的工具,它们的存
在可以帮助程序员发现程序中的各种类型的缺陷.但是这些工具未进行精确的数据流分析和约束求解,因此对
于数组越界这一类型的缺陷存在大量误报和漏报.
我们的工具采用数组长度区间分析、按需污点分析、精确的数据流分析和约束求解,所以有相对更少的误
报和漏报.但在人工确认这些静态分析工具报告的警报时,我们也发现了本文工具 Carraybound 在实现上的一些
不足,主要包括可扩展性和准确性两方面的不足.
可扩展性.由于约束求解比较耗时,尤其是求解一些复杂约束,比如一些按位运算时,约束求解器将无法在
较短的时间内给出求解结果.这将会限制我们工具的可扩展性.在实验时只能通过设置 timeout 时间来跳过一些
复杂的约束求解,但是这样做又可能会导致该工具的误报和漏报.
准确性.影响本文工具 Carraybound 准确性的问题主要包括:
(1) 类型转换:C 语言程序中经常存在类型转换,我们目前的工具实现中未能很好地处理该问题,因此可能
会导致工具的误报和漏报.
(2) 复杂循环越界:有些情形下很难分析出数组下标和循环上界的关系,这会导致工具的误报和漏报.
(3) 库函数:由于采用静态分析方法,在不能获得库函数的源码实现的情况下,我们将无法判断这些库函数
的功能和作用,但是可能这些库函数实现了对数组边界的检查和保证,因此会导致我们的工具产生误报.
(4) 复杂数组下标:程序中存在一些使用复杂表达式作为数组下标的情形,会导致工具产生误报.尤其是对
于简单匹配方法,容易因为无法匹配越界检查条件,产生误报.比如数组下标 2×i+j,而程序中可能是分别对 i 和 j
的范围约束,无法直接匹配到如 2×i+j<xx 的检查语句,这样就会导致误报.目前的工具出于可扩展性考虑,对约束
求解设置了 timeout 时间,因此复杂数组下标也会导致约束求解方法的误报和漏报.比如数组下标为包含按位运