Thu 20 Jan 2022 15:05 - 15:30 at Salon I - Systems Chair(s): Arthur Azevedo de Amorim

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 Jan

Displayed time zone: Eastern Time (US & Canada) change

15:05 - 16:20
SystemsPOPL at Salon I
Chair(s): Arthur Azevedo de Amorim Boston University
15:05
25m
Research 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
25m
Research 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
25m
Research 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