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

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

的内存资源下扫描 10 万行甚至 100 万行代码的程序,我们在 Carraybound 中实现了内存优化策略.内存优化策
略的关键思想是使用一个 AST 队列仅在内存保留最新使用的 AST 文件,例如只保留 200 个 AST 文件.AST 文
件越少,内存消耗就越少.并且,AST 队列的最大容量可以由用户配置.用户可以根据需求和计算机容量配置
AST 队列的最大容量.在分析 AST 的内容时,Carraybound 将首先检查相应的 AST 是否在内存中.如果 AST 在
内存中,Carraybound 会将 AST 移动到队列的末尾.如果 AST 不在内存中,Carraybound 将从 AST 文件读入 AST
的内容.当 AST 队列达到其最大容量时,Carraybound 将删除最先读入的 AST.值得注意的是,如果用户设置了一
个较小的最大 AST 数,Carraybound 将会更加频繁地读取 AST 文件.因此,如果有足够的内存,用户应选择更大的
最大 AST 数,以减少频繁的读操作并提高 Carraybound 的效率.
求解优化.约束求解是非常耗时的,尤其是频繁地调用约束求解器将严重增加分析时间,制约工具的可扩展
性.而在我们的方法中,由于需要计算不动点,会增加对相同约束求解的需求.因此,我们针对 Carraybound 分析方
法的特征,在使用时进行了特殊优化.
• 结果缓存.为了减少对约束求解器的调用,将保存函数内语句是否隐含数组边界检查的结果列表,首先查
询这个列表,若未查询到结果,再调用约束求解器,这样可以大大减少对约束求解器的调用次数.
• 快速求解.由于在通过数据流分析判断所遇到的表达式是否隐含数组边界检查时,总是将!(cond→
idx<size)这样的约束条件交给约束求解器进行求解,并且这个约束条件满足 cond 中必须包含 idx 这个对象才能
使得约束条件 UNSAT.因此,为了辅助约束求解器更快求解,我们通过映射表的比对提前完成约束的快速求解,
过滤不满足 cond 中必须包含 idx 这个对象的约束条件,可以有效地减少对约束求解器的调用次数.
• 时间限制.程序中可能存在一些按位操作及一些其他操作语句,对应到 Z3 约束求解时可能比较耗时.因
此,我们为 Z3 提供了 timeout 的配置项.
3.2 实验评估
我们对 Carraybound 的实验评估主要试图回答以下几个问题.
Q1:Carraybound 的有效性?
Q2:Carraybound 的效率?
Q3:Carraybound 与已有方法/工具的比较?
Q4:Carraybound 发现真实缺陷(CVE)的能力如何?
实验对象和工具.为了评估 Carraybound 的有效性,我们选用了几个常用的开源项目作为实验对象,见表 2.
由于在相关工作的文献中未发现可用的工具,因此我们与如下几个知名的可以检查数组越界缺陷的静态分析
工具进行了比较,包含开源静态分析工具 Cppcheck [18] 、商业静态分析工具 Checkmarx [19] 和 HP Fortify [20] .
Cppcheck 是针对 C/C++语言的开源静态分析工具,该工具主要检查未定义行为相关的程序缺陷,包括除零错、
整型溢出和越界访问等安全问题 [18] .Checkmarx 是一个基于源码的静态分析工具,对于被测程序,该工具会首先
根据代码的元素和流程信息构造逻辑图,然后通过在该图上进行查询以发现程序中可疑的安全漏洞和业务逻
辑问题.HP Fortify 是一个基于规则的源码级静态分析工具,支持对 25 种编程语言的漏洞分析.对这些工具的警
报数目进行了统计,结果见表 2,其中,CAB-Simple 为赋值语句简单匹配处理方法,CAB-Z3 为约束求解处理方法.
程序的规模最大可以达到 200+万行.我们通过人工审查程序源码,对表 2 中 Carraybound 报告的数组越界检查
警报进行了人工确认,确认过程默认为两层函数调用.由于其他几个静态分析工具内存消耗不易统计,我们仅统
计了其时间开销,并在表 2 的基础上增加两个大规模程序,见表 3.由于我们不知道表 2 中的程序包含多少个真
正的数组越界缺陷,通过人工确认的方式也无法完全确认所有警报,因此,为了解答问题 4,我们在 CVE 中阅读了
与缓冲区溢出漏洞相关的报告,找到其中几个由于数组越界缺陷导致的缓冲区溢出的程序以及其修复后的版
本,见表 4.