  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 the overhead of enforcing memory safety in software
ranges from 22% (enforcing spatial safety alone) to 198% (enforcing full memory
safety) on the PolyBenchC suite. 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.
