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

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

句不会导致数组越界.
判定规则 1.对于数组访问语句 arr[idx],如果数组下标 idx 为非污染的,数组长度列表中任意一个长度为污
染的,则该数组访问语句会导致数组越界.
)
⎧ ⎪ T (idx ≡ untainted
⎨ ⇒ Warr [ ( ]idx ≡ ) T 6
,T s ≡
⎪ ⎩ i ∃∈ ⎡ ⎣ 0,n ] () tainted
i
判定规则 2.对于数组访问语句 arr[idx],如果数组下标 idx 为非污染的,数组长度列表中每一个长度都为非
污染的,则如果数组下标小于数组长度列表中的每一个长度,则该数组访问语句不会导致数组越界;否则,该数
组访问语句会导致数组越界.
⎧ ⎪ T (idx ≡ untainted ⎧ , Ti ∃∈ ⎡ ⎣ 0,n ],idx≥ s i
)
⎪
⎨ i ∀∈ ⎡ 0,n ] () untainted≡ ⇒ Warr [ ( ]idx ≡ ) ⎨ (7)
,T s
⎩
⎪ ⎩ ⎣ i ⎪ , F ∀ ∈ i ⎡ ⎣ 0,n ],idx < s i
判定规则 3.对于数组访问语句 arr[idx],如果数组下标 idx 为污染的,假设程序中有 n 条与数组下标 idx 相关
的语句,构成语句序列为 S 1 ,S 2 ,…,S n ,将每一条语句转换为约束表达式,则约束表达式序列为 c 1 ,c 2 ,…,c n ,设第 i 条
语句 S i 在函数 f 的基本块 bb 中,此时数组 arr 对应的数组下标为 idx i ,数组长度列表为 LenSet i ={len 1 i ,len i 2 ,...,len i m }.
如果存在一条语句 S i ,可以推导出 idx 大于等于 LenSet i 中任一长度(公式(8)中的条件 A);或者如果存在一条语句
S i ,可以推导出 idx 小于 0(公式(8)中的条件 B);或者对所有语句都不能推导出 idx 小于 LenSet i 中所有长度(公式
(8)中的条件 C)或者大于等于 0(公式(8)中的条件 D),则该数组访问语句会导致数组越界.如果存在一条语句 S i ,
可以推导出 idx 小于 LenSet i 中所有长度(公式(8)中的条件 E),并且存在一条语句 S j ,可以推导出 idx 大于 0(公式
(8)中的条件 F),则该数组访问语句不会导致数组越界.
(
≡
A : ∃∃ i ( ( ,! c → len i k )idx≥ ) UNSAT ) ⎫ ⎪
, i k
B ( i ( ( 0 ≡ )idx < ) ,! i c → UNSAT ) : ∃ ⎪ ⎪
(
, i
C : ∀∀ k i ( ( < k i ) idx len ) ,! c → ≡ SAT ) ⎪ ⎪ ⎪
D ( i ( ( 0 ≡ )idx≥ ) ,! i c → SAT ) : ∀ ⎪ ⎬ (8)
( ( ( i ) ⎪
E : ∃∀ k i len k ) idx < ) ,! c → ≡ UNSAT ⎪ ⎪
, i
F ( c → j ( ( 0 ≡ )idx≥ ) ,! j ∃ UNSAT ) : ⎪ ⎪

( T )idx ≡ tainted ⇒ W [ ( ]idx = )arr ⎧ ⎨ , TA ∨ B ∨ C ∨ D⎪ ⎪
⎩ , FE ∧ F ⎭
依据以上 3 个判定规则,本文将参照算法 1 对程序进行数组越界检测.对于每一条数组访问语句,首先查询
数组下标的污点值.如果数组下标为非污染的,则根据判定规则 1 和规则 2 检测该数组访问语句是否会导致数
组越界.如果数组下标为污染的,则通过高精度的后向数据流分析,检测该数组下标是否可能导致数组越界.后
向数据流分析时,使用 OutState 表示一个基本块在该基本块出口时的状态,是其所有后继基本块的 InState 的并
集,如公式(4)所示(见第 3.2 节),此处代表在该基本块待检查是否会导致数组越界的数组访问语句信息的集合;
InState 表示一个基本块在该基本块入口时的状态,如公式(5)所示(见第 3.2 节),此处是在其 OutState 的基础上,
该基本块的语句根据判定规则 3 和表 1 对待检查是否会导致数组越界的数组访问语句信息的集合进行杀死和
生成的结果.过程内后向数据流分析从数组访问语句所在的基本块开始,向上遍历函数中的每个基本块,到函数
的入口点结束.当分析完一个基本块 bb 后向上分析其前驱基本块 pred 时,将同时根据 bb 位于 pred 的哪个分支,
以决定在使用分支语句的条件时是否需要取反.如果在到达入口点时待检查语句集合为空,则将终止后向数据
流分析,否则将继续进行过程间的后向数据流分析.首先,需要根据程序的函数调用图获取函数 f 的所有父函数.
对于每个父函数,遍历其 CFG 并找到调用数组函数 f 的调用语句.对于每个数组边界条件,如果其下标索引与函
数 f 的形参之一相同,则将获取相应的实参来构造新的数组边界条件,见算法 interABChecker 第 7 行.然后在父