Isolation without Taxation: Near-Zero-Cost Transitions for WebAssembly and SFIInPerson
Software sandboxing or software-based fault isolation (SFI) is a lightweight approach to building secure systems out of untrusted components. Mozilla, for example, uses SFI to harden the Firefox browser by sandboxing third-party libraries, and companies like Fastly and Cloudflare use SFI to safely co-locate untrusted tenants on their edge clouds. While there have been significant efforts to optimize and verify SFI enforcement, context switching in SFI systems remains largely unexplored: almost all SFI systems use \emph{heavyweight transitions} that are not only error-prone but incur significant performance overhead from saving, clearing, and restoring registers when context switching. We identify a set of \emph{zero-cost conditions} that characterize when sandboxed code is well-structured enough so that security can be guaranteed via lightweight \emph{zero-cost} transitions (simple function calls). We show that using WebAssembly (Wasm) as an intermediate representation for low-level code naturally results in an SFI system with zero-cost transitions. We modify the Lucet Wasm compiler and its runtime to use zero-cost transitions, eliminating the undue performance tax on systems that rely on Lucet for sandboxing (e.g., we speed up image and font rendering in Firefox by up to 29.7% and 10% respectively). To remove the Wasm specification and, more importantly, the Lucet compiler from the trusted computing base we (1) develop a \emph{static binary verifier}, VeriZero, which (in seconds) checks that binaries produced by Lucet satisfy our zero-cost conditions, and (2) prove the soundness of VeriZero by developing a logical relation that captures when a compiled Wasm function is semantically well-behaved with respect to our zero-cost conditions. Finally, we show that our model is useful beyond Wasm by describing a new, purpose-built SFI system, SegmentZero32, that uses x86 segmentation and LLVM with mostly off-the-shelf passes to enforce our zero-cost conditions; our prototype performs on-par with the state-of-the-art Native Client SFI system.
Thu 20 JanDisplayed time zone: Eastern Time (US & Canada) change
15:05 - 16:20 | |||
15:05 25mResearch paper | Isolation without Taxation: Near-Zero-Cost Transitions for WebAssembly and SFIInPerson POPL Matthew Kolosick University of California at San Diego, Shravan Ravi Narayan University of California at San Diego, Evan Johnson University of California at San Diego, Conrad Watt University of Cambridge, Michael LeMay Intel Labs, Deepak Garg MPI-SWS, Ranjit Jhala University of California at San Diego, Deian Stefan University of California at San Diego DOI Media Attached | ||
15:30 25mResearch paper | Relational E-matchingRemote POPL Yihong Zhang University of Washington, Yisu Remy Wang University of Washington, Max Willsey University of Washington, Zachary Tatlock University of Washington DOI Media Attached | ||
15:55 25mResearch paper | Linked Visualisations via Galois DependenciesRemote POPL Roly Perera Alan Turing Institute, Minh Nguyen University of Bristol, Tomas Petricek University of Kent, Meng Wang University of Bristol DOI Media Attached |