如何为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++二进制文件的基准测试时，我们观察到以下运行时间：

选项	总持续时间/秒
默认	311秒
emulate_until到main	12秒

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

共享库支持

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

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

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

GDB状态转储

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

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

我为GEF开发了一个GDB插件，允许用户将调试器的状态转储为Manticore状态对象。这存储在系统上的文件中，以后可以加载到MUI/Manticore中用作执行的初始状态。这个插件 dramatically 增加了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 isTopDown, 
  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 (Sint32, 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 (Sint32, 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塑造成一个更好的工具，用于辅助漏洞发现，很好地补充了传统的漏洞狩猎方法。

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

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

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

ManticoreUI 图形化符号执行工具的优化与漏洞挖掘实践

本文详细介绍如何通过增强ManticoreUI的仿真性能、共享库支持和GDB状态导入功能，提升符号执行效率，并成功挖掘DICOM工具包中的整数溢出漏洞。