符号执行可视化：Manticore与Binary Ninja的完美融合

MUI：使用Manticore和Binary Ninja实现符号执行可视化

符号执行的温和介绍

在进行漏洞研究和逆向工程时，研究人员通常希望彻底测试软件并探索所有可能状态。符号执行正是解决这一需求的方法之一。如下代码片段所示，程序执行可以进入if分支或else分支。

代码片段和约束图

使用具体输入测试代码（例如x=4）时，执行过程中只会到达两种状态之一。这意味着需要多次运行程序才能完全探索状态空间。然而，如果我们将x视为符号值（类似于数学中的变量概念），就可以同时探索两种状态，只需在探索过程的每个点跟踪符号变量的约束。

具体在这个例子中，if-else语句将创建两个状态：一个带有约束x<5（探索①），另一个带有x≥5（探索②）。这就是符号执行背后的核心概念，可以帮助我们确定给定代码段是否可达以及需要什么输入。

状态爆炸问题

然而，符号执行技术并非没有缺点，最显著的是状态爆炸问题。当程序中存在多个条件分支和循环时，需要探索的状态数量可能呈指数级增长，很快变得不可行。以下示例说明了这一点：仅三次循环迭代，代码片段就会产生八个需要探索的状态，随着迭代次数增加，这个数字会迅速爆炸。

状态爆炸示例

大多数符号执行库缺乏可视化状态探索过程的方法，这使得状态爆炸问题更加严重。这意味着通常很难精确定位状态爆炸发生的位置，更不用说开始修复它们了。

MUI功能演示

MUI项目旨在通过提供交互式用户界面来解决这些问题，更好地可视化符号执行中的状态探索过程，并保持人工参与。具体来说，MUI是一个Binary Ninja插件，具有自定义Qt小部件，提供可视化直观界面来与Manticore（Trail of Bits开发的开源符号执行库）交互。

为了演示MUI的一些功能，让我们尝试解决Manticore存储库中的一个简单破解挑战。目标很明确：我们需要确定该程序的正确输入。

使用错误输入运行挑战

首次尝试：使用find和avoid命令

在Binary Ninja中打开ELF二进制文件，我们可以快速发现main函数中的两个puts调用。这两个函数调用分别用于成功和失败情况。现在，我们的目标可以重新表述为：找到使代码执行到达成功案例的输入。

我们可以使用find命令向MUI传达这个目标（指令以绿色高亮显示）。同样，我们可以使用avoid命令告诉MUI避免失败情况。

指定目标后，我们可以运行MUI来找到这个破解挑战的解决方案。如gif所示，我们可以在Binary Ninja UI中使用Manticore探索挑战的状态空间，并获得解决方案"coldlikeminisodas"。将这个答案反馈给程序验证了我们确实解决了挑战。

使用正确输入运行程序

将注意力转回MUI，我们可以使用自定义的State List小部件查看MUI如何获得这个解决方案以及它探索的所有状态。列表中的状态34表示到达成功案例的最终状态。

运行中的State List小部件

为了进一步可视化各状态之间的关系，我们可以使用Graph View小部件。该小部件显示包含所有状态的来源树。双击状态节点将带我们到状态分叉或终止前的最后一条指令。使用tab快捷键，树图可以展开显示其他终止状态。

运行中的Graph View小部件

第二种解决方案：自定义钩子

除了我们已经演示的所有酷炫功能外，MUI还有更多技巧。让我们使用不同的方法再次解决这个挑战。

再次显示main函数体以便参考

如果我们花些时间理解反编译代码，可以看到用户输入与正确答案逐个字符比较，当输入字符与正确答案不匹配时，我们会看到失败消息。有了这个知识，我们可以通过明确告诉MUI我们想要采取的路径来防止所有状态分叉。这可以通过自定义钩子和以下代码片段实现：

global bv,m,addr
def hook(state):
   flag_byte = state.cpu.AL - 0xa
 
   with m.locked_context() as context:
       if 'solution' in context:
           context["solution"] += chr(flag_byte)
       else:
           context["solution"] = chr(flag_byte)
       print(f'flag: {context["solution"]}')
 
   state.cpu.RIP = 0x400a51
m.hook(addr)(hook)

这里的自定义钩子功能是一种后备方案，让您无需在不同环境中编写完整脚本即可获得Manticore API的全部功能。这使得研究人员可以在Binary Ninja内部完成所有工作，减少所需的上下文切换量。

EVM支持如何？

为了弥补Binary Ninja缺乏内置EVM支持的问题，MUI利用了Trail of Bits开发的其他几个开源工具。智能合约使用crytic-compile（智能合约构建系统的抽象层）进行编译，反汇编代码和CFG的生成和可视化由ethersplay（EVM反汇编器）处理。

有了这些工具，MUI中的EVM功能集现在与默认的Manticore CLI相当，并且更多功能正在积极开发中。但即使功能相同，MUI在可用性和可发现性方面确实超越了CLI工具。用户现在可以看到所有可用的Manticore运行选项，并使用动态生成的最新UI面板选择所需选项，而不需要查阅文档来找到正确的命令行参数。此外，与Binary Ninja的紧密集成还意味着这些选项可以持久保存在Binary Ninja数据库（BNDB）项目文件中，提供更多便利。

EVM运行对话框

结论

我为在实习期间能够通过MUI项目取得的成就感到非常自豪。MUI已经可用于许多用例，帮助研究人员改进工作流程。我们已经实现了这个项目的目标：为符号执行工作提供直观的可视化界面。

这次实习对我来说是一个很好的学习机会。通过这次实习，我对符号执行的工作原理有了更深入的理解，并学习了许多不同的主题，从项目规划和文档到Qt UI开发，从多线程应用程序到Git工作流程等等。

我要感谢我的导师Eric Kilmer和Sonya Schriner在实习期间给予的巨大帮助。他们在我需要时提供指导，同时在MUI开发过程中给予我足够的自由去探索和创新。没有他们，我的实习经历将会完全不同。我非常感谢在Trail of Bits的这次实习机会，迫不及待想看到MUI项目的未来发展。