  WebAssembly (Wasm) is a next-generation portable compilation target for
deploying applications written in high-level languages on the web. In order to
protect their memory from untrusted code, web browser engines confine the
execution of compiled Wasm programs in a memory-safe sandbox. Unfortunately,
classic memory-safety vulnerabilities (e.g., buffer overflows and
use-after-free) can still corrupt the memory within the sandbox and allow Wasm
code to mount severe attacks. To prevent these attacks, we study a class of
secure compilers that eliminate (different kinds of) of memory safety
violations. Following a rigorous approach, we discuss memory safety in terms of
hypersafety properties, which let us identify suitable secure compilation
criteria for memory-safety-preserving compilers. We conjecture that, barring
some restrictions at module boundaries, the existing security mechanisms of
Wasm may suffice to enforce memory-safety preservation, in the short term. In
the long term, we observe that certain features proposed in the design of a
memory-safe variant of Wasm could allow compilers to lift these restrictions
and enforce relaxed forms of memory safety.
