在Manticore中对WebAssembly进行符号执行

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

为什么选择WASM？

WASM正在成为软件开发方式的重要组成部分。所有主流Web浏览器均已支持WASM，且它最近被接纳为Web标准。更重要的是，WASM有助于弥合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成为最好的工具。

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

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