Manticore中的WebAssembly符号执行

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

为什么选择WASM？

WASM正在成为软件开发方式的重要组成部分。所有主流Web浏览器都支持它，并且最近已被接受为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程序

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


#include <stdio.h>
#include <stdlib.h>

int main() {
    int branch_counter = 0;
    char input = getchar();
    
    if ((input & 0x80) == 0x80) branch_counter++;
    if ((input & 0x40) == 0x40) branch_counter++;
    if ((input & 0x20) == 0x20) branch_counter++;
    if ((input & 0x10) == 0x10) branch_counter++;
    if ((input & 0x08) == 0x08) branch_counter++;
    if ((input & 0x04) == 0x04) branch_counter++;
    if ((input & 0x02) == 0x02) branch_counter++;
    if ((input & 0x01) == 0x01) branch_counter++;
    
    return branch_counter;
}

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

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

图2：Python导入语句

1

from manticore.wasm import ManticoreWASM

由于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之间
    value = state.new_symbolic_value(32, "getchar_input")
    state.constrain(value >= 0)
    state.constrain(value < 256)
    return value

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

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

1
2
3
4
5
6
7
8


def did_finish(state):
    # 检查栈顶的值（main的返回值）是否为零
    return_val = state.stack.peek()
    if return_val == 0:
        print("Found successful input!")
        # 求解此状态下所有符号的具体值
        concrete_values = state.solve()
        print(f"Concrete input: {concrete_values}")

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

图5：运行Manticore的Python语句

1
2
3
4


m = ManticoreWASM('crackme.wasm')
m.set_symbolic_getchar(symbolic_getchar)
m.set_termination_callback(did_finish)
m.run(start='main')

这是完整的脚本：

图6：Manticore解决方案脚本

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


from manticore.wasm import ManticoreWASM

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

def did_finish(state):
    return_val = state.stack.peek()
    if return_val == 0:
        print("Found successful input!")
        concrete_values = state.solve()
        print(f"Concrete input: {concrete_values}")

m = ManticoreWASM('crackme.wasm')
m.set_symbolic_getchar(symbolic_getchar)
m.set_termination_callback(did_finish)
m.run(start='main')

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

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

1
2


Found successful input!
Concrete input: {'getchar_input': 88}

尝试使用

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

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