Skip to content

Memory Management

Research substrate for Mochi MEP-41 (May 2026). A 57-file deep dive into memory-safety advances from 2023 to mid-2026: capability hardware, generational references, ownership systems, runtime techniques, formal verification, and industry policy (CISA / NSA / ONCD).

memory-safety research mep-41

Background research for Mochi MEP-41: the memory-safety positioning that frames Mochi’s vm3 runtime as a Vale generational reference machine, an MSWasm capability ABI, and a kalloc_type / xzone typed allocator, all under one roof.

Each subsection drills into one thread of the 2023-2026 memory-safety landscape. Every file has a §1 Provenance with canonical URLs, a §2 Mechanism, a §3 status as of May 2026, an engineering-cost section, a Mochi adaptation note, and §7 open questions.

Sections

  1. Overview — the 12-thread sweep across hardware, runtime, ownership, verification, and industry policy.
  2. Hardware — CHERI, Morello, CHERIoT 1.0, MTE, Apple MIE (iPhone 17, Sept 2025), PAC/BTI, Intel CET, MarkUs, Scudo.
  3. Ownership — Rust+Polonius, Vale, Hylo, Mojo, Austral, Pony, Verona, Swift, OxCaml, Linear Haskell, Scala 3, Inko.
  4. Runtime — Perceus, Roc, Lobster, ZGC, MMTk LXR, JSC Riptide, V8 Oilpan, V8 Sandbox, MSWasm, WasmGC, JIT hardening.
  5. Verification — RustBelt/Iris, Verus, Creusot, Kani, Aeneas, CompCert, CakeML, capability-machine logics.
  6. Industry — Microsoft 70%, Google/Android Rust crossover, CISA Secure-by-Design (Jan 2026 deadline), NSA CSI, ONCD, DoD SWFT, EU CRA.
OverviewBroad research substrate for MEP-41: a 12-thread literature/systems survey of memory-safety advances 2023-2026.
1 pages · 23 min
Hardware Capability Machines and Tagged MemoryCHERI, Morello, CHERIoT, MTE, Apple MIE, PAC/BTI, Intel CET, MarkUs, Scudo, Intel LAM.
10 pages · 66 min
Ownership, Borrowing, Reference ModesRust+Polonius, Vale generational references, Hylo, Mojo, Austral, Pony, Project Verona, Swift, OxCaml, Linear Haskell, Scala 3 capture checking, Inko.
12 pages · 61 min
Runtime Techniques and Sandboxed MemoryPerceus/Koka, Roc, Lobster, generational ZGC, MMTk LXR, JSC Riptide, V8 Oilpan/Sandbox, MSWasm, WasmGC, V8 cage, W^X / JIT hardening, Spectre/JIT mitigations.
15 pages · 80 min
Formal Verification and Mechanized SafetyRustBelt/Iris, Verus, Creusot, Kani, Aeneas, CompCert, CakeML, Stacked/Tree Borrows, separation logic for managed heaps, capability-machine logics.
10 pages · 51 min
Industry, Policy, and Deployment DataMicrosoft 70%, Google/Android Rust, CISA Secure-by-Design (Jan 2026), NSA CSI, ONCD, DoD SWFT, EU CRA, Chrome CVE data, curl, UAF landscape.
10 pages · 56 min