2009 NDSS: IntScope
工具:IntScope
漏洞:整型溢出漏洞
技术:静态分析(符号执行 + 数据流分析)自动检测缺少合适输入验证的程序路径。
作者:王铁磊(TaintScope, S&P2010, 也是他的作品)作者个人主页
作者相关工作(整数相关)
- 2009, NDSS, IntScope:使用符号执行自动检测 X86 二进制文件中的整数溢出漏洞。
- 2010,S&P,TaintScope:用于自动软件漏洞检测的校验和感知定向模糊测试工具。
- 2010,ESORICS,IntPatch:在编译时自动修复整数溢出到缓冲区溢出漏洞。
- 2011,JOCS期刊,Using Type Analysis in Compiler to Eliminate Integer-Overflow-to-Buffer-Overflow Threat. 在编译器中使用类型分析来消除整数溢出到缓冲区溢出威胁。
简介
Intscope是专门针对整数溢出漏洞的静态分析工具。没有一个基于fuzz的二进制代码分析是专门针对整数溢出的,而且即使fuzzing工具可以探索所有的程序路径,漏洞还是可能无法重现,如果它没有生成对应的输入的话。
大部分一致的整数溢出漏洞都是由于不完全或者不恰当的输入验证(incomplete or improper input validation)造成的。
整数漏洞还有很多,除了溢出之外,还有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,发现现实世界的漏洞。
整型溢出漏洞分析挑战
缺少类型信息。对于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)降低数量级,但仍然是个问题
系统设计
ntScope分为两个部分:程序预处理和溢出检测。
预处理
预处理分为三个组件: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
型。前者对应寄存器或者内存,可以多次赋值,但只能作为左值;后者表示内存地址中储存的值,只能作为右值。内存建模。模拟程序执行需要构造符号内存空间,维护符号内存地址和符号值。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
开始的值都给个被污染的值即可。