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

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

条件语句(包括循环条件)和对数组下标的赋值表达式(包括声明赋值表达式和复合赋值表达式).其中,声明赋值
表达式中 idx 声明的数据类型如果是无符号类型,则公式(8)中的条件 F 成立,同时,条件 B 和条件 D 不成立.本文
提供了两种判断方法来检查公式(8)中条件 A~F 是否满足,即简单匹配方法和约束求解方法,将条件 A~F 统一用
c i →(idx op expr)来表示,以下描述中均先假设数组访问语句所在的基本块条件语句.
简单匹配处理方法.主要处理包含目标数组下标和常量的语句,即条件格式为(idx op const 1 )→(idx op
const 2 ),且当其中的两个操作符 op 一致时,通过比较两个常量 const 1 和 const 2 来判断条件的可满足性.针对不同
类型的语句,如表 1 的第 3 列所示,具体处理规则如下.
• 赋值语句.只能处理语句为 idx=const 和 idx=expr%const 的情形,其中,若 idx=const 中 const 大于 0,则公式
(8)中条件 F 成立,同时条件 B 和条件 D 不成立;同时,如果公式(8)中条件 E 中的数组长度 len 也为常量,且若语
句中的常量 const 小于或等于所有数组长度 len,则条件 E 成立,同时条件 A 和条件 C 不成立;如果语句中的常量
const 大于任一常量数组长度 len,则条件 A 成立,报告数组越界.当语句为 idx=expr%const 时,则只在公式(8)中条
件 E 中的数组长度 len 同时也为常量时,若常量 const 小于或等于所有数组长度 len,则条件 E 成立,同时条件 A
和条件 C 不成立.
• 复合赋值语句.只能处理语句为 idx%=const 的情形,判定方法与 idx=expr%const 相同.
• 条件语句.只能处理语句条件为 idx<const、idx<=const、idx>const 和 idx>=const 的情形.当条件为
idx<const 时,如果公式(8)中条件 E 中的数组长度 len 同时也为常量,且如果语句中的常量 const 小于或等于所有
数组长度 len,则条件 E 成立,同时条件 A 和条件 C 不成立.当条件为 idx<=const 时,判定 const 是否小于数组长
度 len.当条件为 idx>const 时,判定 const 是否大于–1;当条件为 idx>=const 时,判定 const 是否大于 0.
约束求解处理方法.直接将条件 c i →(idx op expr)作为约束,并将约束取反(即!(cond→idx<size)交给约束求
解器,通过约束求解来判断条件的可满足性.如果约束求解的结果为 UNSAT(不可满足),则表明原来的约束 c i →
(idx op expr)恒为真,也就是说当前的语句 S i 隐含了 idx op expr;如果约束求解的结果为 SAT(可满足),则表明原
来的约束 c i →(idx op expr)不可满足.针对不同类型的语句,具体处理规则如下.
• 赋值语句.如表 1 第 4 列所示,将赋值语句 idx=expr 和待检查的数组边界检查条件 idx〈len/idx〉=len/idx<0/
idx>=0,构成!(idx==expr→idx<len)等约束交给约束求解器进行求解.
• 复合赋值语句.如表 1 第 4 列所示,将复合赋值语句 idx op=expr 和待检查的数组边界检查条件 idx<len,
构成!(idx 1 ==idx 0 op expr→idx 1 <len)约束交给约束求解器进行求解.
• 条件语句.当遇到“if”语句、“for”语句或“while”语句时,将抽取出语句中的条件 expr 和待检查的数组边界
检查条件 idx<len,构成约束!(expr→idx<len)交给约束求解器进行求解.
循环越界检测.如果在“for”或“while”条件中找不到对相应数组边界的检查,那么我们将检查数组下标是否
是循环变量.如果“for”或“while”条件与模式 idx<var 相匹配,则在后续数据流分析过程中,公式(8)中的条件将用
var 替换 idx 以进行更新.也就是说将数组越界问题转换为循环越界问题继续检查.
当分析结束时,将报告数组越界警报.数组越界检查报告主要包括关于每个数组下标索引的以下信息:文
件、行号、函数及其所在的数组表达式,以及待添加的边界检查条件.这些信息比较详细,可以帮助程序员更加
方便、快速地定位和确认工具报告的数组越界警报,也可以作为修复推荐建议提供给程序员作为参考.
示例解析.如图 2 所示代码,对于数组访问语句 arr[2],数组下标 2 为非污染,数组长度{j,k}为污染的,根据判
定规则 1,确定为数组越界缺陷.对于数组访问语句 s.noisy[n]、s.arr[i]和 tmp[i],其数组下标 n 和 i 为污染的,将通
过后向数据流分析并根据判定规则 3 检测是否会导致数组越界.由于结构体中的数组 noisy 和 arr 以及数组 tmp
是无符号类型,因此数组下标一定不小于 0,只需要检测是否越出数组上界.如图 5 所示的 CFG,我们从包含数组
表达式的最底层基本块 Block2 开始执行数组越界检查,也就是从源码中的第 16 行代码开始进行分析.首先,将
遍历基本块 Block2,未发现对数组下标边界的检查.然后继续向上分析,得到 Block2 的前驱块 Block4.接下来,我
们得到 Block4 的后继(Block2 和 Block3),从而得到 Block4 中待检查的数组信息,即 OutState 为 16 行的 s.arr[i]
中 i<15、tmp[i]中 i<3.由于 Block2 在 Block4 的 false 分支上,所以 if 条件为!(i>=15).由此可以推出 i<15,因此,