如何安全高效地执行不受信任的第三方代码,一直是安全研究领域中被广泛关注的问题之一。随着云计算、智能合约等技术的发展,这一问题受到了更多人的重视。今年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或恶意第三方代码),并希望从沙箱中逃逸以控制外部运行环境。
在作者定义的威胁模型中,攻击者具有以下能力:
-
攻击者可以从模块的任意位置开始执行代码;
-
攻击者可以操纵模块线性内存中的任意点;
-
攻击者可以调用并传递任意参数给模块中的任意函数。
因此,作者之后的设计实现均围绕以上威胁模型,通过形式化或非形式化的方法证明,在作者的编译器实现中,攻击者不能通过获取某一模块的控制权影响程序的其他部分,即不能访问不属于模块自身的内存 (这也是后续实现所遵循的唯一定理)。
具体实现
vWasm: 基于F*
的形式化验证的编译器
作者的第一种实现使用了形式化验证的方法证明编译过程的安全性。作者在实现过程中使用了F*
语言,一种为形式化验证构建的通用函数式编程语言。
vWasm的设计分为三部分:
-
将Wasm编译成中间表示的前端;
-
对中间表示进行沙箱化的模块;
-
将沙箱化的结果翻译成 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
- 左青龙
- 微信扫一扫
-
- 右白虎
- 微信扫一扫
-
评论