Manticore：面向人类的符号执行工具

本周初，我们开源了一款我们依赖的动态二进制分析工具：Manticore！Manticore帮助我们快速利用符号执行、污点分析和插桩技术来分析二进制文件。Manticore的部分功能支撑了我们在网络大挑战赛（Cyber Grand Challenge）中的符号执行能力。作为开源工具，我们希望其他人也能在自己的项目中利用这些能力。

在构建Manticore时，我们优先考虑了简单性和可用性。我们使用了最少的外部依赖，并且我们的API对于任何有漏洞利用或逆向工程背景的人来说都应该看起来很熟悉。如果您以前从未使用过这样的工具，请尝试一下Manticore。

两种接口，多种用例

Manticore附带了一个易于使用的命令行工具，可以快速生成带有符号执行的新程序“测试用例”（或样本输入）。每个测试用例在运行程序时都会产生一个独特的结果，比如正常进程退出或崩溃（例如，无效的程序计数器、无效的内存读/写）。

命令行工具满足了一些用例，但实际使用需要更大的灵活性。这就是为什么我们创建了一个Python API，用于自定义分析和应用特定的优化。Manticore的表达性强且可编写脚本的Python API可以帮助您回答以下问题：

在执行点X，变量Y是否可能为指定值？
程序在运行时能否到达这段代码？
什么程序输入会导致执行这段代码？
用户输入是否曾被用作这个libc函数的参数？
程序执行这个函数多少次？
如果给定这个输入，程序执行多少条指令？

在我们的第一个版本中，API提供了扩展核心分析引擎的功能。除了测试用例生成，Manticore API还可以：

放弃无关状态
在任意执行点运行自定义分析函数
具体化符号内存
内省和修改模拟机器状态

早期应用

Manticore是我们用于二进制分析研究的主要工具之一。我们使用了一个早期版本作为我们在网络大挑战赛中符号执行漏洞挖掘的基础。我们正在使用它为DARPA LADS构建一个自定义程序分析器。

在发布前的一个月，我们向社区征集了简单的用例想法，以展示Manticore的功能。以下是我们最喜欢的一些：

Eric Hennenfent解决了一个简单的逆向工程挑战。他提出了两种解决方案：一种使用二进制插桩，另一种使用符号执行。
Yan和Mark用一个受污染的符号值替换了一个变量，以确定用户输入可以影响哪些特定比较。
Josselin Feist仅使用Manticore API生成了一个漏洞利用。他插桩了一个二进制文件以找到崩溃，然后使用符号执行确定调用任意函数的约束。
Cory Duplantis解决了Google CTF 2016的一个逆向工程挑战。他的脚本是一个很好的例子，展示了用Manticore解决许多CTF挑战是多么直接。

最后，向Murmus致敬，他在我们开源后仅4小时就制作了一个Manticore的视频评测！

轻松上手

使用其他工具，您可能需要花时间研究它们的内部结构。而使用Manticore，您有一个编写良好的接口和易于理解的代码库。所以，直接跳进去，尽快完成一些有用的工作。

抓取一个Ubuntu 16.04虚拟机，然后：

1
2
3
4
5
6
7


# 安装系统依赖
sudo apt-get update && sudo apt-get install z3 python-pip -y
python -m pip install -U pip

# 安装manticore及其依赖
git clone https://github.com/trailofbits/manticore.git && cd manticore
sudo pip install --no-binary capstone .

图1：安装Manticore及其依赖

您已经安装了Manticore CLI和API。我们在源代码库中包含了一些示例。让我们先尝试CLI：

1
2
3
4
5
6
7
8


# 构建示例
cd examples/linux
make

# 使用Manticore CLI发现独特的测试用例
manticore basic
cat mcore_*/*1.stdin | ./basic
cat mcore_*/*2.stdin | ./basic

图2：构建和运行示例

“Basic”是一个玩具示例，它读取用户输入并打印两个语句之一。Manticore使用符号执行探索了basic并发现了两个独特的输入。它将发现的样本输入放入“stdin”文件中，您可以将其管道传输到二进制文件。接下来，我们将使用API：

1
2
3


# 使用Manticore API计算执行的指令数
cd ../script
python count_instructions.py ../linux/helloworld

图3：使用Manticore API计算指令数

count_instructions.py脚本使用Manticore API插桩helloworld二进制文件，并计算其执行的指令数。

告诉我们您的想法！

如果您对逆向工程、二进制漏洞利用感兴趣，或者只是想了解CPU模拟器和符号执行，我们鼓励您尝试一下，并加入我们的Slack上的#manticore频道进行讨论和反馈。在那里见！

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