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语言）。通过基于p-code，我们能够利用Ghidra出色的C++库sleigh进行反汇编和提升二进制代码，该库已经支持非常广泛的架构。更妙的是：Maat使用独立的sleigh版本，因此您无需安装Ghidra即可使用Maat。

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

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

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

性能驱动

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

Maat的核心完全用C++编写，这是许多开发人员选择用于优化和性能的语言。我们尽最大努力编写高效代码，同时不牺牲代码可读性或限制功能。Maat的运行时性能可能因符号计算量、对SMT求解器的调用以及用户提供的分析回调而有很大差异；但我们早期的实验测量结果相当有希望，在典型笔记本电脑（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讨论以提问和反馈——让我们知道您的想法！