Targeted Automatic Integer Overflow Discovery Using Goal-Directed Conditional Branch Enforcement (2015)

原文：Targeted Automatic Integer Overflow Discovery Using Goal-Directed Conditional Branch Enforcement

DIODE工具

利用动态污点分析和符号执行自动生成导致在关键位置发生整数溢出的输入。

难点

程序本身会对输入进行sanity check，检查输入或整数运算操作数的合法性，仅靠random fuzzing等技术得到的新输入很难满足所有的sanity check。此外，还存在一种被称为blocking check的检查，此类检查可能会控制循环的次数或其他执行控制语句，从而影响执行路径。

流程

1. 先以种子输入（seed input）执行程序，动态污点分析找到受输入污染的溢出点（target site）。【种子输入没有执行的程序空间中的溢出点则无法进行检查】
2. 二次执行程序，利用插桩等技术找出溢出点的计算公式（以输入为参数），称为target expression。
3. 计算target expression的溢出条件，并求解该条件（称为target constraint），并以此为新的输入执行程序。如果触发溢出，则程序结束，此次生成的输入即为所求目标；否则记录其路径表达式，并进行下一步
4. 根据第二次执行（seed input）得到的插桩信息得到路径表达式，这条路径是能到溢出点的，但是不能导致溢出。
5. 对比新输入和seed输入的路径表达式，选取首个两条路径产生分叉的分支点的路径约束，将其沿种子路径执行时的约束加入target constraint（称为目标导向的条件分支强制执行，goal-directed conditional branch enforcement），返回步骤3

找到漏洞之后

配合另一个叫做CodePhage的工具，给定目标程序和另一个贡献者程序，从贡献者程序中找到消除bug的代码，加以变形后得到目标程序关于该bug的补丁。以二进制程序为输入，输出的补丁是源码级别的。

方法描述

采用了一种操作语义描述程序的具体和符号执行，并用这种语义来描述条件分支强制实行的算法。

实现

9000行的C和6000行的Python，前者主要是污点分析（基于Valgrind ）和符号表达式跟踪，后者主要是分支约束生成、和Z3接口，以及相关数据管理（包括分布式的work queue）。

可以接受文件或者网络连接作为输入，输入格式的解析用了Hachoir和Peach。用Valgrind的memcheck工具来检测新的输入是否真的触发了溢出。

实验结果

实验对象必须同时为Hachoir和Peach所接受。在5个application里找到了14个整数漏洞，其中11个是新的。

大部分的溢出会导致SIGSEGV【部分是因为他们只选择了malloc作为target site】，部分溢出仅导致无效的读写操作，并没有导致程序崩溃