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

在我暑期实习期间，我有幸参与了Manticore用户界面（MUI）项目。MUI项目旨在结合强大的符号执行库Manticore和流行的二进制分析工具Binary Ninja，为符号执行提供一个更直观和可视化的界面。

探索ELF二进制文件与MUI

符号执行的温和介绍

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

代码片段和约束图

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

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

状态爆炸的问题

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

状态爆炸示例

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

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

MUI功能与演示

为了说明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我们想要采取的路径来防止所有状态分叉。这可以通过自定义钩子和以下代码片段实现：

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13

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项目的未来。

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