在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程序

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14

#include <stdio.h>
int main() {
    char input = getchar();
    int counter = 0;
    if ((input >> 7) == 0) counter++;
    if ((input >> 6) == 1) counter++;
    if ((input >> 5) == 0) counter++;
    if ((input >> 4) == 1) counter++;
    if ((input >> 3) == 1) counter++;
    if ((input >> 2) == 0) counter++;
    if ((input >> 1) == 0) counter++;
    if ((input >> 0) == 0) counter++;
    return counter;
}

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

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

图2：Python导入语句

1
2

from manticore.wasm import ManticoreWASM
import sys

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

图3：符号getchar实现

1
2
3
4
5
6
7

def symbolic_getchar(state):
    # 虽然C程序期望从getchar获得8位整数，但最小的WASM数据类型是32位整数
    # 因此，我们返回一个32位值并将其约束在0到256之间
    val = state.new_symbolic_value(32, "getchar_input")
    state.constrain(val >= 0)
    state.constrain(val < 256)
    return val

我们还需要一个在状态终止时运行并检查是否找到正确答案的回调。我们将使用Manticore插件来实现这一点：

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

1
2
3
4
5
6
7
8

def did_terminate(state):
    # 检查栈顶的值（main的返回值）是否为零
    # 如果是，则求解此状态下所有符号的具体值
    return_val = state.stack.peek()
    if return_val == 0:
        print("Found solution!")
        for symbol in state.symbols:
            print(f"{symbol}: {state.solve(symbol)}")

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

图5：运行Manticore的Python语句

1
2
3

m = ManticoreWASM('crackme.wasm', env={'getchar': symbolic_getchar})
m.register_plugin(did_terminate)
m.run()

以下是完整的脚本：

图6：Manticore解决方案脚本

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18

from manticore.wasm import ManticoreWASM

def symbolic_getchar(state):
    val = state.new_symbolic_value(32, "getchar_input")
    state.constrain(val >= 0)
    state.constrain(val < 256)
    return val

def did_terminate(state):
    return_val = state.stack.peek()
    if return_val == 0:
        print("Found solution!")
        for symbol in state.symbols:
            print(f"{symbol}: {state.solve(symbol)}")

m = ManticoreWASM('crackme.wasm', env={'getchar': symbolic_getchar})
m.register_plugin(did_terminate)
m.run()

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

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

1
2

Found solution!
getchar_input: 88

尝试使用

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

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