pith. sign in

arxiv: 2208.13583 · v3 · submitted 2022-08-29 · 💻 cs.CR · cs.PL

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
show 2 more authors
Marco Vassena Deian Stefan
This is my paper

Pith reviewed 2026-05-24 11:27 UTC · model grok-4.3

classification 💻 cs.CR cs.PL
keywords memory safetyWebAssemblyMSWasmformal semanticscompiler correctnessrobust safetyC to WebAssembly
0
0 comments X

The pith

Well-typed MSWasm programs are robustly memory safe by construction.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

MSWasm extends WebAssembly with language-level abstractions that enforce memory safety for code compiled from unsafe languages such as C. The paper supplies a formal semantics for the extension and proves that any well-typed program satisfies a robust memory-safety property. The proof rests on a colored-memory model that tracks ownership of locations and pointers. A separate compiler from C to MSWasm is shown to emit only well-typed code and to preserve the observable behavior of already-safe C programs. Implementations then demonstrate that the same typed programs can be executed under different enforcement strategies that trade performance for stronger guarantees.

Core claim

The central claim is that a well-typed MSWasm program cannot violate memory safety even when the source program contains buffer overflows or use-after-frees; the colored-memory property ensures that every pointer dereference respects the color boundaries established at allocation time, and the C-to-MSWasm compiler is proven to produce only such well-typed programs while preserving semantics for safe inputs.

What carries the argument

The colored-memory property, which labels each memory location and pointer with a color so that accesses are permitted only when colors match and bounds are respected.

If this is right

  • The C-to-MSWasm compiler always emits memory-safe code.
  • MSWasm programs can be executed under interchangeable enforcement mechanisms ranging from software checks to hardware support.
  • Spatial safety alone incurs 22 percent overhead while full memory safety incurs 198 percent overhead on PolyBenchC.
  • New enforcement techniques can be adopted by swapping the runtime without changing the typed source programs.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The same colored-memory discipline could be applied to other low-level languages that target WebAssembly.
  • Hardware memory-safety features could be integrated by mapping colors directly to hardware tags.
  • The formal results supply a reusable template for proving memory safety of compilers from other unsafe languages.

Load-bearing premise

The colored-memory property exactly matches the intended robustness notion of memory safety without either missing attacks or ruling out valid programs.

What would settle it

A concrete well-typed MSWasm program together with an input that produces a memory-safety violation such as an out-of-bounds write or a use-after-free.

Figures

Figures reproduced from arXiv: 2208.13583 by Aidan Denlinger, Alexandra E. Michael, Anitha Gollamudi, Bryan Parno, Conrad Watt, Craig Disselkoen, Deian Stefan, Jay Bosamiya, Marco Patrignani, Marco Vassena.

Figure 1
Figure 1. Figure 1: Syntax of MSWasm with extensions to Wasm highlighted. [PITH_FULL_IMAGE:figures/full_fig_p007_1.png] view at source ↗
Figure 2
Figure 2. Figure 2: Wasm and MSWasm runtime structures. (Stack-Top) Φ ∗ ⊢ ⟨𝚺, (𝜽, i, v ∗ )⟩ 𝜶 −−→→ ⟨𝚺 ′ , (𝜽 ′ , i ′∗ , v ′∗ )⟩ Φ ∗ ⊢ ⟨𝚺, (𝜽, i : i∗ , v ∗ ++ vb ∗ )⟩ 𝜶 −−→→ ⟨𝚺, (𝜽, i ′∗ ++ i ∗ , v ′∗ ++ vb ∗ )⟩ (Get) 𝜽 [n] = v Φ ∗ ⊢ ⟨𝚺, (𝜽, get n, [])⟩ −→→ ⟨𝚺, (𝜽, [], [v])⟩ (If-T) n ≠ 0 Φ ∗ ⊢ ⟨𝚺, (𝜽, branch i1 ∗ i2 ∗ , [n])⟩ −→→ ⟨𝚺, (𝜽, i1 ∗ , [])⟩ (Load) 0 ≤ n n + |𝝉 | < |H| b |𝝉 | = [ Σ.H[n + j] | j ∈ {0..|𝝉 | − 1} ] v = 𝝉 … view at source ↗
Figure 3
Figure 3. Figure 3: Semantics of Wasm (excerpts). stack v ∗ for the values produced (and consumed) by those instructions. Values include constants c and integers n. The semantics judgment Φ ∗ ⊢ ⟨𝚺, F⟩ 𝜶 −−→→ ⟨𝚺 ′ , F ′ ⟩ indicates that under function definitions Φ ∗ , local configuration ⟨𝚺, F⟩ executes a single instruction and steps to ⟨𝚺 ′ , F ′ ⟩, generating event 𝜶 (explained below). The semantics features also a separate… view at source ↗
Figure 4
Figure 4. Figure 4: Semantics of MSWasm (excerpts). The premises that ensure handle integrity are highlighted. [PITH_FULL_IMAGE:figures/full_fig_p010_4.png] view at source ↗
Figure 5
Figure 5. Figure 5: Trace-based definition of memory safety. [PITH_FULL_IMAGE:figures/full_fig_p012_5.png] view at source ↗
Figure 6
Figure 6. Figure 6: Relation between MSWasm and abstract events (excerpts). [PITH_FULL_IMAGE:figures/full_fig_p013_6.png] view at source ↗
Figure 7
Figure 7. Figure 7: C syntax and runtime structures (excerpts). [PITH_FULL_IMAGE:figures/full_fig_p015_7.png] view at source ↗
Figure 8
Figure 8. Figure 8: Semantics of C (excerpts). of MSWasm however, the source allocator does not trap upon an invalid free request, i.e., a free of an unallocated memory region, but silently drops the request.5 The source language uses a separate semantic judgment for function calls and returns (omitted), and a top-level judgment M _𝛼 ∗ , which collects the trace generated by program M. We define memory safety for source trace… view at source ↗
Figure 9
Figure 9. Figure 9: Compiler from C to MSWasm (excerpts). function sz (·) : 𝜏 → n) and offsets for expressions that involve pointer arithmetic, struct accesses and memory allocations. For example, a binary operation (⊕) whose first operand is an array (array 𝜏) needs to be compiled in a handle.add, as in Rule (C-Ptr-BinOp). On the other hand, a binary operation on naturals needs to be compiled in the related MSWasm binary ope… view at source ↗
Figure 10
Figure 10. Figure 10: Cross-language equivalence relation: values (top) and events (bottom). [PITH_FULL_IMAGE:figures/full_fig_p018_10.png] view at source ↗
Figure 11
Figure 11. Figure 11: Proof diagram for Theorem 2: functional correctness (left) and memory-safety preservation (right). Theorem 3 (Memory Violations Trap). If ⊢ M : wt and M _𝛼 ∗ ++ [𝛼] ++ 𝛼 ′∗ and MS(𝛼 ∗ ) and ¬MS(𝛼 ∗ ++ [𝛼]) then ∃𝛿, 𝜶 ∗ . 𝛼 ∗ =𝛿 𝜶 ∗ and JMK_ 𝜶 ∗ ++ [trap] Together these theorems characterize the scope of our compiler-based memory-safety enforcement: Corollary 1 (Memory-Safety Enforcement). If JMK_ 𝜶 ∗ then… view at source ↗
Figure 12
Figure 12. Figure 12: End-to-end compilation pipeline. We first compile [PITH_FULL_IMAGE:figures/full_fig_p020_12.png] view at source ↗
Figure 13
Figure 13. Figure 13: Performance of our implementations of MSWasm compared to normal Wasm, normalized against native (non-Wasm) execution on benchmarks from PolyBenchC the end-to-end overhead to 197.5%. For the JIT compiler, enforcing spatial and temporal safety results in an overhead comparable to that of the AOT compiler: Graal𝑆𝑇 imposes a 42.3% geomean overhead. The JIT approach is much slower than the AOT approach though—… view at source ↗
read the original abstract

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.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

1 major / 2 minor

Summary. The paper introduces Memory-Safe WebAssembly (MSWasm) as an extension to WebAssembly with language-level memory-safety abstractions. It defines a precise formal semantics for MSWasm, introduces a novel colored-memory property as the basis for a language-independent notion of robust memory safety, proves that well-typed MSWasm programs satisfy this property by construction, and proves that a formal C-to-MSWasm compiler always produces memory-safe programs while preserving the semantics of safe programs. The paper further describes two MSWasm-to-native compilers supporting different enforcement mechanisms and a Clang-based C-to-MSWasm compiler, with an evaluation on PolyBenchC reporting overheads ranging from 22% (spatial safety) to 198% (full memory safety).

Significance. If the colored-memory property accurately models the intended robustness guarantees, the work supplies a sound formal foundation for memory-safe execution of unsafe code targeting WebAssembly, together with practical compiler implementations that allow security-performance trade-offs. Explicit strengths include the machine-checked-style formal semantics and proofs of type safety and compiler preservation, the design that supports swapping enforcement mechanisms, and the reproducible evaluation on PolyBenchC.

major comments (1)
  1. [§4] §4 (colored-memory property definition): The property is load-bearing for both the claim that well-typed MSWasm programs are robustly memory safe and the compiler correctness theorem. The manuscript defines the property via colored locations and pointers and proves internal theorems within this model, but provides no reduction, lemma, or explicit argument showing that the property blocks all standard memory-safety violations (buffer overflows, use-after-free, etc.) while permitting legitimate programs. This modeling assumption therefore requires additional justification to support the security claims in the abstract.
minor comments (2)
  1. [Evaluation] The evaluation reports overhead ranges but does not clearly map each percentage to a specific enforcement mechanism or include per-benchmark breakdowns; adding a table with these details would improve clarity.
  2. [§3] Notation for colored pointers and memory in the operational semantics could be introduced with a small example to aid readability for readers unfamiliar with the position paper.

Simulated Author's Rebuttal

1 responses · 0 unresolved

We thank the referee for the careful review and for highlighting the importance of the colored-memory property. We address the single major comment below.

read point-by-point responses

  1. Referee: [§4] §4 (colored-memory property definition): The property is load-bearing for both the claim that well-typed MSWasm programs are robustly memory safe and the compiler correctness theorem. The manuscript defines the property via colored locations and pointers and proves internal theorems within this model, but provides no reduction, lemma, or explicit argument showing that the property blocks all standard memory-safety violations (buffer overflows, use-after-free, etc.) while permitting legitimate programs. This modeling assumption therefore requires additional justification to support the security claims in the abstract.

    Authors: We agree that an explicit argument linking the colored-memory property to standard violations strengthens the presentation. The property is defined so that every allocation receives a fresh color, every pointer carries its target color, and well-typed programs may only dereference a pointer whose color matches the accessed location. Consequently, a buffer overflow necessarily targets either an out-of-bounds address (different color) or an invalid location; a use-after-free necessarily targets a location whose color has been updated on deallocation/reuse. Legitimate intra-object accesses remain possible because they stay within the same colored region. We will add a short subsection (or lemma) in §4 that states this correspondence formally, supplies one-line arguments for each classic violation, and notes that the same reasoning applies to the compiler theorem. This addition will be included in the revised manuscript. revision: yes

Circularity Check

1 steps flagged

Minor self-citation to prior position paper by overlapping authors; core colored-memory property, semantics, and proofs are newly defined

specific steps
  1. self citation load bearing [Abstract]
    "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."

    The MSWasm vision and approach is introduced via reference to a prior paper whose authors overlap with the present work, though the subsequent formal development (colored memory, semantics, and proofs) does not reduce to that citation.

full rationale

The paper cites an earlier MSWasm position paper by overlapping authors when introducing the vision, but the colored-memory property is presented as novel, the operational semantics and type system are defined in this work, and the robust memory safety theorems for well-typed programs and the C-to-MSWasm compiler are proved here without reducing to prior fitted quantities or self-citations by construction. No self-definitional, fitted-prediction, uniqueness-import, ansatz-smuggling, or renaming patterns appear. This is a normal minor self-citation that does not affect the independence of the central formal results.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 1 invented entities

The central claims rest on the validity of the colored-memory model as a faithful abstraction of memory safety and on standard background results from operational semantics and type theory; no data-fitted parameters appear in the formal development.

axioms (1)
  • standard math Standard properties of operational semantics and type systems hold for the defined language.
    Used to establish that well-typed programs satisfy the memory-safety property.
invented entities (1)
  • colored memory locations and pointers no independent evidence
    purpose: To define a language-independent memory-safety property enabling robustness proofs
    New modeling device introduced to capture spatial and temporal safety in a uniform way.

pith-pipeline@v0.9.0 · 5873 in / 1353 out tokens · 62530 ms · 2026-05-24T11:27:18.730138+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

23 extracted references · 23 canonical work pages

  1. [1]

    In 2019 IEEE 32th Computer Security Foundations Symposium (CSF

    Journey Beyond Full Abstraction: Exploring Robust Property Preservation for Secure Compilation. In 2019 IEEE 32th Computer Security Foundations Symposium (CSF

    work page 2019

  2. [2]

    White Paper (2019)

    Armv8.5-A Memory Tagging Extension. White Paper (2019). Todd M. Austin, Scott E. Breach, and Gurindar S. Sohi

    work page 2019

  3. [3]

    In Proceedings of the ACM SIGPLAN 1994 Conference on Programming Language Design and Implementation (Orlando, Florida, USA) (PLDI ’94)

    Efficient Detection of All Pointer and Array Access Errors. In Proceedings of the ACM SIGPLAN 1994 Conference on Programming Language Design and Implementation (Orlando, Florida, USA) (PLDI ’94). Association for Computing Machinery, New York, NY, USA, 290–301. https://doi.org/10.1145/ 178243.178446 Arthur Azevedo de Amorim, Cătălin Hriţcu, and Benjamin C. Pierce

    work page arXiv 1994

  4. [4]

    https://community

    Supporting the UK in becoming a leading global player in cybersecurity. https://community. arm.com/blog/company/b/blog/posts/supporting-the-uk-in-becoming-a-leading-global-player-in-cybersecurity. Andreas Haas, Andreas Rossberg, Derek L. Schuff, Ben L. Titzer, Michael Holman, Dan Gohman, Luke Wagner, Alon Zakai, and JF Bastien. 2017a. Bringing the Web up ...

    work page doi:10.1145/3062341.3062363 2017

  5. [5]

    Aaron Hilbig, Daniel Lehmann, and Michael Pradel

    What is memory safety? http://www.pl-enthusiast.net/2014/07/21/memory-safety/. Aaron Hilbig, Daniel Lehmann, and Michael Pradel

    work page 2014

  6. [6]

    Native Code

    Not So Fast: Analyzing the Performance of WebAssembly vs. Native Code. In 2019 USENIX Annual Technical Conference (USENIX ATC

    work page 2019

  7. [7]

    In 2002 USENIX Annual Technical Conference (USENIX ATC

    Cyclone: A Safe Dialect of C. In 2002 USENIX Annual Technical Conference (USENIX ATC

    work page 2002

  8. [8]

    In Proceedings of the 2013 ACM SIGSAC Conference on Computer and Communications Security

    Low-Fat Pointers: Compact Encoding and Efficient Gate-Level Implementation of Fat Pointers for Spatial Safety and Capability-Based Security. In Proceedings of the 2013 ACM SIGSAC Conference on Computer and Communications Security . ACM. Byoungyoung Lee, Chengyu Song, Yeongjin Jang, Tielei Wang, Taesoo Kim, Long Lu, and Wenke Lee

    work page 2013

  9. [9]

    Journal of Automated Reasoning 43, 4 (2009), 363–446

    A Formally Verified Compiler Back-end. Journal of Automated Reasoning 43, 4 (2009), 363–446. http://dx.doi.org/10.1007/s10817-009-9155-4 Hans Liljestrand, Thomas Nyman, Kui Wang, Carlos Chinea Perez, Jan-Erik Ekberg, and N. Asokan

    work page doi:10.1007/s10817-009-9155-4 2009

  10. [10]

    Principles of Secure Compilation (PriSC)

    Lucet: A Compiler and Runtime for High-Concurrency Low-Latency Sandboxing. Principles of Secure Compilation (PriSC). Kayvan Memarian, Victor B. F. Gomes, Brooks Davis, Stephen Kell, Alexander Richardson, Robert N. M. Watson, and Peter Sewell. 2019a. Exploring C Semantics and Pointer Provenance. Proc. ACM Program. Lang. 3, POPL, Article 67 (Jan. 2019), 32 ...

    work page doi:10.1145/3290380 2019

  11. [11]

    SIGPLAN Not

    Into the Depths of C: Elaborating the de Facto Standards. SIGPLAN Not. 51, 6 (June 2016), 1–15. Santosh Nagarakatte, Jianzhou Zhao, Milo M.K. Martin, and Steve Zdancewic

    work page 2016

  12. [12]

    44, 6 (June 2009), 245–258

    SoftBound: Highly Compatible and Complete Spatial Memory Safety for C.SIGPLAN Not. 44, 6 (June 2009), 245–258. https://doi.org/10.1145/1543135.1542504 Santosh Nagarakatte, Jianzhou Zhao, Milo M.K. Martin, and Steve Zdancewic

    work page doi:10.1145/1543135.1542504 2009

  13. [13]

    SIGPLAN Not

    CETS: Compiler Enforced Temporal Safety for C. SIGPLAN Not. 45, 8 (June 2010), 31–40. https://doi.org/10.1145/1837855.1806657 Shravan Narayan, Craig Disselkoen, Tal Garfinkel, Nathan Froyd, Eric Rahm, Sorin Lerner, Hovav Shacham, and Deian Stefan

    work page doi:10.1145/1837855.1806657 2010

  14. [14]

    ACM Trans

    CCured: Type-safe Retrofitting of Legacy Software. ACM Trans. Program. Lang. Syst. 27, 3 (May 2005), 477–526. https://doi.org/10.1145/1065887.1065892 Oleksii Oleksenko, Dmitrii Kuvaiskii, Pramod Bhatotia, Pascal Felber, and Christof Fetzer

    work page doi:10.1145/1065887.1065892 2005

  15. [15]

    Intel MPX Explained: A Cross-Layer Analysis of the Intel MPX System Stack. Proc. ACM Meas. Anal. Comput. Syst. 2, 2, Article 28 (jun 2018), 30 pages. https://doi.org/10.1145/3224423 Aleph One

    work page doi:10.1145/3224423 2018

  16. [16]

    Phrack magazine 7, 49 (1996), 14–16

    Smashing the stack for fun and profit. Phrack magazine 7, 49 (1996), 14–16. Oracle. 2021a. GraalVM. https://www.graalvm.org/. Oracle. 2021b. Truffle Language Implementation Framework. https://www.graalvm.org/22.0/graalvm-as-a-platform/ language-implementation-framework/. Matthew Parkinson, Kapil Vaswani, Dimitrios Vytiniotis, Manuel Costa, Pantazis Deligi...

    work page 1996

  17. [17]

    Tech- nical Report MSR-TR-2017-32

    Project Snowflake: Non-blocking safe manual memory management in .NET . Tech- nical Report MSR-TR-2017-32. Microsoft. https://www.microsoft.com/en-us/research/publication/project-snowflake- non-blocking-safe-manual-memory-management-net/ Harish Patil and Charles Fischer

    work page 2017

  18. [18]

    Low-Cost, Concurrent Checking of Pointer and Array Accesses in C Programs. Softw. Pract. Exper. 27, 1 (jan 1997), 87–110. Marco Patrignani

    work page 1997

  19. [19]

    CoRR abs/2001.11334 (2020)

    Why Should Anyone use Colours? or, Syntax Highlighting Beyond Code Snippets. CoRR abs/2001.11334 (2020). arXiv:2001.11334 https://arxiv.org/abs/2001.11334 Gregor Peach, Runyu Pan, Zhuoyi Wu, Gabriel Parmer, Christopher Haster, and Ludmila Cherkasova

    work page arXiv 2001

  20. [20]

    IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems 39, 11 (2020), 3492–3505

    eWASM: Practical Software Fault Isolation for Reliable Embedded Devices. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems 39, 11 (2020), 3492–3505. https://doi.org/10.1109/TCAD.2020.3012647 Louis-Noel Pouchet

    work page doi:10.1109/tcad.2020.3012647 2020

  21. [21]

    ACM Trans

    Enforceable Security Policies. ACM Trans. Inf. Syst. Secur. 3, 1 (feb 2000), 30–50. https://doi.org/10. 1145/353323.353382 Laszlo Szekeres, Mathias Payer, Tao Wei, and Dawn Song

    work page arXiv 2000

  22. [22]

    InProceedings of the 2013 IEEE Symposium on Security and Privacy (SP ’13)

    SoK: Eternal War in Memory. InProceedings of the 2013 IEEE Symposium on Security and Privacy (SP ’13) . IEEE Computer Society. Gang Tan

    work page 2013

  23. [23]

    In 2015 IEEE Symposium on Security and Privacy

    CHERI: A Hybrid Capability-System Architecture for Scalable Software Compartmentalization. In 2015 IEEE Symposium on Security and Privacy . 20–37. https://doi.org/10.1109/SP.2015.9 WebAssembly. [n.d.]. WebAssembly System Interface. https://github.com/WebAssembly/wasi. Wei Xu, Daniel C. DuVarney, and R. Sekar

    work page doi:10.1109/sp.2015.9 2015