Manticore中的符号路径合并

每年，Trail of Bits都会举办为期一个月的冬季实习“winternship”项目。今年我们很高兴接待了4名实习生，他们参与了3个项目。这是涵盖2019年Wintern班级系列博客文章的第一篇。

我们的第一份报告来自明尼苏达大学的博士生Vaibhav Sharma（@vbsharma）。Vaibhav的研究重点是改进符号执行器，他尝试为Manticore引入一种新的优化：

Manticore中的符号路径合并

我的项目是研究在Manticore中使用路径合并技术。Manticore是一个符号执行引擎，支持对为X86、X64和Ethereum平台编译的二进制文件进行符号探索。符号探索许多实际程序的一个主要障碍是路径爆炸。当符号执行器探索程序时，会遇到具有两个可行分支的指令。符号执行器需要探索分支指令的两个方向。Manticore通过将到达分支指令的路径分叉成两个路径来探索这些分支指令，每个路径探索一个可行方向。具有两个可行方向的分支指令数量线性增加会导致Manticore需要探索的路径数量呈指数级增长。如果我们遇到足够多的这些分支条件，Manticore可能永远无法完成所有状态的探索。

路径合并减少了需要探索的路径数量。核心思想是在相同程序位置合并相似的路径。Manticore使用“状态”对象的概念，在通过程序进行符号探索的每个点将处理器、内存和文件系统信息捕获到单个数据结构中。因此，在Manticore中，路径合并可以专门化为“状态合并”，在相同程序位置合并相似状态会导致需要探索的路径数量呈指数级减少。通过一个简单程序，我观察到如果Manticore在相同程序位置合并相似状态，它可以减少33%的探索执行路径数量。

状态合并可以静态或动态实现。静态状态合并按拓扑顺序探索目标程序的控制流图，并在可能时在相同程序位置合并状态。Veritesting是一种类似于静态状态合并的路径合并技术，它要求路径位于相同程序位置才能合并它们。动态状态合并不要求两个状态位于相同程序位置才能考虑合并。给定两个分别位于不同程序位置l1、l2的状态a1、a2，如果a1的传递后继a1′与a2具有高度且有益的相似性，动态状态合并将a1快速转发到a1′并将其与a2合并。快速转发涉及覆盖符号执行器的搜索启发式以到达l2。动态状态合并使用这样的直觉：如果两个状态相似，它们在几步内的后继状态也可能相似。

虽然可以在Manticore中实现任一种状态合并技术，但我选择Kuznetsov等人描述的动态状态合并，因为它更适合Manticore使用基于状态而不是基于路径的符号执行器。此外，静态状态合并不太适合针对目标引导的符号探索，更适合对目标程序进行穷举探索。由于静态状态合并只能在相同程序位置合并状态，当针对目标时，它在相同时间预算内往往比动态状态合并覆盖更少的代码。这也是Kuznetsov等人的结论（见下图他们论文中的图8）。由于我们经常倾向于使用符号执行来达到探索目标，静态状态合并不太适合我们的需求。

动态状态合并（DSM）比静态状态合并（SSM）提供更多的语句覆盖。图来自“Efficient state merging in symbolic execution.” Kuznetsov et al. 2012年6月11日。

工程挑战

静态和动态状态合并都需要使用外部静态分析工具（如Binary Ninja）来查找程序位置的拓扑顺序。鉴于我的实习时间较短，我选择实现机会主义状态合并，它只合并恰好位于相同程序位置的状态。虽然这种方法不能完全获得动态状态合并的好处，但它更容易实现，因为它不依赖于与外部静态分析工具的集成来获得拓扑顺序。这种方法也很容易扩展到动态状态合并，因为它使用许多相同的原始操作，如状态比较和状态合并。

实现

我为Manticore实现了机会主义状态合并。实现在“isMergeable”谓词中检查相同程序位置的两个状态是否具有语义上等效的输入、输出套接字缓冲区、内存和系统调用跟踪。如果满足此谓词，实现会合并语义上不等效的CPU寄存器值。

结果

我使用了一个简单示例，在该示例中我可以看到Manticore队列中保存的两个状态位于相同程序位置，使它们成为合并的良好候选。下面我展示此示例程序的部分CFG。

合并的CFG注释

以红色高亮显示的两个基本块导致控制流在以绿色高亮显示的基本块处合并。第一个高亮红色块导致控制流直接跳转到绿色块。第二个高亮红色块将常量（0x4a12dd）移动到edi寄存器，然后跳转到绿色块。为了探索此示例，Manticore创建两个状态，一个探索第一个红色块并跳转到绿色块，另一个状态探索第二个红色块并跳转到绿色块。由于这两个位于相同程序位置（绿色块）的状态之间的唯一区别是它们的edi寄存器中的值，Manticore可以将这两个状态合并为一个状态，其中edi的值设置为if-then-else表达式。此if-then-else表达式将使用选择分支（jbe 0x40060d）哪一侧被采用的条件。如果满足条件，if-then-else表达式将评估为第一个红色块中edi存在的值。如果不满足条件，它将评估为0x4a12dd（在第二个红色块中设置的常量）。因此，Manticore机会主义地将两个控制流路径合并为一个路径，最终导致Manticore在使用gcc的-Os优化选项编译的二进制文件上减少33%的执行路径数量，如果二进制文件使用-O3优化选项编译，则减少20%。

未来改进方向：

• 通过将Manticore与可以提供程序位置拓扑排序的工具集成，可以扩展此实现以获得动态状态合并的全部好处。
• 状态合并总是创建新的符号数据，因为它将代码区域中的所有具体写入转换为符号写入。
• 检查状态合并引入的新符号数据是否在后续探索中导致更多分支。我们需要实现重新解释启发式方法，如Kuznetsov等人的查询计数估计，以便我们可以在最有用时使用动态状态合并。

路径合并是一种需要重新解释以适应符号执行器需求的技术。这次实习让我了解了Manticore（一个基于状态的符号执行器）的内部工作原理，并重新解释了路径合并以更好地适应使用Manticore进行二进制符号执行的用例。我的机会主义状态合并实现如果状态位于相同程序位置，则合并相似状态。该实现可以通过向Manticore注册名为Merger的插件在Python脚本中使用。examples/script下的basic_statemerging.py是这种状态合并使用的示例。

如果您喜欢这篇文章，请分享： Twitter LinkedIn GitHub Mastodon Hacker News