Jay Bosamiya on X: "Two compilers, both generate provably sandboxed machine code from WebAssembly. One's traditionally-formally-verified; the other uses the power of Rust! Check out our paper (accepted at USENIX Security'22): https://t.co/gIxyugsJwl https://t.co/7YyFXxfCI9" / X

Two compilers, both generate provably sandboxed machine code from WebAssembly. One's traditionally-formally-verified; the other uses the power of Rust! Check out our paper (accepted at USENIX Security'22): jaybosamiya.com/publications/2

Provably-Safe Multilingual Software Sandboxing using WebAssembly

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.

read image description

ALT

9:02 PM · Feb 22, 2022

Bookmarks

Conversation