IntScope (2009)

原文：IntScope: Automatically Detecting Integer Overflow Vulnerability in X86 Binary Using Symbolic Execution

Intscope是专门针对整数溢出漏洞的静态分析工具。没有一个基于fuzz的二进制代码分析是专门针对整数溢出的，而且即使fuzzing工具可以探索所有的程序路径，漏洞还是可能无法重现，如果它没有生成对应的输入的话。

大部分一致的整数溢出漏洞都是由于不完全或者不恰当的输入验证（incomplete or improper input validation）造成的。IntScope采用符号执行和数据流分析（如污点分析）自动检测缺少合适输入验证的程序路径。

整数漏洞还有很多，除了溢出之外，还有assignment truncation, integer underflow, signedness error等，IntScope只关注溢出问题，因为它占了所有整数漏洞中约70%的数量。

思路：

• 在类SSA的IR基础上符号执行x86二进制文件
• 利用污点分析，不仅跟踪污染属性的传播，也对被污染数据的准确边界建模
• 使用lazy checking，并不检查所有算术操作，只检查出现在敏感点的被污染的符号值（如malloc, alloca是否可能在路径约束条件下溢出。

用IDA Pro反编译，然后翻译成自己的IR——PANDA。检测到了所有已知的整数溢出漏洞，并发现了超过20个新的整数溢出漏洞（如CVE-2008-4201, FrSIRT/ADV-2008-2919）出现在QEMU、Xen、Xine、MPlayer和VLC中。这些漏洞都用他们自己的动态测试工具证实过了。

贡献：

• 针对整数溢出的污点分析+路径敏感符号执行分析；
• PANDA中间表示，基于IDAPro的结果和符号执行引擎；
• 实现了IntScope，发现现实世界的漏洞。

整数溢出漏洞的分析

特征

• 不可靠的来源。大多数的整数溢出漏洞都源自被污染的操作数，而它们则来源于不可靠的输入，如网络报文、输入文件或者命令行选项。典型的源函数则有read, fread, recv。

• 不同类型的汇点（sink）。溢出是否有害取决于程序如何使用这些溢出值，所谓汇点指的是程序中一旦使用溢出值就会造成危害的（敏感）点。通常汇点出现在以下部分：

  • 作为内存分配函数，如malloc, alloca，的尺寸参数
  • 作为数组的索引或指针的偏移量
  • 作为分支指令的判定条件
  • 作为和程序相关的敏感点，如CVE-2002-1490中可溢出值被当作了结构引用计数器
• 不完全或者不合适的检查

整数溢出漏洞分析所面临的挑战有：

• 缺少类型信息。对于signed int和unsigned int，同样的数值会导致不同的结果（溢出或者不溢出）。

  mov eax, x; // eax = x add eax, 2; // eax = eax + 2 %js target

• 区分有益的溢出。如语句 if (x >= -2 \&\& x<= 0x7ffffffd)会被GCC-4.2.0翻译成上面的形式，此时如果 x = 0x7fffffff，则会产生溢出，但GCC使用这个溢出化简掉了一条比较指令，是无害的。
• 路径爆炸。溢出的主要原因是不合适的检查，这需要对程序路径进行分析（路径敏感），然而软件中的路径数量过于庞大，尽管可以采用函数摘要（function summaries）降低数量级，但仍然是个问题。

##系统设计

大部分的整数溢出漏洞都是由于汇点处（如内存分配函数）溢出值的错误使用造成的。IntScope因此跟踪污染数据的传播，收集关于污染数据的路径约束，当污染数据出现在汇点时，查路径是否对数据进行了足够的溢出检查。因为只检查在汇点处被使用的污染数据，称之为“懒惰检查”（lazy checking）。这种方法既可以区分“好的”溢出，也可以减少检查数量。此外，大部分的汇点在类型推导（type inference）时都会有提示。为了缓解路径爆炸，** 只分析从源函数（如read, fread, recv）到汇点函数（如malloc, alloca, LocalAlloc）的路径**。IntScope以二进制文件为输入，输出导致溢出值出现在汇点的可疑路径。

IntScope分为两个部分：程序预处理和溢出检测。预处理分为三个组件：Decompiler, Component Extractor, Profile Constructor。首先Decompiler将程序P反汇编，得到类SSA的IR，PANDA描述，同时构建控制流图CFG和调用图CG。然后利用Component Extractor和Profile Constructor组件计算控制流图的片段G’，G’包含从源函数点到汇点函数的路径。G’为预处理部分的输出。

Decompiler采用了它们内部开发的Bestar，该反编译器利用了IDA Pro作为前端执行反汇编、识别控制流结构，之后翻译成PANDA。

第二部分溢出检测分为四个组件：Integer Overflow Checker, Path Validator, Symbolic Execution Engine, Symbolic Memory Environment。首先用深度优先搜索遍历G’，它维护着符号内存环境，并符号执行二进制代码，以PANDA的形式。同时，跟踪污染数据，在每个分支点，由Path Validator组件检查该分支在当前路径约束下是否可达，如果两条路径均可达，则fork出一个额外的执行并模拟每条路径。遇到被污染数据出现在汇点时，则由Integer Overflow Checker组件实施约束检查，一旦被污染值能够溢出，则将其路径记为可疑并输出。

Symbolic Execution Engine基于GiNaC开发，GiNaC是一个使用C++的开源的符号计算框架。使用它可以很方便的描述和操作符号表达式。

Integer Overflow Checker, Path Validator基于STP开发，用于处理符号约束。关键是STP支持符号敏感（signed/unsigned）的关系操作。

PANDA的设计。为什么要采用IR？x86指令集太复杂，数目众多，很多都有副作用；没有记录变量；需要推导、记录符号地址的相互关系以跟踪被污染数据的扩散。PANDA区分了符号数比较和无符号数的比较。PANDA有两种变量：mem型和val型。前者对应寄存器或者内存，可以多次赋值，但只能作为左值；后者表示内存地址中储存的值，只能作为右值。

Component Extractor组件（CE）和Profile Constructor组件（PC）。负责选择可能同时（显式或间接）调用源函数（src）和汇点函数（sink）的函数。对于调用图C，节点为函数名，边为调用关系，那么CE组件只需寻找被污染的src和sink的公共祖先（common ancestor）作为候选。PC组件利用CE得到的候选函数计算控制流图片段G’，控制流图的节点为指令，边为指令流向，对于候选函数的控制流图，PC计算G’的节点集合为\(E_{sr}\cup (S_e\cap E_{sk})\)，如果\(S_e\cap E_{sk}\ne \emptyset\)。其中，

• $E_{sr}$表示从函数入口到集合$S_r$中各节点的路径集合，$S_r$为调用src的节点集合；
• $E_{sk}$表示从函数入口到集合$S_k$中各节点的路径集合，$S_k$为调用sink的节点集合；
• $S_e$集合包含了从$S_r$到函数出口点的路径上的所有节点。

内存建模。模拟程序执行需要构造符号内存空间，维护符号内存地址和符号值。IntScope使用了三种映射关系。M：符号地址到变量名的映射；ST：变量名到符号值以及其它信息的映射，如位长（如qword, dword, word, byte）、类型（如mem型变量或val型变量）；VT：符号值到值属性的映射（如该值是否被污染）。是否被污染依赖于变量的当前值，如果多个变量拥有相同的被污染值，则一旦它们中间的一个被彻底的检查，则所有变量都是可信的。

执行策略。从入口点出发，探索所有可达路径，维护符号内存空间并更新之。

• 遇到分支时，两个分支都检查，如果可达则继续执行。
• 间接跳转的操作数如果是地址，则继续执行，若是符号值则终止。
• 对于调用指令，实施进程间分析，模拟函数调用栈。
• 对于和污染数据扩散相关的函数，实施函数摘要。如对于read, fread等函数，对其参数 buffer做被污染的标记。
• 对于循环，这是静态分析中的难点。如果边界是符号变量，只对其中的分支遍历一遍；如果边界是常数，尽可能准确地模拟之
• 块内存操作（如strncpy, memcpy, memmove等）在其参数size为符号值时比较难办，比如memcpy(dst, src, n)中的n若未确定，则无法对dst的访问进行检查。由于IntScope只关心污点的传播，所以如果src是被污染的缓冲，则dst也是被污染的，从地址dst开始的值都给个被污染的值即可。

懒惰检查。整数溢出是否有害取决于溢出值是如何使用的。因此，当被污染值在sink处被使用时，对其是否溢出进行检查。

• 很多sink隐含了类型信息，如内存分配的参数size通常都是unsigned int类型，那么它一般就不会大于$2^{32}-1$；数组的索引也不会是负数；谓词中如果出现了污染值也需要进行检查，看溢出值是否会改变谓词的结果。
• 跳转语句也会给出类型信息，如JG, JNLE, JGE, JNL, JNGE, JLE, JNG, JE都是符号数比较，而JA, JNBE, JAE, JNB, JB, JNAE, JBE, JNA, JE, JNE都是无符号比较。
• 对于无符号比较中的x + y, x * y，检查其是否大于$2^{32}-1$；对于无符号比较中的x - y，检查其是否大于0；对于有符号比较中的x + y，执行类似于__addvsi3的检查

即使发现了谓词中的被污染数据可能溢出，也并不报警，而是检查该谓词本身是不是为了检查溢出错误的。通常，此类利用错误结果检测溢出错误的代码都有一定的模式，如

if ((x+1)<x), if(x !=(x*y)/y)

等，而且这些代码一旦成立（确实有溢出），很快就会return或跳到错误处理函数。这种情况通常不报警。至于复合分支语句，如

if (x>0 && (x+y)<y)

会被编译成多条比较语句，需要专门加以识别，见它们之前的工作。

IntScope在Linux下运行。它是静态工具，所以会有假警报，需要动态测试生成工具¹以验真伪。这个工具可以从“好的”输入出发，执行程序到一个特定的点。对于300Kb左右的二进制文件，IntScope需要290s翻译成PANDA，得到的IR文件约5Mb，而符号执行需要300s。如何减少IntScope的误判：获得输入之间的约束；获得全局变量的信息；更准确的符号执行，IntScope对于块内存函数和字符串函数的模拟是有近似的。

相关工作

整数误用的检测和保护。为了防止整数溢出错误，引入了编译器扩展和安全C++整数类等技术。如GCC的 -ftrapv选项，允许在signed加法操作前插入额外的调用（如__addvsi3）检查整数溢出。Rich根据C语言中整数的安全操作语义加入了运行时检查。这种运行时检查会生成false positive，因为它没有考虑“善意”的整数溢出。使用其他的安全C++类，如SafeInt、IntSafe等，以及任意精度算术包（如GMP、CLN），虽然可以缓解此类整数安全问题，但是其性能损耗是不能忽略的。

用污点分析来检测整数型漏洞相当的有效。如Ebrima N. Ceesay et al.、Ashcraft and Engler，以及Sarkar et al.的工作。

UQBTng是一个用来发现Win32二进制代码的整数溢出的工具，它用UQBT将二进制代码翻译成C代码，然后UQBTng在内存分配函数之前插入assert，然后用模型检测器CBMC验证属性。UQBTng的表现完全依赖于翻译器的能力，而这项技术现在仍不理想。

二进制分析。Vine是BitBlaze的静态分析组件，它将x86指令翻译为一种类RISC的中间表示（Intermediate Representation，IR），并以此为基础实施数据流和控制流的分析。IntScope也可以在Vine的基础上实现。

CodeSurfer/x86是一个二进制分析平台，利用了IDA Pro和CodeSurfer工具。它使用了值-集合分析（Value-Set Algorithm，VSA）算法恢复二进制文件中类似变量的项，并将二进制文件翻译成CodeSurfer可以接受的IR。

Chevarista是一个基于SPARC平台的自动漏洞分析工具。它提到了一种基于模型检测来检测竞争条件的技术。

符号执行。符号执行广泛用于EXE、CUTE、DART、SAGE、Bit-Scope²、Archer等项目。Archer、EXE、CUTE和DART都是在程序源代码中假如一个符号执行引擎、使用混合执行生成测试输入或者找到可达路径上的可能漏洞。SAGE则第一次运行了目标程序恶并收集真实的路径，然后再虚拟地重新执行所记录的路径以手机和输入相关的约束并生成新的约束。BitScope则实现了混合执行以分析恶意二进制代码。