G.O.S.S.I.P 阅读推荐 2022-09-02

如何安全高效地执行不受信任的第三方代码，一直是安全研究领域中被广泛关注的问题之一。随着云计算、智能合约等技术的发展，这一问题受到了更多人的重视。今年USENIX Security的获奖论文[Distinguished Paper Award Winner and Second Prize Winner (tie) of the 2022 Internet Defense Prize]之一的Provably-Safe Multilingual Software Sandboxing using WebAssembly，针对WebAssembly的沙盒提出了新的（可证明安全的）解决方案。

在本文中，作者以WebAssembly的安全性和多语言特性为基础，实现了两种可证明安全性的软件沙箱化方法。通过将第三方代码编译成Wasm，再通过作者设计的编译器编译成沙箱代码，可以在保证运行效率的情况下，提供可证明的安全性。

背景介绍

软件沙箱化

软件沙箱化是指在代码运行过程中，代码中出现的问题 (尤其是内存相关的安全问题) 只会影响出现问题的部分代码，对于软件其他部分的内存安全不会造成影响。

一种常见的软件沙箱化技术是 Software Fault Isolation (SFI)，这种技术将模块或库作为代码边界，保证代码中的 bug 只会影响问题代码所在的模块或库，不会超出代码边界。

WebAssembly

WebAssembly (Wasm) 是一种类似于汇编的低级编程语言，被用于在浏览器中提供比JavaScript更高效率的执行。Wasm 使用了一种以栈为基础的虚拟架构，其代码被分为多个模块 (modules)，每个模块都有自己独立的代码和数据，只能访问为模块分配的内存和定义的全局变量。同时 Wasm 确定性的语义使得其几乎不存在未定义行为 (除了浮点数NaN)。同时，Wasm作为一种编译目标语言，可以由C、C++、Rust、Java、Go等多种语言编译得到，具有良好的多语言特性和跨平台性。

由于Wasm具有良好的安全性和跨平台性，并且可以由多种语言编译得到，许多开发者尝试将Wasm从浏览器端移植到桌面端，通过构建虚拟机和AoT技术使得Wasm代码可以高效地运行在桌面端。虽然 Wasm 本身定义了良好的安全性，但由于运行环境的实现可能存在安全问题，因此很难完全保证程序的安全运行。

除此之外，作者还分析了各种Wasm的实现方法在安全性和效率之间的关系：

因此，作者实现了两种可证明安全的Wasm编译器 (上图中绿色的点)，将需要执行的Wasm代码沙箱化，在高效执行的同时，保证代码的内存安全性。

威胁模型

对于作者实现的基于Wasm的沙箱，攻击者被定义为拥有某个沙箱中的模块的控制权 (通过bug或恶意第三方代码)，并希望从沙箱中逃逸以控制外部运行环境。

在作者定义的威胁模型中，攻击者具有以下能力：

1. 攻击者可以从模块的任意位置开始执行代码；

2. 攻击者可以操纵模块线性内存中的任意点；

3. 攻击者可以调用并传递任意参数给模块中的任意函数。

因此，作者之后的设计实现均围绕以上威胁模型，通过形式化或非形式化的方法证明，在作者的编译器实现中，攻击者不能通过获取某一模块的控制权影响程序的其他部分，即不能访问不属于模块自身的内存 (这也是后续实现所遵循的唯一定理)。

具体实现

vWasm: 基于F*的形式化验证的编译器

作者的第一种实现使用了形式化验证的方法证明编译过程的安全性。作者在实现过程中使用了F*语言，一种为形式化验证构建的通用函数式编程语言。

vWasm的设计分为三部分：

1. 将Wasm编译成中间表示的前端；

2. 对中间表示进行沙箱化的模块；

3. 将沙箱化的结果翻译成 x64 汇编的输出部分。

其中第二部分为沙箱化的主要模块，也是作者进行形式化验证的部分。作者将 Wasm 的指令对应为 x64 汇编的子集，并使用F*对该子集以及沙箱化过程进行建模，通过F*提供的形式化验证功能，证明沙箱化过程输出的代码满足 Wasm 的安全性定义，即代码只会访问自身所在模块的内存，而不会访问内存的其他部分。

下图为作者在F*中建立的模型：

rWasm: 基于 Rust 的安全高效的编译器

作者的第二种实现方法基于 Rust 语言，通过将 Wasm 代码提升 (lifting) 到 Rust 代码，并使用 Rust 编译器编译成可执行文件，使得生成的可执行文件具有 Rust 的高效和安全性。而这种实现方法的安全性完全依赖于 Rust 的内存安全性，所以这种实现被作者称为非形式化证明安全 (Informally-Proven-Safe) 。

由于 Rust 本身的内存安全性，这种实现方法基本可以满足 Wasm 的安全性定义 (除非 Rust 本身出现内存安全问题)。

在实现中，作者将 Wasm 模块定义为一个 Rust 的结构体，结构体中存储模块的线性内存、全局变量、函数调用表和运行上下文：

将 Wasm 指令和变量对应翻译成基于该结构体的 Rust 代码并编译：

最终将 Wasm 代码编译成可执行文件从而在桌面端运行。

结果分析

上述两种方法均实现了 Wasm 代码安全且高效的沙箱化执行，其中的安全性分别由形式化验证和 Rust 的内存安全性保证。在阐述了实现与安全性后，作者将两种实现的运行效率与其他本地 Wasm 运行环境进行了对比。

对比结果如下图所示：

其中基于F*语言和形式化验证实现的 vWasm 虽然可以提供最好的安全性但运行效率略有不足，但是作者通过增加一项关闭沙箱化功能的 vWasm* 的结果表明，效率的降低并非来自于保证安全性的沙箱化过程。

而基于 Rust 语言的 rWasm 则表现出较高的运行效率，并且对于某些特定的测试，rWasm 的运行效率甚至超过了主要针对运行效率进行优化的 WAVM。

---

论文PDF：https://www.jaybosamiya.com/publications/2022/usenix/provably-safe-sandboxing-wasm.pdf

原文始发于微信公众号（安全研究GoSSIP）：G.O.S.S.I.P 阅读推荐 2022-09-02