在 Manticore 中符号执行 WebAssembly

随着 Manticore 0.3.3 的发布，我们自豪地宣布支持对 WebAssembly（WASM）二进制文件进行符号执行。WASM 是一种新标准化的编程语言，允许 Web 开发者在浏览器中以接近原生的性能直接运行代码。Manticore 0.3.3 能够探索 WASM 程序中所有可达状态，并推导出产生特定状态的具体输入。我们开发此功能的目标是为未来 WASM 程序的安全分析奠定坚实基础。

为什么选择 WASM？

WASM 正成为软件编写方式的重要组成部分。所有主流 Web 浏览器均支持 WASM，且它最近被接受为 Web 标准。更重要的是，它有助于弥合 Web/原生应用之间的性能差距，并通过允许开发者使用 C++ 和 Rust 等熟悉语言来简化开发流程。

一个令人兴奋的 WASM 发展是 Bytecode Alliance：这是 Mozilla 提出的提案，旨在围绕小型、经过充分验证的 WASM 纳米进程重构现代包管理，这些进程可被形式化证明没有重大安全漏洞。符号执行特别适合此类问题，因为它设计用于在所有可能条件下评估代码。然而，迄今为止，在符号执行 WebAssembly 方面尚未取得重大进展。据我们所知，Manticore 是第一个积极维护并支持 WASM 二进制的符号执行引擎。

以太坊 WASM（EWASM）

WASM 也预计对我们的以太坊智能合约分析工作产生积极影响。作为以太坊 2.0 改进的一部分，以太坊基金会计划将以太坊虚拟机（EVM）语言替换为以太坊风格的 WebAssembly（EWASM）。EWASM 看起来与常规 WASM 有些不同，但我们认为，在开发 WASM 工具方面积累的经验将使得在过渡发生时轻松升级我们现有的 EVM 工具。

在 Manticore 中使用 WASM

让我们看一个可以用符号执行解决的经典问题示例。我们将使用 Manticore 来解决一个已交叉编译到 WebAssembly 的简单 crackme。

我们从以下 C 程序开始。它从 stdin 读取一个字节，然后将其与具体值进行比较。它逐位进行比较，因此我们无法直接从源代码读取值。它还包括一个分支计数器，在每个位被检查后递增，因此返回代码将反映有多少前导位与期望值匹配。这也防止编译器将嵌套的 if 语句优化为单个比较。

图 1：执行与 stdin 字节的逐位比较的 C 程序

由于这只是一个示例，您可能可以从源代码中看出正确的输入字节是 0x58（‘X’）。让我们使用 WASMFiddle 将其编译到 WebAssembly，然后将其放入 Manticore，看看它是否能找到相同的结果。

首先，我们将导入处理 WASM 所需的 Python 模块：

图 2：Python 导入语句

由于 WASM 二进制文件在浏览器中运行，它们无法以原生二进制文件的方式访问标准库。相反，像 getchar 或 printf 这样的函数通常由 Emscripten 或 WASI 在 JavaScript 中提供。这里，我们将使用 Manticore API 提供一个最小化的符号实现：

图 3：符号 getchar 实现

尽管 C 程序期望从 getchar 获取 8 位整数，但最小的 WASM 数据类型是 32 位整数。因此，我们返回一个 32 位值，并将其约束在 0 到 256 之间。

我们还需要一个在状态终止时运行的回调，以检查是否找到了正确答案。我们将使用 Manticore 插件来完成此操作：

图 4：识别成功状态的回调

此回调检查栈顶的值（main 的返回值）是否为零，如果是，则求解此状态下所有符号的具体值。

最后，我们将所有内容整合在一起。我们创建一个新的 Manticore 实例，并为其提供 WASM 模块的名称和我们的符号 getchar 实现。我们注册状态终止回调，然后指示 Manticore 从 main 方法开始状态探索。

图 5：运行 Manticore 的 Python 语句

以下是最终脚本：

图 6：Manticore 解决方案脚本

当我们运行此脚本时，可以看到 Manticore 正确求解了输入字节：

图 7：终端输出显示 ‘X’ 返回 0

尝试一下

您现在可以通过从 PyPi 安装 0.3.3 版本来尝试 Manticore 中的 WASM 支持。WASM 支持仍处于 alpha 阶段，因此请通过在我们的 Github 存储库中提交错误报告或建议来帮助我们改进。随着可用性改进，API 可能会略有变化，但我们将确保上述示例的 Github 版本保持最新。最后要注意的一点：Manticore 的 WASM 模块目前不支持符号浮点语义，并且仅对符号内存解引用有有限支持。到目前为止，这些对我们来说还不是问题，但我们正在努力改进它们，以使 Manticore 成为最好的工具。

我们一直在开发更快、更智能的工作方式。需要帮助您的下一个项目吗？请联系我们！