MSWasm: Soundly Enforcing Memory-Safe Execution of Unsafe Code

Computer Science > Cryptography and Security [Submitted on 29 Aug 2022 (v1), last revised 16 Apr 2026 (this version, v3)] MSWasm: Soundly Enforcing Memory-Safe Execution of Unsafe Code Alexandra E. Michael, Anitha Gollamudi, Jay Bosamiya, Craig Disselkoen, Aidan Denlinger, Conrad Watt, Bryan Parno, Marco Patrignani, Marco Vassena, Deian Stefan 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. Subjects: Cryptography and Security (cs.CR); Programming Languages (cs.PL) Cite as: arXiv:2208.13583 [cs.CR]   (or arXiv:2208.13583v3 [cs.CR] for this version)   https://doi.org/10.48550/arXiv.2208.13583 Focus to learn more Related DOI: https://doi.org/10.1145/3554344 Focus to learn more Submission history From: Anitha Gollamudi [view email] [v1] Mon, 29 Aug 2022 13:22:28 UTC (1,095 KB) [v2] Mon, 26 Sep 2022 16:50:30 UTC (1,095 KB) [v3] Thu, 16 Apr 2026 03:27:12 UTC (993 KB) Access Paper: HTML (experimental) view license Ancillary files (details): tr.pdf Current browse context: cs.CR < prev   |   next > new | recent | 2022-08 Change to browse by: cs cs.PL References & Citations NASA ADS Google Scholar Semantic Scholar Export BibTeX Citation Bookmark Bibliographic Tools Bibliographic and Citation Tools Bibliographic Explorer Toggle Bibliographic Explorer (What is the Explorer?) Connected Papers Toggle Connected Papers (What is Connected Papers?) Litmaps Toggle Litmaps (What is Litmaps?) scite.ai Toggle scite Smart Citations (What are Smart Citations?) Code, Data, Media Demos Related Papers About arXivLabs Which authors of this paper are endorsers? | Disable MathJax (What is MathJax?)