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

符号执行的温和介绍

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

代码片段和约束图

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

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

状态爆炸问题

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

状态爆炸示例

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

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

MUI功能演示

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

使用错误输入运行挑战

第一次尝试：使用find和avoid命令

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

我们可以使用find命令将此目标传达给MUI；指令以绿色突出显示。类似地，我们可以使用avoid命令告诉MUI避免失败情况。

现在，指定目标后，我们可以运行MUI来找到此crackme挑战的解决方案。

如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