如何改造 ManticoreUI - Trail of Bits 博客

在我于 Trail of Bits 实习期间，我探索了符号执行在发现原生应用程序漏洞方面的有效性，范围从 CTF 挑战到流行的开源库（如图像解析器），重点在于寻找增强 ManticoreUI 的方法。这是一个强大的工具，提高了符号执行和漏洞发现的可访问性，但其可用性和效率仍有很大的改进空间。最终，我实现了新的 ManticoreUI 功能，通过模拟减少分析时间，改进了共享库支持，并允许从 GDB 引导符号状态以绕过复杂的程序初始化。借助这些新功能，我发现并报告了 DICOM 工具包（DCTMK）中的一个漏洞，这是一套广泛部署的用于医学成像的库！

ManticoreUI 的现状

Manticore 是一个符号执行引擎，它使用符号数据（而非具体数据）模拟应用程序。这使得 Manticore 能够测试其目标的所有可能执行路径。ManticoreUI（MUI）是 Binary Ninja 的图形用户界面插件，通过有用的图形元素以更简单的方式向用户展示 Manticore 的功能。其设计允许用户享受符号执行的好处，而无需担心 Manticore API 的细节。

GUI 示例。

我的目标之一是改进 MUI 在发现漏洞方面的用户体验。我花了一些时间在 CTF 挑战、人工创建的易受攻击代码样本以及一些小型真实目标上使用 MUI。由此，我确定了三个改进方向：

• 我意识到许多非默认功能对新或不熟练的 Manticore 用户来说并不明显。这些功能有时在代码中实现，但未在文档中涵盖。
• 我还注意到，真实世界的软件目标比 CTF 挑战等小样本更具挑战性。CTF 挑战往往是小型命令行应用程序，通常从标准输入接收输入。然而，现实世界中有许多应用程序类型，包括网络服务、守护进程和库。MUI 的用户体验因类型而异。
• 最后，当测试处理大型输入的软件时，如具有大迭代循环的格式解析器或复杂的 C++ 二进制文件，MUI 的模拟速度明显慢于真实 CPU 的执行速度。

通过 ManticoreUI 暴露有用功能

为了解决第一个改进领域，我让 MUI 的两个有用功能——函数模型和全局钩子——对用户更加明显。

函数模型

函数模型是常见库函数的 Python 重新实现，具有对 Manticore 符号执行引擎的意识。这些模型在符号执行期间覆盖实际的库函数。这提高了性能，因为 Manticore 不必单独模拟每个原生指令。

ManticoreUI 现在在有库函数可以被现有函数模型实现替代时提示，如下所示：

启动时显示具有函数模型实现的函数

“添加函数模型”命令允许用户在函数地址添加自定义钩子，以使用函数模型而非原生代码。

函数模型选择弹出窗口

全局钩子

全局钩子是另一个不太明显的功能。这些是自定义钩子，对每个执行的指令触发。它们可用于实现用户定义的跟踪功能，如跟踪发生的每个系统调用（类似于 strace）。或者，它们可以帮助执行不绑定到特定指令的检查（例如，当 RAX 寄存器值为 0xdeadbeef 时结束 Manticore 运行的全局钩子）。它们可以使用“添加/编辑全局钩子”命令添加。

全局钩子管理弹出窗口

改进漏洞发现工作流

为了解决第二和第三个改进领域，我实现了新的 MUI 功能，以促进漏洞发现过程。emulate_until 功能提高了 MUI 的性能，而共享库支持和 GDB 状态转储改进了 MUI 在复杂目标中的可用性。这些功能在下面更详细地描述。

emulate_until

emulate_until 功能是 MUI 的一个额外解决选项。将此值设置为地址将使 Manticore 使用 Unicorn 模拟器具体模拟目标二进制文件，直到达到指定地址。Unicorn 模拟器比 Manticore 自己的模拟 CPU 快得多，这大大提高了执行速度。

Manticore 运行选项中的 Emulate_until 字段

我注意到这个功能对 C++ 二进制文件非常有用，它们在初始化期间执行更多指令。当我们在 Ubuntu 20.04 机器上符号执行一个简单的基准测试（使用 hello world C++ 二进制文件）时，我们观察到以下运行时间：

显然，使用带有 emulate_until 选项的 Unicorn 模拟对即使最简单的 C++ 二进制文件也能带来显著的性能好处。

共享库支持

在漏洞发现中，我们通常测试应用程序的底层库而非完整应用程序本身。此类工作流通常涉及一个简单的 harness 二进制文件，它加载库并调用要测试的库函数。由于 MUI 仅支持在单个二进制文件中加载和设置钩子，使用带有共享库的 harness 二进制文件对 MUI 来说是一个麻烦的工作流。

有了这个新功能，用户可以单独在 MUI 中加载共享库并设置所有必要的钩子。然后，他们可以在 MUI 中加载 harness 二进制文件并链接共享库的 Binary Ninja 项目文件。在执行期间，共享库项目中设置的所有钩子将被解析并相应添加到运行时。

虽然尚未实现，但这个功能非常适合 Ghidra MUI 插件。Binary Ninja 项目仅包含单个二进制文件，而 Ghidra 项目可以包含多个二进制文件。这个功能将 enable 在 Ghidra 中进行漏洞发现的更方便的工作流。

GDB 状态转储

在用不同目标测试 MUI 时，我遇到了各种问题，包括不支持的 system calls、未实现的指令以及通过 MUI/Manticore 交互过于复杂的应用程序。我还经常遇到情况，其中符号测试整个应用程序会导致状态爆炸（即，太多分叉状态）。

这使我开始探索限制 Manticore 执行引擎使用的想法。例如，与其尝试从应用程序开始符号执行，不如从感兴趣的函数开始执行？当在函数的小子集中寻找漏洞时，这仍然非常有用，并且通过限制 Manticore 必须符号执行的代码量来减少模拟问题。

我为 GEF 开发了一个 GDB 插件，允许用户将调试器的状态转储为 Manticore 状态对象。这存储在系统上的文件中，以后可以加载到 MUI/Manticore 中，用作执行的初始状态。这个插件极大地增加了 MUI 的可能性！

例如，通常难以在 Manticore 中完全模拟的网络服务现在可以正常运行并附加到调试器。用户然后可以从选择的断点转储状态，并将该状态加载到 MUI 中以开始符号执行。这个过程允许 MUI 用于各种复杂目标。

这种方法与其他两种技术有相似之处：欠约束符号执行和具体符号执行。然而，它无疑是三种方法中最“约束”的。这不一定是坏事，但用户必须行使判断以确定哪种技术最适合他们的用例。使用来自 GDB 的状态的一个关键弱点是，注入符号值需要更深入地理解当前程序状态。例如，如果您因为未分析程序中早期的某些 if-else 检查而用完全无约束的符号值替换变量值，Manticore 可能会给出不准确的结果。

借助 MUI 发现漏洞

有了 MUI 在我的武器库中，我决心在使用符号执行的力量时发现一个漏洞。我的目标不是完全通过符号执行发现漏洞。相反，我希望使用 MUI/Manticore 作为预言机，可以告知我可达性和执行约束，补充传统的漏洞狩猎方法，如源代码审计。

我目标的代码库是 DICOM 工具包（DCTMK）。DCMTK 是一套用于处理 DICOM 标准的库和实用程序。因为 DICOM 文件通常用于医学成像，DCMTK 用于处理医疗产品或数据的软件中。

用 Manticore 快速评估可达性

我开始检查源代码，重点关注某些漏洞接收器，如内存访问或内存分配。当我发现可能导致漏洞的接收器时，我然后依赖 MUI 来确定目标代码是否可达，以及是否可以创建内存损坏的条件。

在阅读解析 BMP 图像的代码时，我注意到了以下漏洞接收器：

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21

// dcmdata\libi2d\i2dbmps.cc:330 
OFCondition I2DBmpSource::readBitmapData( 
  const Uint16 width, 
  const Uint16 height, 
  const Uint16 bpp, 
  const OFBool is TopDown, 
  const OFBool isMonochrome, 
  const Uint16 colors, 
  const Uint32* palette,
  char * & pixData, 
  Uint32& length) 
{
  …
  Uint8 *row_data; 
  …
  Uint16 samplesPerPixel = isMonochrome ? 1 : 3; 
  …
  length = width * height * samplesPerPixel;     // [1]
  …
  pixData = new char [length];                   // [2]
}

在 [1] 处，我们看到 length 变量被设置为 width、height 和 samplesPerPixel 的乘积。然后这个 length 在 [2] 处用作分配 char 缓冲区的大小。这是整数溢出漏洞的常见接收器。如果 width、height 和 samplesPerPixel 的乘积足够无界以溢出 length 的容量，它可能使 [2] 处的分配过小。

由于 width 和 height 是用户控制的，我想确定用户是否可以提供任何值的组合导致整数溢出。这就是 MUI 发挥作用的地方！我使用 MUI 作为预言机来确定，给定 width、height 和 samplesPerPixel 的边界，是否可能存在 length 的整数溢出。

快速查看代码显示，samplesPerPixel 对彩色图像最大设置为 3。此外，width 和 height 被限制在无符号 16 位整数的范围内：

1
2
3
4
5

if (tmp_height <= 0 || tmp_height > OFstatic_cast (Sint 32, UINT16_MAX)) 
   return makeOFCondition (OFM_dcmdata, 18, OF_error, "Unsupported BMP file - height too large or zero"); 
 ...
 if (tmp_width <= 0 || tmp_width > OFstatic_cast (Sint 32, UINT16_MAX)) 
   return makeOFCondition (OFM_dcmdata, 18, OF_error, "Unsupported BMP file - width too large or zero"); 

使用 GDB 状态转储插件，我在 I2DBitmapSource::readBitmapData 函数上设置了一个断点，并用一个简单的蜗牛 BMP 图像达到了断点。通过将调试环境转储到 Manticore 状态，我可以然后将状态加载到 MUI 中。以下视频演示了这个过程：

状态加载到 MUI 后，我可以将 width 和 height 设置为符号值。使用自定义钩子，我强制 Manticore 解决发生整数溢出的状态。Manticore 将使用 sat-solver 来确定这样的状态是否可能，允许我们彻底验证这个漏洞的有效性。

运行后，我得到了以下值：

显示已解决 width 和 height 的结果屏幕

这意味着，具有上述图像中指定 width 和 height 的精心制作的 BMP 图像可以创建 length 过小的情况，导致分配不足。在 GDB 中使用此漏洞利用图像运行二进制文件立即导致崩溃和成功的漏洞发现！

补丁

在通知供应商几小时内，他们引入了补丁来修复漏洞。这是一个非常愉快的安全响应！

成功的改造

我对在这个实习期间取得的进展非常满意，我认为改进的分析性能、共享库支持以及用 GDB 绕过复杂应用程序初始化已经将 ManticoreUI 塑造成一个更好的工具，用于辅助漏洞发现，很好地补充了传统的漏洞狩猎方法。

通过这个实习，我学到了很多关于符号执行在安全领域应用的知识，并且我很兴奋看到它将如何继续发展。除了符号执行，我还有机会通过处理 ManticoreUI 的不同组件来提高我的软件开发技能。

我非常感谢我的导师 Eric Kilmer 在整个实习期间提供的帮助。他为我提供了项目方向的指导，并对改进我贡献的代码和想法提供了宝贵的反馈。这个实习对我来说无疑是一个难忘且富有成果的经历。

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

页面内容 ManticoreUI 的现状 通过 ManticoreUI 暴露有用功能 函数模型 全局钩子 改进漏洞发现工作流 emulate_until 共享库支持 GDB 状态转储 借助 MUI 发现漏洞 用 Manticore 快速评估可达性 补丁 成功的改造 最近帖子 我们构建了 MCP 一直需要的安全层 利用废弃硬件中的零日漏洞 Inside EthCC[8]：成为智能合约审计员 用 Vendetect 大规模检测代码复制 构建安全消息传递很难：对 Bitchat 安全辩论的 nuanced 看法 © 2025 Trail of Bits。 用 Hugo 和 Mainroad 主题生成。