MSWasm: Soundly Enforcing Memory-Safe Execution of Unsafe Code
Most programs compiled to WebAssembly (Wasm) today are written in unsafe languages like C and C++.
Unfortunately, memory-unsafe C code remains unsafe when compiled to Wasm—and attackers can exploit
buffer overflows and use-after-frees in Wasm almost as easily as they can on native platforms. Memory-
Safe WebAssembly (MSWasm) proposes to extend Wasm with language-level memory-safety abstractions to
precisely address this problem. In this paper, we build on the original MSWasm position paper to realize this vision. We give a precise and formal semantics of MSWasm, and prove that well-typed MSWasm programs are, by construction, robustly memory safe. To this end, we develop a novel, language-independent memory-safety property based on colored memory locations and pointers. This property also lets us reason about the security guarantees of a formal C-to-MSWasm compiler—and prove that it always produces memory-safe programs (and preserves the semantics of safe programs). We use these formal results to then guide several implementations: Two compilers of MSWasm to native code, and a C-to-MSWasm compiler (that extends Clang). Our MSWasm compilers support different enforcement mechanisms, allowing developers to make security-performance trade-offs according to their needs. Our evaluation shows that on the PolyBenchC suite, the overhead of enforcing memory safety in software ranges from 22% (enforcing spatial safety alone) to 198% (enforcing full memory safety), and 51.7% when using hardware memory capabilities for spatial safety and pointer integrity.
More importantly, MSWasm’s design makes it easy to swap between enforcement mechanisms; as fast (especially hardware-based) enforcement techniques become available, MSWasm will be able to take advantage of these advances almost for free.
Wed 18 JanDisplayed time zone: Eastern Time (US & Canada) change
15:10 - 16:25
|MSWasm: Soundly Enforcing Memory-Safe Execution of Unsafe Code|
Alexandra E. Michael University of California at San Diego; University of Washington, Anitha Gollamudi University of Massachusetts Lowell, Jay Bosamiya Carnegie Mellon University, Evan Johnson University of California at San Diego; Arm, Aidan Denlinger University of California at San Diego, Craig Disselkoen University of California at San Diego, Conrad Watt University of Cambridge, Bryan Parno Carnegie Mellon University, Marco Patrignani University of Trento, Marco Vassena Utrecht University, Deian Stefan University of California at San DiegoDOI
|Reconciling Shannon and Scott with a Lattice of Computable Information|
Sebastian Hunt City University of London, Dave Sands Chalmers University of Technology, Sandro Stucki Amazon Prime VideoLink to publication DOI Pre-print
|A Core Calculus for Equational Proofs of Cryptographic Protocols|
Joshua Gancher Carnegie Mellon University, Kristina Sojakova Inria, Xiong Fan Rutgers University, Elaine Shi Carnegie Mellon University, Greg Morrisett Cornell UniversityDOI