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

页面内容

两种接口，多种用例
早期应用
轻松入门
告诉我们您的想法！

近期文章

使用Deptective调查您的依赖项
系好安全带，Buttercup，AIxCC的评分回合正在进行中！
将您的智能合约成熟度提升至私钥风险之外
Go解析器中意外的安全陷阱
我们审查首批DKLs23库的收获
Silence Laboratories的23个库