随着移动计算、物联网、云计算、人工智能、开源软件、RISC-V开源指令集等领域的飞速发展, 相关的软/硬件都迎来了新的发展机遇和挑战.为了适应软/硬件的发展, 当前也涌现出了很多新的编程语言和编译器.但是, C语言作为高效率、面向过程、抽象化的通用程序设计语言, 仍然广泛应用于系统软件的开发.系统软件中如果存在漏洞, 就可能会被恶意利用, 将会严重影响人们的生产生活, 甚至威胁到生命财产安全.软件安全已成为软件企业不能回避的挑战.

C语言被广泛应用于底层软件生态系统的开发, 这是因为C语言程序具有更高的运行效率.其中, 数组是C语言最重要的数据结构之一.当一个数组在程序中被使用时, 访问该数组的下标索引必须在一定范围之内, 即不小于0并且小于数组的大小, 否则会造成数组下标越界.数组越界的缺陷在很多编译后的系统中都存在, 而且通过实验, 我们发现, 像gcc、clang这样主流的C语言编译器, 在编译过程中不会对数组下标取值范围的合法性加以严格检查.数组越界有两种模式, 读越界和写越界.读越界会导致读取到随机的值, 继而使用该值会导致未定义行为.相比之下, 写越界会造成更加严重的后果, 不仅会造成未定义行为, 甚至会导致控制流截取, 使得攻击者可执行任意恶意代码^{[1, 2]}.如图 1所示, 根据CVE历史统计可以发现, 占据前三的漏洞类型为拒绝服务、代码执行和溢出^[3].而数组越界缺陷常常会导致拒绝服务、代码执行和溢出.比如Adobe阅读器2017之前版本中存在的远程代码执行和拒绝服务漏洞就是由于外部输入作为数组下标从而可能导致写越界引起的(CVE-2017- 16391、CVE-2017-16410).同时, 研究表明^[4-6], 31%的缓冲区溢出是由数组越界造成的.因此, 可见数组越界缺陷仍然是严重威胁系统软件安全的重要缺陷类型.本文主要针对在给定C程序源码时, 检测数组下标越界和由循环导致的数组下标越界问题.为了提高系统软件的安全性, 程序必须对由外部输入控制的数组下标进行边界检查.但是, 开发者可能会遗漏边界检查或者没有进行正确的边界检查, 使得程序处于可被攻击利用的不利状态.

目前已有一些研究工作提出使用静态分析方法和动态测试方法来进行数组越界检查.由于动态方法总是依赖于测试用例的完整性, 从而导致这些方法无法达到足够高的程序覆盖率.静态分析方法通过扫描分析程序源代码以检查程序中的缺陷.当前的静态分析方法出于效率的考虑, 未对程序进行高精度的分析, 未处理循环导致的数组越界, 并且多是基于规则的匹配方法, 无法处理复杂约束、复杂表达式等情况, 导致一些已有的数组越界静态检测方法从而存在大量的误报和漏报现象.

因此, 为了进行高精度的、高效的静态分析来检测数组越界缺陷, 一方面, 我们提出使用按需污点分析计算数组下标和数组长度的污点值, 当数组长度污染时, 即使在数组下标非污染的情况下仍然可能导致数组越界(比如图 2第11行所示的数组访问语句), 而在数组下标污染时, 则需要进行高精度的数据流分析以检测是否会导致数组越界; 另一方面, 我们提出在静态分析的过程中使用优化后的约束求解器来处理程序中与数组访问相关的复杂约束和复杂表达式, 从而有效地提高检测方法的准确性.对于数组下标越界问题, 我们关注从程序入口到数组访问语句之间, 数组下标越界条件的可满足性, 通过将约束求解引入到数据流分析过程中, 能够更加精确地检查数组越界问题.

在本文中, 我们提出了一个静态分析框架Carraybound, 该框架基于静态的污点分析、数据流分析以及约束求解检查程序中是否存在潜在的数组越界缺陷.除此之外, Carraybound还提供待增加的数组边界检查条件, 可以帮助程序员更加方便、快速地定位、确认和修复我们报告的数组越界警报.实验结果表明Carraybound可以快速、有效地报告出程序中的数组越界缺陷, 并通过与已有静态分析工具Cppcheck、Checkmarx和HP Fortify进行对比, 展示了Carraybound在发现数组越界缺陷上的优越性.

本文的主要贡献包括:

●提出流敏感、上下文敏感的按需指针分析方法, 实现数组长度区间分析; 提出按需污点分析方法, 实现数组下标和数组长度污染情况的计算.

●提出基于污点分析的数组越界缺陷的检测方法, 定义了数组越界缺陷判定规则, 然后依据判定规则, 使用后向数据流分析检测数组越界, 并将约束求解引入到数据流分析过程中以检查数组越界缺陷, 同时通过优化尽量减少对约束求解器的调用, 以提高分析效率.

●实现了一个静态分析工具Carraybound, 检测C程序中的数组越界缺陷(包括由循环导致的数组越界缺陷), 并通过实验展示了工具的有效性.

本文第1节介绍我们工作的背景知识.第2节介绍所提出的基于污点分析的数组越界的静态检测方法.第3节介绍实现工具Carraybound, 并通过实验展示该工具的有效性和效率, 同时讨论该工具的不足之处.第4节介绍相关工作.第5节进行总结, 并提出未来工作展望.

1 背景知识 1.1 数组越界

数组是在内存中连续存储的具有相同类型的一组数据的集合.C语言中数组分为静态数组和动态数组.静态数组在内存中位于栈区, 其长度为常量, 是定义时就在栈上分配了固定大小, 运行时, 这个大小不能改变, 例如char a^[7].对静态数组的写越界访问将会导致栈上的缓冲区溢出.动态数组在内存中位于堆区, 其长度可以是变量, 亦即可以在程序运行时在堆上动态分配大小, 例如int *a=(int*)malloc(sizeof (int)*10).对动态数组的写越界访问将会导致堆上的缓冲区溢出.

当一个数组在程序中被使用时, 访问该数组的下标索引必须在一定范围之内, 即不小于0并且小于数组的大小, 否则会造成数组下标越界^[8].如图 2中第11行所示的数组, 由于数组arr的长度m来自于外部输入, 因此常量数组下标也可能会导致数组越界访问.

如图 3所示, 我们将C语言程序中的越界访问问题归结为以下两类.

① 数组下标越界:包括读越界和写越界.例如char c=a[5]是读越界而a[5]=0属于数组的写越界.其中, 数组下标访问写越界会导致缓冲区溢出, 即图 3所示的交集部分.数组下标越界还包括循环导致的数组下标越界, 比如char a[5]; for (int i=0;i < 6;i++) {a[i]=0;}.

② 缓冲区溢出:包括API调用和数组下标访问写越界导致的缓冲区溢出.比如strcpy(dest, src)和a[5]=0.

本文方法目前侧重于数组下标越界(包含循环导致的数组下标越界)问题.对于由API调用导致的缓冲区溢出问题, 我们的另一项缓冲区溢出静态警报确认的工作重点关注了该类问题^[5].

通常情况下, 程序员可以通过特定的方式限制数组下标的范围, 以避免数组越界的发生.常见的3种方式如下所示.

① idx=idx % size;

② if (idx > =size||idx < 0)…

③ assert (idx > =0 & & idx < size);

程序中也可能存在一些复杂的约束和表达式实现了对数组下标的范围限制, 比如按位操作、包含多个运算符的线性运算, 甚至是非线性约束.这些情况会加大分析难度, 导致传统方法无法精准地检查出程序中的数组越界缺陷.

1.2 污点分析

污点分析是检测程序漏洞的常用技术^{[7, 9, 10]}.如果攻击者向程序输入一些恶意数据, 而程序没有进行恰当的防护, 则可能会导致系统处于不安全的状态.这些受外部输入影响的数据在污染分析中标记为污染.外部输入包括用户或文件的输入、主函数的参数.污点分析尝试识别程序中那些会被用户输入污染的变量, 并最终追溯到可能会导致程序缺陷的语句.如果在该语句之前, 未经检查就直接使用被污染的数据, 则视为一个程序缺陷.污点分析分为静态污点分析和动态污点分析.其中, 动态污点分析需要执行程序, 无法保证对源码的覆盖率.静态污点分析主要依赖于程序抽象语法树和控制流图进行数据流分析, 不需要实际执行程序.因此静态污点分析可以实现比动态污点分析更高的源代码覆盖率.但静态污点分析可能因缺乏运行时信息而产生误报和漏报.

1.3 数据流分析

数据流分析通常用于静态代码分析, 是一种基于控制流图来收集数据流信息的技术.对程序进行数据流分析的一种简单方法是为控制流图的每个节点建立数据流方程, 并通过在每个节点上重复计算输入的输出来反复迭代, 直到整个系统到达不动点^{[11, 12]}.前向数据流分析和后向数据流分析是数据流分析的两种不同方法.前向数据流分析沿着正常的执行路径, 从入口节点开始并在目标节点处结束.一个基本块的出口状态是该基本块中的语句对该基本块的入口状态作用的结果, 一个基本块的入口状态则是其所有前驱基本块的出口状态的组合.与之相对地, 后向数据流分析与控制流图中的有向边方向相反, 从目标节点开始并在入口节点处结束.一个基本块的入口状态是该基本块中的语句对该基本块的出口状态作用的结果, 一个基本块的出口状态则是其所有后继基本块的入口状态的组合.

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和函数调用图, 执行污点分析以确定可能被污染的数组下标.然后, 定位所有包含这些被污染的数组下标的数组表达式的语句, 将数组下标符号化, 通过边界分析得到每个数组下标的边界信息.接下来, 执行后向数据流分析, 并提供简单匹配和约束求解两种方法, 检测程序中是否存在相应的表达式保证了数组下标的边界条件.如果不存在这些表达式, 则报告数组越界缺陷警报.

2.2 数组长度区间分析

首先, 定位数组下标访问语句, 然后, 通过后向数据流分析得到所关注数组名的别名, 进而定位到数组声明语句, 每一个数组声明语句对应一个相应的数组长度.由于一个数组可能对应多个数组声明语句, 因此, 这一过程将分析得到数组的长度区间, 具体步骤如下.

数组长度区间分析.对于数组访问语句arr[idx], 在AST上判断是否存有数组声明大小, 如果无法直接获取数组声明大小, 则进行指针分析, 得到arr实际是某个或者某几个静态数组或动态数组的别名.

本文设计了一种流敏感、上下文敏感的按需指针分析.按需是指本文只对所关注的数组名(即通过被污染数组下标访问数组元素的语句中的数组名)进行指针分析, 目的是计算出数组名实际对应的静态数组或动态数组表达式.对于每个函数f, 首先, 统计每个基本块block中包含被污染的数组下标的数组表达式, 然后从最底层包含关注数组表达式的位置开始, 向上进行一个后向数据流分析, 后向数据流分析中, 使用OutState表示一个基本块在该基本块出口时的状态, 是其所有后继基本块的InState的并集, 如公式(1)所示, 此处代表在该基本块每个所关注的数组名对应的待分析的指针集合; InState表示一个基本块在该基本块入口时的状态, 如公式(2)所示, 此处是在其OutState的基础上, 该基本块的赋值语句根据下文的指针处理规则对每个所关注的数组名对应的待分析的指针集合进行杀死(kill)和生成(gen)的结果.

$ OutState\left( {block} \right) = { \cup _s}_{ \in succ\left( {block} \right)}InState\left( s \right) $

(1)

$ InState\left( {block} \right) = Gen\left( {block} \right) \cup \left( {OutState\left( {block} \right)-Kill\left( {block} \right)} \right) $

(2)

指针分析时, InState和OutState维护的是在某一个基本块中每个所关注的数组名arr对应的待分析的指针集合AliasSet={p₁, p₂, …, p_n}.初始时, AliasSet={arr}.对于AliasSet中每一个指针p, 首先查询AST是否可以直接获取静态数组声明的大小, 如果可以, 则将AliasSet中该元素p标记为终止点, 停止对p进行指针分析; 否则, 继续对p进行指针分析, 针对以下赋值语句, 后向数组流分析的具体指针处理规则为:

●  p=malloc(size)将AliasSet中的p替换为malloc(size), 并将AliasSet中该元素malloc(size)标记为终止点, 停止对malloc(size)进行指针分析.

●  p= & a将AliasSet中的p替换为 & a.

●  p=q将AliasSet中的p替换为q, 后续数据流分析继续分析q的别名.

●  p=*q将AliasSet中的p替换为*q.

●  *p=q将AliasSet中的p替换为 & q.

●  p=g(…)将进入函数g中, 从函数返回语句开始进行指针分析.

如果AliasSet中的元素包含 & 符号, 形如 & p, 则在后续数据流分析中分析对p的赋值表达式, 如果替换的新指针为q, 则AliasSet中替换 & p为 & q, 如果新指针为*q, 则AliasSet中 & p替换为 & (*q), 即替换为q, 以此类推.规则中将AliasSet中的p替换为q, 对应着对AliasSet中杀死(Kill)p和生成(Gen)q.

如果在函数f中没有定位到数组名对应的数组声明语句, 则用相同方法分析该函数的所有调用者.以此类推, 直到定位到数组声明语句.由于不同的上下文、不同的分支将导致一个数组名可能存在多个数组声明语句作为别名, 其中, 每一个数组声明语句将对应一个数组长度, 因此, 对于一个数组名arr, 通过指针分析将得到它的一组数组长度{s₀, s₁, …, s_n}.为了支持流敏感和上下文敏感, 将在数据流分析过程中额外记录:(1)每个基本块block的后继节点集合(计算方法参照公式(1)), 记为succs(block); (2)在分析函数f时, 过程间后向数据流分析的函数调用链, 记为succs(f).对于数组名arr, 当在指针分析时, 在函数f的基本块bb中定位到一个arr的数组声明语句作为别名时(即AliasSet中的终止点之一记为p₀), 设p₀对应的数组长度为s₀, 则将记录s₀对应的有效函数和基本块信息, 有效函数信息为过程间后向数据流分析的函数调用链, 即ValidFuncs(s₀)=succs(f), 有效基本块信息为所在基本块的后继节点集合, 即ValidBBs(s₀)=succs(bb).最终, 每个数组名arr, 记录一组数组长度{s₀, s₁, …, s_n}, 且其中每一个数组长度s_i记录该值的作用域, 即有效函数ValidFuncs(s₀)=succs(f)和有效基本块ValidBBs(s₀)= succs(bb), 并由此推导出每个函数f的每个基本块bb中数组名arr对应的数组长度的集合size(arr, f, bb)={s_i, s_j, …, s_k}.

基于每个函数f的基本块bb中数组名arr的数组长度的集合size(arr, f, bb)={s_i, s_j, …, s_k}, 取其中的最大值记为数组长度的上界up, 取其中的最小值记为数组长度的下界low, 则数组长度的区间为[low, up], 如果数组长度为外部输入的变量, 无法确定上下界, 则保留长度集合.

示例解析.如图 2代码示例, 遍历可知, 在函数f中, 共有4个数组表达式的使用位置, 即11行的s.noisy[n]、12行的arr[2]和16行的s.arr[i]以及tmp[i].s.noisy[n]和s.arr[i]均为结构体成员数组, 可以直接定位其数组声明位置为第3行、第4行, 继而可知数组长度分别为12和15.tmp[i]的数组声明位置为第9行, 数组长度为3.arr[2]来自于函数参数, 通过指针分析可知, 动态数组p和q为arr的别名, 因此arr数组长度集合为{j, k}.

2.3 按需污点分析

按需污点分析是指本文中的污点分析只针对程序中的数组下标和数组长度进行静态污点分析, 包括过程内和过程间污点分析.本文将外部输入(包括用户或文件的输入以及主函数的参数)作为污点源.通过污点传播, 可以得到程序中每个关注变量v的污点值T(v), 可以是被污染(tainted)或者无污染(untainted), 即

$ T\left( v \right) \in \left\{ {tainted, untainted} \right\}. $

污点值的tainted可以对应布尔值1, untainted可以对应布尔值0, 因此可以使用逻辑运算符“或”(记为⋁)来计算污点值的和, 即只要有一个子表达式的污点值为tainted, 则整个表达式的污点值为tainted.

2.3.1 污点传播规则

对于污点分析中遇到的每条语句, 将按照如下污点传播规则计算该语句的污点值.

常量.每个常量c是非污染的.比如字符串常量、整型常量和浮点型常量等.

$ T\left( c \right) = untainted. $

类型转换.类型转换后的表达式CastExpr(e)的污点值与原来类型的表达式e的污点值一致.

$ T\left( {CastExpr\left( e \right)} \right) = T\left( e \right). $

数组下标表达式.将被当作一个整体, 数组的某一个元素被污染, 则整个数组为污染的.结构体同理.

$ T\left( {arr\left[ i \right]} \right) = T\left( {arr} \right), T\left( {expr.elem} \right) = T\left( {expr} \right). $

一元运算表达式.op expr的污点值等于其中表达式expr的污点值.

$ T\left( {op{\rm{ }}expr} \right) = T\left( {expr} \right). $

二元运算表达式.expr1 op expr2的污点值等于子表达式expr1和expr2的污点值之和.

$ T(expr1opexpr2) = T\left( {expr1} \right) \vee T\left( {expr2} \right). $

三元运算表达式.expr1?expr2:expr3的污点值等于子表达式expr2和expr3的污点值之和.

赋值表达式.赋值语句expr1=expr2将把右侧表达式的污点值传递给左侧变量.

$ T\left( {expr1} \right) = T\left( {expr2} \right). $

条件语句.if c then expr1 else expr2将把条件语句中条件表达式c的污点值传递给基本块中的赋值语句中的左值.循环语句同理, 同时, 循环变量的污点值等于循环上界的污点值.

函数调用语句.设函数f有n个参数, 对f的调用语句将把第i个实参p_i的污点值传递给第i个形参a_i.

$ \forall i \in \left[ {0, n} \right), T\left( {{a_i}} \right) = T\left( {{p_i}} \right). $

同时, 函数调用语句将把被调用函数返回值的污点状态传递给调用者被赋值的变量.

函数返回语句.如果返回的是变量, 则函数返回值的污点值等于该变量的污点值; 如果返回的是常量(包括返回值为空), 则函数返回值的污点值为untainted.

2.3.2 按需过程内污点分析

污点分析前, 首先统计程序中所有与数组下标和数组长度相关的函数, 以及直到入口函数的所有调用者函数, 构成数组相关函数集合FS.过程内的污点分析是对FS中的每个函数进行前向数据流分析.对于函数中的每个基本块, 使用InState表示一个基本块在该基本块入口时的污点状态, 是其所有前驱基本块的OutState的并集, 代表在该基本块执行前所有表达式的污点状态; OutState表示一个基本块在该基本块出口时的污点状态, 是在该基本块的InState的基础上, 由该基本块中的语句按照上一节中的污点传播规则更新表达式的污点状态的结果, 其中, Kill将消除表达式的污点状态, Gen将生成表达式的污点状态:

$ InState\left( {block} \right) = { \cup _p}_{ \in pred\left( {block} \right)}OutState\left( p \right) $

(3)

$ OutState\left( {block} \right) = Gen\left( {block} \right) \cup \left( {InState\left( {block} \right)-Kill\left( {block} \right)} \right) $

(4)

对于包含循环的函数, 将迭代计算每个基本块的InState和OutState, 直到该基本块的InState和OutState的状态不再改变.函数的污点状态与函数出口基本块的OutState相同.这样, 就可以得到函数内所有表达式与相应函数形参之间的污点关系, 即为该函数f的污点摘要TS(f).

对于每个函数f, 其形参列表为A={a₁, a₂, …}, 函数中每个变量v的污点状态记为T(v), 其值可能是被污染、无污染或依赖于函数的形参, 即

$ T(v) = \left\{ \begin{array}{l} tainted\\ untainted\\ \bigcup\nolimits_{a \in A'} {T(a), A' = \left\{ {{a_i}|RelyOn({a_i}, v), {a_i} \in A} \right\}} \end{array} \right. $

(5)

2.3.3 按需过程间污点分析

首先将入口函数的参数标记为污染的.然后从入口函数开始, 对FS的所有函数依据调用图上的拓扑顺序分析, 通过函数调用语句, 在调用点将实参的污点值传递给函数形参, 计算得到FS中每个函数形参的污点值.如果有多个函数调用同一函数, 则被调用函数的参数污点值是其所有调用者实参的污点值之和.

对于函数f的第i个形参a_i^f, 其污点值是f所有调用者Caller₁, …, Caller_j相应实参p_i的污点值之和, 即

$ T\left( {a_i^f} \right) = \bigcup\limits_{k = 1}^j {T\left( {p_i^{calle{r_k}}} \right)} . $

当需要查询程序中表达式的污点状态时, 如果发现可以直接得到污点值, 则直接返回(tainted/untainted); 否则, 表示该表达式的污点状态依赖于函数的形参, 此时只需要将所依赖的函数形参的污点值T(a)代入到公式(5)第3个赋值中即可得到原表达式的污点值.

2.3.4 示例解析

如图 2所示的代码片段, 其中, 函数f的控制流程图如图 5所示, 图 5中冒号后的数字是入口语句的行号.分析可知, 4个数组表达式的数组下标为n、2和i.通过对函数f进行污点分析, 可以知道f中的变量n和i的污点值与f的参数m一致.然后对main函数进行污点分析, argc和argv由外部输入, 因此是污染的.由于main函数通过参数argc–1调用函数f, 导致函数f的形参m为污染的.进而, f中的变量n和i也是污染的.

2.4 数组越界缺陷检测

对于每一条数组访问语句arr[idx], 数组arr对应的数组长度列表为{len₀, len₁, …, len_n}, 其数组越界缺陷的检测结果记为W(arr[idx]), W(arr[idx])≡T表示该数组访问语句会导致数组越界, W(arr[idx])≡F表示该数组访问语句不会导致数组越界.

判定规则1.对于数组访问语句arr[idx], 如果数组下标idx为非污染的, 数组长度列表中任意一个长度为污染的, 则该数组访问语句会导致数组越界.

$ \left\{ \begin{array}{l} T(idx) \equiv untainted\\ \exists i \in \left[ {0, \left. n \right]} \right., T\left( {{s_i}} \right) \equiv tainted \end{array} \right. \Rightarrow W\left( {arr\left[ {idx} \right]} \right) \equiv T $

(6)

判定规则2.对于数组访问语句arr[idx], 如果数组下标idx为非污染的, 数组长度列表中每一个长度都为非污染的, 则如果数组下标小于数组长度列表中的每一个长度, 则该数组访问语句不会导致数组越界; 否则, 该数组访问语句会导致数组越界.

$ \left\{ \begin{array}{l} T(idx) \equiv untainted\\ \forall i \in \left[ {0, \left. n \right]} \right., T\left( {{s_i}} \right) \equiv untainted \end{array} \right. \Rightarrow W\left( {arr\left[ {idx} \right]} \right) \equiv \left\{ \begin{array}{l} T, \exists i \in \left[ {0, \left. n \right]} \right., idx \ge {s_i}\\ F, \forall i \in \left[ {0, \left. n \right]} \right., idx < {s_i} \end{array} \right. $

(7)

判定规则3.对于数组访问语句arr[idx], 如果数组下标idx为污染的, 假设程序中有n条与数组下标idx相关的语句, 构成语句序列为S₁, S₂, …, S_n, 将每一条语句转换为约束表达式, 则约束表达式序列为c₁, c₂, …, c_n, 设第i条语句S_i在函数f的基本块bb中, 此时数组arr对应的数组下标为idx_i, 数组长度列表为LenSet_i= {len₁ⁱ, len₂ⁱ, ……, len_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), 则该数组访问语句不会导致数组越界.

$ \left. \begin{array}{l} A:\left( {\exists i, \exists k, !\left( {{c_i} \to \left( {idx \ge len_k^i} \right)} \right) \equiv UNSAT} \right)\\ B:\left( {\exists i, !\left( {{c_i} \to \left( {idx < 0} \right)} \right) \equiv UNSAT} \right)\\ C:\left( {\forall i, \forall k, !\left( {{c_i} \to \left( {idx < len_k^i} \right)} \right) \equiv SAT} \right)\\ D:\left( {\forall i, !\left( {{c_i} \to \left( {idx \ge 0} \right)} \right) \equiv SAT} \right)\\ E:\left( {\exists i, \forall k, !\left( {{c_i} \to \left( {idx < len_k^i} \right)} \right) \equiv UNSAT} \right)\\ F:\left( {\exists j, !\left( {{c_j} \to \left( {idx \ge 0} \right)} \right) \equiv UNSAT} \right)\\ T\left( {idx} \right) \equiv tainted \Rightarrow W\left( {arr\left[ {idx} \right]} \right) = \left\{ \begin{array}{l} T, A \vee B \vee C \vee D\\ F, E \wedge F \end{array} \right. \end{array} \right\} $

(8)

依据以上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行.然后在父函数中继续进行过程内的后向数据流分析.过程间后向数据流分析过程将一直执行, 直到待检查语句集合为空或达到配置的检查深度.

算法1. 数组越界检测算法.

函数:ABChecker(CallGraph,CFG,Depth).

输入:CallGraph,CFG,Depth;

输出:Warnings.

1.for each f in CallGraph

/*in backwards topological order*/

2.  bbSet=Ø

3.   for each BB in CFG off

/*in backwards topological order */

4.    for each ArrStmt in BB

5.      if T(ArrStmt.idx)==untainted

6.        if T(ArrStmt.LenSet)==tainted

7.          Warnings.add(ArrStmt)

8.        else

9.          for each Len in ArrStmt.LenSet

10.            if ArrStmt.idx>=Len

11.              Warnings.add(ArrStmt)

12.              break

13.      else

14.        OutState[BB].add(ArrStmt)

15.    if OutState[BB]≠Ø

16.      bbSet.add(all predecessors of BB)

17.  ABCSet=intraABChecker(bbSet,OutState)

18.  if ABCSet≠Ø

19.    result=interABChecker(ABCSet,f,Depth-1)

20. Warnings.add(all ArrStmt in result)

函数:intraABChecker(bbSet,OutState).

1.while bbSet≠Ø

2.  BB=bbSet.pop()

3.  for each succ of BB

4.    OutState[BB]+=InState[succ]

5.  InState[BB]=Ø

6.  for each stmt in BB

7.    checkStmt(stmt,&OutState[BB])

8.  if OutState[BB]≠InState[BB]

9.    InState[BB]=OutState[BB]

10.    bbSet.add(all predecessors of BB)

11.  ABCSet=OutState[BB]

12.return ABCSet

函数:checkStmt(stmt,OutState[BB]).

1.for each ABC in OutState[BB]

2.  if imply(stmt, ArrStmt.idx,less,0)

3.    Warnings.add(ABC)

4.    OutState[BB].remove(ABC,low)

5.  else if imply(stmt,ArrStmt.idx,notless,0)

6.    OutState[BB].remove(ABC,low)

7.  for each len in ArrStmt.LenSet

8.    if imply(stmt,ArrStmt.idx,less,len)

9.      cnt++

10.    else if imply(stmt,ArrStmt.idx,notless,len)

11.     Warnings.add(ABC)

12.      OutState[BB].remove(ABC,up)

13.      break

14.  if cnt==ArrStmt.LenSet.size()

15.    OutState[BB].remove(ABC,up)

函数:interABChecker(ABCSet,f,Depth).

1.if Depth<=0 or ABCSet==Ø

2.  return ABCSet

3.result=Ø

4.for each caller off

5.  bbSet=Ø

6.  bbSet.add(caller.callsite.BB)

7.  OutState[callerBB]=update(ABCSet)

8.  set=intraABChecker(bbSet,OutState)

9.  set2=interABChecker(set,caller,Depth-1)

10.  result+=set2

11.return result

如算法1中函数checkStmt所示, 在数据流分析过程中, 对于遇到的每一条语句stmt, 将根据表 1和判定规则3进行处理.如果分析到一条语句可使公式(8)中的条件A或条件E满足, 则后续数据流分析中不再关注A、C、E; 如果分析到一条语句可使公式(8)中的条件B或条件F满足, 则在后向数据流分析过程中不再关注B、D、F.在后向数据流分析过程中, 主要关注与数组下标相关的语句, 如表 1的前两列所示, 主要包括包含该数组下标的条件语句(包括循环条件)和对数组下标的赋值表达式(包括声明赋值表达式和复合赋值表达式).其中, 声明赋值表达式中idx声明的数据类型如果是无符号类型, 则公式(8)中的条件F成立, 同时, 条件B和条件D不成立.本文提供了两种判断方法来检查公式(8)中条件A~F是否满足, 即简单匹配方法和约束求解方法, 将条件A~F统一用c_i→(idx op expr)来表示, 以下描述中均先假设数组访问语句所在的基本块条件语句.

简单匹配处理方法.主要处理包含目标数组下标和常量的语句, 即条件格式为(idx op const₁)→(idx op const₂), 且当其中的两个操作符op一致时, 通过比较两个常量const₁和const₂来判断条件的可满足性.针对不同类型的语句, 如表 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₁==idx₀ op expr→idx₁ < 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, 因此, 找到了16行的s.arr[i]应满足i < 15的边界检查, 第16行的s.arr[i]将从待检查数组集合中移除.也就是说, Block4的InState是16行的tmp[i]中的, i < 3.然后继续向上分析Block5, 在Block5中遇到for语句时, 16行的tmp[i]中的i恰好为循环变量, 转换为循环越界问题处理, 即在循环上方检测循环上界n是否会超出数组tmp的长度, 即检测n < 4.Block6中的待检测数组信息OutState为16行的tmp[i]中的n < 4, 11行的s.noisy[n]中的n < 12.当遇到Block6中的赋值语句时, 待检测数组信息将更新为16行的tmp[i]中m < 4, 11行的s.noisy[n]中的m < 12.因此, 当遇到函数f的入口时, 待检测数组信息不为空.如果配置的检测深度为1, 那么将报告数组越界警告.否则, 将执行过程间的后向数据流分析.

在函数main中, 根据实参更新待检测数组信息为16行的tmp[i]中的argc < 5, 11行的s.noisy[n]中的argc < 13. if语句的条件为argc+2 < 15, 使用简单匹配方法, 则11行的p.noisy[n]的数组边界检查条件n < 12可以被满足, 因此, 简单匹配方法中的警报“test.c, line 11, p.noisy[n], n < 12”为误报.但是12行的循环上界n应小于11才可以保证15行的arr[i]中的i < 10, 因此, 简单匹配方法和约束求解方法中的警报“test.c, line 12, arr[i], n < 11”为真警报.

因此, 当使用简单匹配方法进行判断时, 无法匹配可以处理的模式, 将会报告:

当使用约束求解方法进行判断时, 可得!((argc+2 < 15)→(argc < 13))≡UNSAT, !((argc+2 < 15)→(argc < 5))≡SAT, 因此将会报告:

3 实现和实验评估

本文扩展了我们的前期工作^{[16, 17]}, 实现了一个面向数组越界缺陷检测的全自动跨平台的静态分析工具Carraybound, 优化了按需污点分析, 并增加了按需指针分析, 从而以此来分析数组长度的区间, 引入了定理证明器Z3^[15], 在数组越界检测过程中用以解决约束求解问题, 工具的架构如图 6所示.该工具可以在Linux和Windows系统上运行, 底层依赖于Clang 3.6和约束求解器Z3, 由数组长度区间分析、按需污点分析和数组越界缺陷检测共3个模块组成.提供了可配置的功能实现用户按需调节检测精度, 用户可以配置函数层数来控制执行过程间数据流分析的深度, 并通过内存优化、求解优化等措施提升了工具的效率.

3.1 实现优化

内存优化.大规模程序总是包含大量AST文件.如果一次性读入所有AST文件, 包含AST文件的所有内容, 将会消耗大量内存.这将会严重制约Carraybound对大规模程序的支持.比如, PHP-5.6.16包含25万行源代码和211个AST文件, 当我们尝试一次性读入所有AST文件时, 在2GB内存的机器上将无法运行.为了支持在有限的内存资源下扫描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.

Q1  有效性评估.我们分别统计了赋值语句简单匹配处理方法(CAB-simple)和约束求解处理方法(CAB-Z3)的误报情况, 发现前者的平均误报率为29.2%, 后者的平均误报率为16.3%.导致约束求解匹配处理方法误报的主要原因是我们无法处理一些库函数调用, 如果在条件语句或者赋值语句中存在库函数调用并保证了数组边界, 但是我们却无法判断从而导致误报.而赋值语句简单匹配处理方法相比约束求解匹配处理方法存在更多误报的原因是前者只简单匹配一些固定格式的语句并要求语句中特定位置为常量, 很多复杂情形无法处理导致误报; 而通过约束求解我们可以增强条件判断的能力, 除了能处理更多的线性约束, 甚至可以处理非线性约束.

Q2  效率评估.为了评估Carraybound的分析效率, 我们统计了如表 3所示的程序的分析时间和内存消耗.约束求解匹配处理方法由于调用约束求解器, 总体会比赋值语句简单匹配处理方法消耗更多的时间和内存.但是时间平均增加了1.53%, 内存平均增加了0.86%.使用约束求解方法并未造成明显的时间和内存消耗增加.这是因为, 一方面, 我们存储和复用了约束求解的结果, 避免了冗余的约束求解; 同时, 我们针对求解expr1→expr2约束进行了专门的优化, 减少了对约束求解器的调用; 另一方面, 由于约束求解可以精确地判断程序语句是否对数组边界进行了检查, 可以尽早地移除已经被满足的数组边界检查, 从而从总体上能够节约开销.如表 3所示, 我们可以发现赋值语句简单匹配处理方法和约束求解匹配处理方法在时间和内存消耗上都随着程序规模的扩大, 呈现接近线性趋势的增长, 因此我们的方法具有很好的可扩展性.

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时间, 因此复杂数组下标也会导致约束求解方法的误报和漏报.比如数组下标为包含按位运算的表达式, 将会导致判定准则中的约束更为复杂, 从而无法在指定时间内求解, 进而导致误报.

4 相关工作 4.1 污点分析

动态污点分析是一种当前流行的软件分析方法.当前有很多工作通过进行动态污点分析来追踪软件中的隐藏漏洞^{[10, 21-23]}.污点分析将可能包含恶意数据的外部输入作为污点源, 比如网络数据包; 然后, 跟踪这些污点数据如何在整个程序执行过程中传播; 当敏感数据(如堆栈中的返回地址或用户特权设置)被污点数据污染时执行相应的处理操作.

与动态污点分析相比, 静态污点分析以静态方式追踪源码或二进制文件中的污点信息.STILL^[24]是一个基于静态污染和初始化分析的防御机制, 可以在各种互联网服务中(例如Web服务), 检测嵌入在数据流中的恶意代码.为了减少污点分析的开销, TaintPipe^[9]借助轻量级的运行时日志记录来生成紧凑的控制流信息, 并产生多个线程, 以流水线的方式并行地执行符号化污点分析.静态污点分析面对的另一个问题是耗费人力.大多数现有的静态污点分析工具会在潜在的易受攻击的程序位置报错.这会导致需要开发者人工确认报告, 为此需要耗费大量的人工成本.Ceara等人^[25]提出了一种污点依赖序列算子, 主要基于细粒度的数据流和控制流污点分析, 为程序员提供需要被分析的路径的一些相关信息.

4.2 指针分析

Andersen算法^[26]和Steensgaard算法^[27]是最具代表性的流不敏感的指针分析算法.Andersen指针分析方法^[26]是一种基于包含的经典的C语言指针指向分析算法, 该算法被认为是最精确的流不敏感、上下文不敏感的指针指向分析算法.该算法将程序中的直接指向关系描述为变量与对象之间的约束关系集合, 再通过求解约束关系集合的传递闭包, 计算得到间接的指向关系, 从而获得所有变量的、完整的指向关系集合.这种基于包含的思想被广泛应用在后续的指针指向分析工作中^[28].Steensgaard算法^[27]是一种基于等价的指针分析算法, 其复杂度接近于线性复杂度.但是流不敏感的指针分析将会影响后续静态分析的精度.目前也有一些流敏感的指针分析算法, 这些方法通常是基于数据流分析^[29], 比如Emami算法^[30]、Lam算法^[31]、Chase算法^[32]等.本文的流敏感、上下文敏感指针分析是按需分析, 即只针对所关心的数组名进行指针分析.

4.3 数组越界检查

Xu等人^[33]提出了一种可以直接在不受信任的机器码上进行分析的方法, 该方法依赖于这些程序的初始输入的类型状态信息和线性约束.Detlefs等人^[34]提出了一种针对常见程序错误的静态检查器, 包括数组下标越界、空指针解引用和多线程程序中的并发类错误.该方法利用线性约束, 自动合成循环不变量用于边界检查. Leroy和Rouaix^[35]提出了一个理论模型, 系统地把基于类型的运行时检查放入主机代码的接口程序中.Kellogg等人^[36]提出了一种在编译时检测数组越界的轻量级验证方法, 但是为了达到线性验证时间, 该方法需要开发者预先注释相关信息, 例如程序边界信息.相比之下, 我们的方法能够分析出程序边界.ABCD^[37]用于按需消除无用的数组边界检查.它平均能够删除45%的动态边界检查指令, 有时可以实现接近理想化的优化.

当前也存在许多静态的数组越界检测工具^[38-40].Chimdyalwar^[8]对5种用于检查数组越界的静态分析工具进行了评估.其中, 商业工具包括Polyspace和Coverity; 学术工具为ARCHER, 其他两个是开源工具UNO和CBMC.Polyspace是唯一无漏报的工具, 但是由于它是内存密集型分析, 不能以同样的高精度扩展到大规模程序上.相比之下, Coverity可以支持百万行级别的代码分析, 但存在大量误报.UNO同时有误报和漏报, 并且不能应用在大规模程序上.ARCHER宣称可以运行在百万行级别的代码上, 但是分析并不完善.CBMC模型检查器进行了精确的分析, 无法在大规模程序上达到相同精度.Nguyen等人^[39]提出了针对Fortran语言的数组越界静态检查方法.Arnaud等人^[38]提出了针对嵌入式程序中数组越界检查的静态分析方法, 该方法处理的程序规模为20+万行, 我们的方法可以处理百万行程序.由于该文献提供的工具CGS是根据NASA程序定制的闭源工具, 并且使用了NASA闭源程序作为被测对象, 因此, 我们在实验中没有与该方法进行比较.

4.4 针对数组越界的缓冲区溢出检测

当前有很多关于缓冲区溢出检测的工作.大多数工作在检测缓冲区溢出的同时也能检测数组越界缺陷.

Tance^[41]提出了一种黑盒组合测试方法检测缓冲区溢出漏洞.Dinakar等人^[42]提出通过对内存进行细粒度的划分等技术来降低C/C++程序动态数组越界检查的运行开销.如Loginov^[43]和rtcc^[44]等基于插桩的方法能在运行时检测是否出现缓冲区溢出.但是这些方法会引入额外的运行时开销, 从而降低测试的效率.例如, Loginov工具的额外开销高达900%.SafeC^[45]、Cyclone^[46]和DangDone^[47]使用扩展的指针表示, 这些扩展包含每个指针值的合法目标对象的对象基础信息和大小.使用这些指针要对程序进行大量修改以使用外部库, 这些外部库函数通常是被包装好的用于转换指针的方法.此外, 编写这样的封装对于间接函数调用以及访问全局变量或存储器中其他指针的函数来说可能是难以实现的.

预防技术是一种用于防止数组下标越界被利用的方法.例如, StackGuard^[2]可能在检测到堆栈上的返回地址被覆盖后终止进程.运行时预防的现有方法具有显著的运行时开销.除此之外, 这些方法在可能有漏洞的程序部署完成后生效.CFI^[48]检查程序的控制流程是否在执行期间被劫持.这与我们的工作形成对比, 我们的工作目的是在部署之前发现程序中的数组越界缺陷.

4.5 针对数组越界的模糊测试

模糊(fuzzing)测试是安全测试中使用最为广泛的黑盒测试方法之一.该方法在检测数组越界或缓冲区溢出问题中也发挥着重要作用^[49-57].它主要通过程序崩溃检测数组越界缺陷.模糊测试通常从一个或多个合法输入开始, 然后随机改变这些输入以获得新的测试输入.高级模糊测试技术^[50]是基于生成的模糊测试技术, 它为了解决具有复杂输入结构的程序的输入生成问题, 通过基于语法的输入归约定义有效输入.Godefroid等人^[51]提出了一种替代的白盒模糊测试方法, 结合符号执行和动态测试生成.虽然模糊测试可以检测到数组越界错误, 但一个主要限制是代码覆盖率低.此外, 一些数组越界的错误可能只读取越界的区域, 因此不会导致崩溃, 这样, 模糊测试中的监视器可能无法检测到这种情况^[52].我们的方法基于静态方法, 可以实现高代码覆盖, 并且可以检测不同类型的数组下标越界.

5 结论和未来工作

本文提出了一种基于污点分析的数组越界缺陷的静态检测方法, 并实现了一个可以在Windows和Linux操作系统上运行的自动化静态分析工具——Carraybound.如果程序中存在数组越界缺陷, 我们将报告相应的数组位置和待添加的数组边界条件.我们通过扫描一些真实程序的源代码来评估Carraybound工具.实验数据表明, Carraybound可以快速报告在程序中没有进行数组边界检查的数组下标, 在使用约束求解方法时, 误报率大约为16.3%.尽管Carraybound有一些误报和漏报, 但它可以有效地减少程序员人工审查工作.我们的方法可以提供待增加的数组边界检查条件和位置, 可以帮助程序员更加方便、快速地定位和确认所报告的数组越界警报, 也可以作为修复推荐建议提供给程序员来参考.

目前, Carraybound由于库函数等原因, 可能导致误报, 对于库函数有源码的情况, 可以考虑通过函数摘要等技术完成更高精度的数组越界缺陷检测, 对于库函数无源码的情况, 可以考虑结合动态测试的方法来检测; 另一方面, 数组越界缺陷是一类特殊的缓冲区溢出缺陷, 我们可以考虑扩展到对缓冲区溢出缺陷的检测, 对于常见的缓冲区溢出相关API, 如strcpy、memcpy, 可以通过定义总结其溢出条件, 建立缓冲区溢出模型, 再利用数据流分析检测程序中是否有相应的越界检查语句, 从而检测缓冲区溢出缺陷.