IntEQ: 基于多精度等价验证的良性整数溢出识别方法

程序员会故意使用整数溢出来实现特殊功能或代码简洁，而现有工作对良性整数溢出的识别能力很低。本文提出了基于多精度等价验证的识别方法IntEQ，通过验证原始版本和高精度版本的语义等价性，即在所有可能输入下的输出是否一致，来判断该溢出是否为良性。...



在C/C++语言中，算术运算如加法、减法、乘法和左移操作可能使运算结果超出相应类型的表示范围，引发整数溢出（integer overflow）。攻击者常常借助程序安全性操作（如内存分配函数malloc、while循环语句、if分支语句和数组下标引用等）间接利用整数溢出，完成恶意攻击行为。图1描述了一个整数溢出漏洞实例。攻击者可恶意构造一个拥有很大width和height的PNG图片文件，引发第12行的整数乘法操作溢出，然后导致第14行分配的内存空间比预期少，造成缓冲区溢出。然后导致第14行分配的内存空间比预期少，造成缓冲区溢出。



国际权威漏洞披露组织CVE在2007年的年度报告中指出，整数溢出已经达到仅次于缓冲区溢出的第二大软件漏洞。2011年的报告指出，整数溢出仍然位列25个最具危害的软件漏洞之中。因此，越来越多的研究人员将目光投向整数溢出漏洞的检测和预防中。例如，RICH、IOC、AIR、RA和IntPatch选择感兴趣的算术运算进行插装以实现实时保护。SmartFuzz、IntScope和Kint等利用符号执行技术来构造可以触发溢出的测试用例。SafeInt、CERT’s IntgerLib和Ranged Integer使用安全库函数封装算术运算。

整数溢出在很多情况下是良性的（benign），现实中程序员可能故意使用整数溢出以实现特殊功能（如哈希值计算、随机数计算）或者代码简洁。图2描述了一个良性整数溢出实例。SPECINT 2000中176.gcc故意使用第11行的有符号整数溢出来计算哈希值。第13行的按位与操作和第14行的取模操作确保溢出数值（即变量hi）在流入第17行数值下标引用前，保持在合法的取值范围内。然而，现有检测方法无法识别这些良性整数溢出，产生大量的误报。

识别良性整数溢出的挑战是如何从源代码中推理出程序员的使用意图。给定一个程序，如果没有程序员的注释，难以从中自动推理出程序员的真实意图。以图1中有害整数溢出和图2中良性整数溢出为例，图1第12行的乘法运算和图2第11行的乘法运算，二者的使用方式十分类似，即从外部获得输入，经过多个数值计算操作后，最终用于程序安全性操作（分别是图1 第14行和图2第17 行）。因此，仅从源代码的结构，难以区分这两个整数溢出。

IntFlow是当前识别良性整数溢出的最新方法。基本原理是如果一个整数溢出的两个源操作数都来自于可信源，则该溢出为良性。IntFlow 认为，仅由可信源决定的整数溢出不可能被攻击者利用到恶意攻击中。换言之，这类溢出是良性的。然而，在现实中仍存在大量的来自于非可信源的良性整数溢出。以图2为例，数组text来源于外部用户输入，因此InFlow 无法识别这类良性整数溢出而产生误报。



因此，我们的ICSE’16论文《IntEQ: Recognizing Benign Integer Overflows via Equivalence Checking Across Multiple Precisions》提出基于多精度等价验证的良性整数溢出识别方法。该方法基于两个重要观察：1）整数溢出的根本原因是采用有限比特来表示整数。我们认为，如果采用足够多的比特来表示整数，则原本发生溢出的运算将不再溢出。和2）溢出后数值最终被程序安全性操作使用，是危害软件的必要条件。我们认为，如果溢出数值在程序安全性操作处没有产生有害影响，则该溢出可判定为良性溢出。

具体思路是，首先利用静态数据流分析抽取出从发生溢出的算术运算到程序安全性操作之间所有可能路径。随后使用更高精度的整数类型为每条路径创建一个新版本路径。高精度版本的特点是，使用充足的比特来表示整数，使得原始版本下发生的整数溢出在高精度版本中不再发生。最后，使用约束求解器来验证原始版本和高精度版本是否语义等价。这里的等价是指，二者在相同的所有可能输入下，程序安全性操作的取值都是一致的。如果一个溢出实例的所有路径的原始版本和高精度版本都是语义等价的，那么该溢出判定为良性。

在GCC编译器和Z3求解器的基础上，我们实现原型系统IntEQ。实验表明，IntEQ可正确将26个现实CVE漏洞判定为有害溢出。IntEQ可成功识别444个良性溢出中的355个，识别精度为79.95%，而当前最新方法IntFlow仅能识别19个。

本文作者：南京大学计算机系博士研究生孙浩，美国Purdue University的Xiangyu Zhang教授，IBM T.J. Watson Research Center的Yunhui Zheng博士和南京大学计算机系曾庆凯教授

    关注 软件工程研究与实践