宣布 Manticore 0.3.0
本周，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
页面内容 最近的帖子 使用 Deptective 调查您的依赖项 系好安全带，Buttercup，AIxCC 的评分回合正在进行中！ 使您的智能合约超越私钥风险 Go 解析器中意外的安全陷阱 我们审查首批 DKLs23 库之一的经验 来自 Silence Laboratories 的库 © 2025 Trail of Bits。 使用 Hugo 和 Mainroad 主题生成。