Unleashing MAYHEM on Binary Code (2012)

原文：Unleashing MAYHEM on Binary Code

贡献

1. 混合online和offline执行。前者具体执行一条路径，然后符号执行（也叫conclic执行，如BitBlaze，SAGE），显然符号分支之前的路径都得执行两遍；后者不用两遍执行，它在每个分支点保留所有分支的状态，换分支时切换状态上下文就可以，这种切换很耗资源（比如KLEE，S2E「在执行过程中实时切换具体执行和符号执行」）。
2. 基于索引的内存模型
3. 基于二进制代码的攻击生成

能检查缓冲区溢出、函数指针覆盖和字符串格式，三种漏洞。共计27000行的C/OCaml代码。基于Pin做插桩，符号执行引擎约10000行。IL基于BAP，SMT是Z3。目前不能处理所有的系统调用，而且不能处理多线程。

关于BAP

Binary Analysis Platform，一个二进制程序的分析平台。可用于自动生成exploit、汇编类型推导、从代码生成验证条件（VC）等场景。BAP是Vine的重新设计，Vine IL缺少形式化的语义，而且不能处理双端构架（ARM）。它提供了

1. 将汇编语句副作用显式表示的中间语言（IL）
2. 常用的代码表示，如CFG、SSA、数据流分析框架、值集分析（value set analysis）等
3. 支持验证功能，提供了最弱前件、SMT求解（STP、SMTLIB1）、动态路径执行（Pin）的接口
4. 支持x86和ARM，开源

关于AEG

方法

分为具体执行组件CEC和符号执行组件SES。CEC接受二进制文件和输入规范（输入可以来自文件、网络和环境变量），并和SES通信。SES符号执行CEC输入的代码段，输出三种测试用例：正常的、导致程序崩溃的，和漏洞利用。过程如下：

1. CEC执行程序，并进行动态污点分析。
2. 如果分支指令或跳转目标被污染，CEC挂起，交给SES确定哪条路径可达，之后CEC执行可达的那条路径。SES需要具体值时由CEC提供。SES维护两种约束：路径约束和攻击约束（是否可以控制指令指针，是否可以执行payload）
3. 对于污染的分支点，SES通过SMT求解是否需要fork执行路径。如果需要，送到SES的路径选择器去排序，最优先的路径拿去给CEC执行。如果系统资源不够了，则不fork该路径，而改生成它的checkpoint。这一步的最后生成能让路径终止的测试用例。SES负责切换checkpoint和当前CEC执行路径的上下文，为此CEC维护了程序和环境的交互，以及checkpoint的。。。
4. 对于污染的跳转目标（buffer overflow中，指令指针如果被污染，则有可能指向shellcode；string format攻击中，如果格式参数被污染，则有可能改写函数返回地址指向shellcode），SES构造攻击约束并求解。如果有解，则生成相应的攻击利用。如果没有解，则继续探索执行路径。直到发现可利用的bug。
5. 从checkpoint恢复时，CEC根据路径约束具体执行到挂起点，而不是像别的标准的concolic执行工具一样符号执行。之后交给SES。

CEC

CEC除了具体执行程序、进行污点分析外，还要在SES的online执行时向它提供当前路径上必要的具体值，如register、memory和系统状态（文件、网络、和内核状态）。这很耗资源，所以和S2E、KLEE一样采用了复用。

SES——Hybrid Symbolic Execution

SES保存变量上下文和内存上下文。开始符号执行时先做online模式，当资源快耗尽/达到阈值时，为活动分支生成checkpoint。当所有分支都online执行完之后，选择优先级最高的checkpoint，交给CEC具体执行。CEC根据checkpoint里的路径约束计算程序输入，从头执行程序到checkpoint点，然后交给SES继续执行。

优先级的计算由启发式算法完成：路径如果经过新的代码，使用了符号内存或符号指针则更有可能包括新漏洞。

性能调整

三种技术：独立的公式（10倍）；算数化简（110%）；污点分析（8倍）。

符号内存的建模

40%的实验涉及到索引内存，但处理带索引的符号内存是很困难的。常见的办法是具体化索引或者将整个内存符号化。采用的办法是写内存都是具体化的，读内存则适当符号化。Mayhem利用路径谓词对符号索引求区间。求解谓词很花SMT的时间，为此采用了多种优化措施：如VSA分析，对VSA的结果做cache，对求解的公式正则化之后再做cache，以及使用二叉搜索树减少搜索索引对象的时间。

实验

自动化工具的几条原则：

1. 在给定资源的前提下，系统能自动向前分析，理想状态下是“永动”
2. 为了最大化性能，系统不能重复劳动
3. 产生的结果不要丢掉，之前的分析结果应该留着以备复用
4. 能推理（依赖于用户输入的）符号内存

MAYHEM 支持以下符号输入：command-line arguments (Arg.)，environment variables (Env. Vars)，network packets (Network) and symbolic files (Files)。

包括发现漏洞/新漏洞；内存的使用和工作速度；各种内存优化对结果的影响；代码覆盖率横向对比；性能调整效果。

实验包括了一个不需要用户干预的GUI程序。