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

admin 2022年9月3日01:06:37安全闲碎评论0 views2422字阅读8分4秒阅读模式

如何安全高效地执行不受信任的第三方代码,一直是安全研究领域中被广泛关注的问题之一。随着云计算、智能合约等技术的发展,这一问题受到了更多人的重视。今年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的沙盒提出了新的(可证明安全的)解决方案。

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

在本文中,作者以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的实现方法在安全性和效率之间的关系:

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

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

威胁模型

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

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

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

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

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

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

具体实现

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

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

vWasm的设计分为三部分:

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

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

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

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

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

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

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

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

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

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

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

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

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

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

结果分析

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

对比结果如下图所示:

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

其中基于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

特别标注: 本站(CN-SEC.COM)所有文章仅供技术研究,若将其信息做其他用途,由用户承担全部法律及连带责任,本站不承担任何法律及连带责任,请遵守中华人民共和国安全法.
  • 我的微信
  • 微信扫一扫
  • weinxin
  • 我的微信公众号
  • 微信扫一扫
  • weinxin
admin
  • 本文由 发表于 2022年9月3日01:06:37
  • 转载请保留本文链接(CN-SEC中文网:感谢原作者辛苦付出):
                  G.O.S.S.I.P 阅读推荐 2022-09-02 http://cn-sec.com/archives/1273770.html

发表评论

匿名网友 填写信息

:?: :razz: :sad: :evil: :!: :smile: :oops: :grin: :eek: :shock: :???: :cool: :lol: :mad: :twisted: :roll: :wink: :idea: :arrow: :neutral: :cry: :mrgreen: