Maat：让符号执行触手可及

我们发布了Maat，一个跨架构、多用途且用户友好的符号执行框架。它提供常见的符号执行功能，如动态符号执行（DSE）、污点分析、二进制插桩、环境模拟和约束求解。

Maat易于使用，基于流行的Ghidra中间表示（IR）语言p-code，优先考虑运行时性能，并提供C++和Python API。我们的目标是创建一个强大而灵活的框架，既可供经验丰富的安全工程师使用，也适合想要入门符号执行的初学者。

虽然我们的Manticore工具提供了高级接口来符号化探索二进制文件，但Maat是一个较低级的符号执行工具包，可以轻松集成到其他项目中或用于构建独立分析工具。有关直接示例，请阅读我们的教程，了解如何使用Maat解决基本的逆向工程挑战。

用户友好、灵活的API

Maat具有C++编程API，可用于低级或性能关键项目。它还提供Python绑定，允许用户轻松快速地编写可移植的分析脚本。

API设计旨在给予用户尽可能多的控制。其类似调试器的接口可用于启动、暂停甚至回滚符号执行过程。用户可以通过任意回调函数插桩目标代码，这些函数由特定事件（如寄存器和内存访问以及分支操作）触发，编写自定义动态分析，在运行时修改程序状态，指定进程应停止的特定状态，甚至对二进制文件的一部分执行路径探索。

最后但同样重要的是，Maat的执行引擎具有可自定义的设置，允许用户控制其处理符号数据的基本行为。它包括处理符号指针、保存状态约束和进行符号简化等策略。默认设置优先考虑正确性而非性能，并适合最通用的用例，但高级用户可以根据自己的用例定制引擎，并绕过默认设置的某些限制。

丰富的架构支持

通过Maat，我们希望将符号执行功能带给尽可能多的架构。为此，我们将Maat的符号执行引擎基于p-code，即Ghidra使用的IR语言。通过将Maat基于p-code，我们能够利用Ghidra出色的C++库sleigh进行反汇编和提升二进制代码，该库已经支持非常广泛的架构。最重要的是：Maat使用独立的sleigh版本，因此您无需安装Ghidra即可使用Maat。

使用sleigh为Maat带来三大优势：

• 能够在Ghidra支持的任何架构上执行符号执行
• 依赖一个非常流行、开源且积极支持的反汇编和提升库的可靠性
• 可以使用sleigh规范语言添加其他架构的可能性

虽然Maat目前仅在X86和X64上进行了测试，但我们计划很快添加其他架构的接口。我们对在Maat中引入对现有工具尚未支持的异架构支持的前景特别兴奋；sleigh无与伦比的架构支持使这成为可能。另一个令人兴奋的机会是使用Maat在虚拟机字节码（如Java、Dalvik和Ethereum）上执行符号执行。

性能驱动

将符号执行扩展到实际应用程序可能是一项挑战。对于通用的、仅二进制的符号执行工具，显著的运行时开销是提升和执行IR所固有的；这 simply 无法避免。话虽如此，在任何合理的日常工作中，在几分钟而不是几小时内运行的脚本可以产生巨大差异。因此，我们在Maat的设计和实现中投入了 care，使其在产生有用结果的同时尽可能快地运行。

Maat的核心完全用C++编写，这是许多开发者选择进行优化和性能的语言。我们尽最大努力编写高效代码，而不牺牲代码可读性或限制功能。Maat的运行时性能可能因符号计算量、对SMT求解器的调用以及用户提供的分析回调而 vary widely；但我们早期的实验测量结果相当 promising，在典型笔记本电脑（2.3 GHz Intel Core i7，32 GB RAM）上每秒符号执行100,000到300,000条指令。

我们还计划添加并公开内省功能，以允许用户识别运行时瓶颈。这不仅有助于最终用户针对其特定用例优化分析脚本，还使我们能够对Maat的核心组件进行更根本的改进。

如何开始

只需使用python3 -m pip install pymaat安装Maat！查看我们的系列教程以获取使用指南。虽然本系列提供了一些基本教程，但我们的长期目标是提供一个更全面的系列，涵盖框架的基础知识、高级应用和复杂功能。

好奇的读者可以在GitHub上查看Maat的源代码！除了教程外，您还可以在Maat的网站上找到安装说明和C++/Python API文档。

最后，加入我们的GitHub讨论以提问和反馈——让我们知道您的想法！

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