Manticore 0.3.0发布 - The Trail of Bits博客

Eric Hennenfent
2019年6月7日
dynamic-analysis, manticore, research-practice

本周，Manticore跃升至0.3.0版本。我们的符号执行引擎进展包括：通过不关心的具体执行进行“快进”、支持为AArch64静态编译的Linux二进制文件，以及选择性求解有趣测试用例的接口。过去一个季度，我们一直在努力开发这些及其他功能，并兴奋地分享我们的成果。

执行器重构

Felipe Manzano完成了Manticore状态机的一次重大重构。现在它使用多处理模块，这可能使未来实现分布式符号执行更加容易。您可以在拉取请求描述中阅读更多关于状态机的细节。请注意，它确实对API引入了一些小变化，其中最重要的是：

• 您现在必须显式调用finalize方法才能在运行后转储测试用例。这意味着您可以在决定是否投入时间求解测试用例之前检查状态。
• will_start_run回调已重命名为will_run
• 求解器单例现在必须显式访问为Z3Solver.instance()

Unicorn预加载

Manticore在Python中模拟原生指令，而Python并不以速度著称。指令吞吐量仅是具体CPU上预期的一小部分，当您关心的代码深埋在二进制文件中时，这可能非常不幸。您可能会花费几分钟等待Manticore执行复杂的初始化例程，然后才能到达任何感兴趣的内容。

为了处理这种情况，我们添加了一个Unicorn模拟器插件，允许Manticore通过您不关心的具体执行进行“快进”。Unicorn是一个快速的原生CPU模拟器，利用QEMU的JIT引擎以获得更好的性能。通过用Unicorn替换Manticore的执行器来处理不重要的初始化例程，我们遇到了高达50倍的速度提升。有关如何调用Unicorn模拟器的示例，请参阅拉取请求。

AArch64支持

在过去的四个月中，Nikita Karetnikov添加了对为AArch64静态编译的Linux二进制文件的支持。由于这是一个全新的架构，我们保留了许多调试组件以帮助我们诊断问题，这一决定可能使其比其他架构稍慢。随着ARMv8 CPU在从嵌入式开发板到服务器农场的平台中日益普及，我们期待收到关于这个新架构的反馈。

系统调用审计

为了提供准确的符号执行环境，Manticore需要所有Linux系统调用的符号模型。以前，我们仅实现了最常见系统调用的一个子集，Manticore在遇到未实现的调用时会立即抛出异常。这足以执行许多二进制文件，但还有改进的空间。

随着0.3.0版本的发布，我们添加了十几个新的系统调用，并为未实现的调用添加了“存根”。现在，当遇到未实现的调用时，Manticore不会抛出异常，而是尝试假装调用成功完成。程序之后可能仍然会中断，但我们发现这种技术通常“足够好”来分析各种有问题的二进制文件。只需确保密切关注“未实现的系统调用”警告消息，因为如果Manticore忽略了重要的系统调用，进一步的分析可能不可靠！

符号EVM测试

Manticore提供的重要保证之一是，当它使用符号执行交易时，结果适用于该符号的所有可能值。为了使其可信，每个指令的符号实现需要正确。这就是为什么我们扩展了持续集成管道，以在每个新提交上自动针对Ethereum VM测试的Frontier版本运行Manticore。这将确保在进一步的开发过程中，您始终可以依赖Manticore正确推理您的代码。

Black

我们相信干净的代码，这就是为什么我们通过black自动格式化工具运行了Manticore。Black根据对pycodestyle约定的相当严格的阅读确定性地格式化您的代码，以便您可以专注于内容而不是格式。从现在开始，您应该在提交拉取请求之前在分支上运行black -t py36 -l 100 .。

下一步是什么？

我们相信安全工具只有在人们实际使用时才有益，因此我们希望使Manticore更容易为每个人使用。在接下来的几个月里，我们对Manticore的可用性有大计划，包括改进我们的文档、更新我们的示例存储库以及进行正式的可用性研究。不过，不要认为我们会让代码停滞不前！我们的下一个版本应该包括对crytic-compile的支持，使在Manticore中分析智能合约更加容易。我们将继续努力改进性能并最终支持EVM Constantinople。

您可以从我们的GitHub、通过PyPI或作为预构建的Docker容器下载Manticore 0.3.0。

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

页面内容
执行器重构
Unicorn预加载
AArch64支持
系统调用审计
符号EVM测试
Black
下一步是什么？
近期文章
我们构建了MCP一直需要的安全层
在废弃硬件中利用零日漏洞
Inside EthCC[8]：成为智能合约审计员
使用Vendetect大规模检测代码复制
构建安全消息传递很难：对Bitchat安全辩论的细致看法
© 2025 Trail of Bits。
使用Hugo和Mainroad主题生成。