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

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

数据流分析沿着正常的执行路径,从入口节点开始并在目标节点处结束.一个基本块的出口状态是该基本块中
的语句对该基本块的入口状态作用的结果,一个基本块的入口状态则是其所有前驱基本块的出口状态的组合.
与之相对地,后向数据流分析与控制流图中的有向边方向相反,从目标节点开始并在入口节点处结束.一个基本
块的入口状态是该基本块中的语句对该基本块的出口状态作用的结果,一个基本块的出口状态则是其所有后
继基本块的入口状态的组合.
1.4 指针分析
数组越界缺陷的根源实际上是由于指针对内存的越界访问引起的.数组名代表了一个指向数组首元素的
指针,通过数组下标访问数组元素(即 p[i]),实际上与指针从数组首元素移动到特定元素进行访问(即*(p+i))是等
价的.为了计算数组名实际指向的内存区域,就需要进行指针分析.
指针分析是一类特殊的数据流问题,是指通过程序分析方法计算指向相同内存区域的指针表达式的集合.
指针分析有几个重要的精度衡量属性,如流敏感性、上下文敏感性等.流敏感的指针分析会区分指针变量在不
同控制流位置的指向信息.上下文敏感性用来反映过程间分析在分析某个过程时,是否会区分不同调用点的上
下文对过程输入带来的不同,从而影响过程的输出.
1.5 SMT可满足性问题

可满足性模理论(satisfiability modulo theories,简称 SMT)求解器是用来判定一阶逻辑公式可满足性的程
序,是许多形式化方法的验证引擎.SMT 求解技术在有界模型检验、基于符号执行的程序分析、线性规划和调
度、测试用例生成以及电路设计和验证等领域有着非常广泛的应用 [13] .
Z3 [14,15] 是一个由微软研究院开发的高性能 SMT 求解器,是目前为止综合求解能力最强的 SMT 求解器.因
此,本文中引入 Z3 约束求解器以帮助 Carraybound 能够更精确地检测数组越界缺陷.
2 Carraybound:基于污点分析的数组越界缺陷的静态检测方法

2.1 方法框架
本文的数组越界缺陷的检查方法主要基于静态污点分析技术和数据流分析技术,这些方法主要基于程序
的抽象语法树、函数调用图和控制流程图进行分析.本文方法的框架如图 4 所示,首先根据程序的源码生成抽
象语法树(AST),再根据 AST 构建函数调用图(call graph)和控制流程图(CFG).然后,基于 CFG、AST 和函数调用
图,执行污点分析以确定可能被污染的数组下标.然后,定位所有包含这些被污染的数组下标的数组表达式的语
句,将数组下标符号化,通过边界分析得到每个数组下标的边界信息.接下来,执行后向数据流分析,并提供简单
匹配和约束求解两种方法,检测程序中是否存在相应的表达式保证了数组下标的边界条件.如果不存在这些表
达式,则报告数组越界缺陷警报.

Fig.4 The overall framework of our method
图 4 方法框架