Provably-Safe Multilingual Software Sandboxing using WebAssembly

Authors: 

Jay Bosamiya, Wen Shih Lim, and Bryan Parno, Carnegie Mellon University

Distinguished Paper Award Winner and Second Prize Winner (tie) of the 2022 Internet Defense Prize

Abstract: 

Many applications, from the Web to smart contracts, need to safely execute untrusted code. We observe that WebAssembly (Wasm) is ideally positioned to support such applications, since it promises safety and performance, while serving as a compiler target for many high-level languages. However, Wasm's safety guarantees are only as strong as the implementation that enforces them. Hence, we explore two distinct approaches to producing provably sandboxed Wasm code. One draws on traditional formal methods to produce mathematical, machine-checked proofs of safety. The second carefully embeds Wasm semantics in safe Rust code such that the Rust compiler can emit safe executable code with good performance. Our implementation and evaluation of these two techniques indicate that leveraging Wasm gives us provably-safe multilingual sandboxing with performance comparable to standard, unsafe approaches.

Open Access Media

USENIX is committed to Open Access to the research presented at our events. Papers and proceedings are freely available to everyone once the event begins. Any video, audio, and/or slides that are posted after the event are also free and open to everyone. Support USENIX and our commitment to Open Access.

BibTeX
@inproceedings {279990,
author = {Jay Bosamiya and Wen Shih Lim and Bryan Parno},
title = {{Provably-Safe} Multilingual Software Sandboxing using {WebAssembly}},
booktitle = {31st USENIX Security Symposium (USENIX Security 22)},
year = {2022},
isbn = {978-1-939133-31-1},
address = {Boston, MA},
pages = {1975--1992},
url = {https://www.usenix.org/conference/usenixsecurity22/presentation/bosamiya},
publisher = {USENIX Association},
month = aug,
}