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

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

因此,为了进行高精度的、高效的静态分析来检测数组越界缺陷,一方面,我们提出使用按需污点分析计
算数组下标和数组长度的污点值,当数组长度污染时,即使在数组下标非污染的情况下仍然可能导致数组越
界(比如图 2 第 11 行所示的数组访问语句),而在数组下标污染时,则需要进行高精度的数据流分析以检测是
否会导致数组越界;另一方面,我们提出在静态分析的过程中使用优化后的约束求解器来处理程序中与数组
访问相关的复杂约束和复杂表达式,从而有效地提高检测方法的准确性.对于数组下标越界问题,我们关注从
程序入口到数组访问语句之间,数组下标越界条件的可满足性,通过将约束求解引入到数据流分析过程中,能
够更加精确地检查数组越界问题.
在本文中,我们提出了一个静态分析框架 Carraybound,该框架基于静态的污点分析、数据流分析以及约束
求解检查程序中是否存在潜在的数组越界缺陷.除此之外,Carraybound 还提供待增加的数组边界检查条件,可
以帮助程序员更加方便、快速地定位、确认和修复我们报告的数组越界警报.实验结果表明 Carraybound 可以
快速、有效地报告出程序中的数组越界缺陷,并通过与已有静态分析工具 Cppcheck、Checkmarx 和 HP Fortify
进行对比,展示了 Carraybound 在发现数组越界缺陷上的优越性.
本文的主要贡献包括:
• 提出流敏感、上下文敏感的按需指针分析方法,实现数组长度区间分析;提出按需污点分析方法,实现数
组下标和数组长度污染情况的计算.
• 提出基于污点分析的数组越界缺陷的检测方法,定义了数组越界缺陷判定规则,然后依据判定规则,使用
后向数据流分析检测数组越界,并将约束求解引入到数据流分析过程中以检查数组越界缺陷,同时通过优化尽
量减少对约束求解器的调用,以提高分析效率.
• 实现了一个静态分析工具 Carraybound,检测 C 程序中的数组越界缺陷(包括由循环导致的数组越界缺
陷),并通过实验展示了工具的有效性.
本文第 1 节介绍我们工作的背景知识.第 2 节介绍所提出的基于污点分析的数组越界的静态检测方法.第 3
节介绍实现工具 Carraybound,并通过实验展示该工具的有效性和效率,同时讨论该工具的不足之处.第 4 节介绍
相关工作.第 5 节进行总结,并提出未来工作展望.

1 背景知识

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