MEP-41 Research Substrate: Memory Safety Advances 2023–May 2026
MEP-41 Research Substrate: Memory Safety Advances 2023–May 2026
Tag
Memory-Safety
65 notes
Android Scudo + MTE inside ART
The canonical "secure allocator inside a managed runtime." Scudo is Android's hardened native heap, used for ART's non-managed allocations (JIT code, off-heap buffers, JNI). Pairs with ARM MTE on Armv9 hardware for hardware-checked tagging. Default for all native allocations on Android since 11.
Spectre Mitigations in Hosted JITs
Speculative-execution attacks haven't gone away. As of May 2026, every shipping JIT either implements index masking + bounds-check hardening, or relies on process-level Site Isolation, or both. The consensus: software mitigations alone are necessary but not sufficient; hardware (eIBRS, BHI controls, CET-IBT) carries the load on CPUs that have it.
W^X Enforcement in Modern JITs
What every shipping JIT must do on day 1 to be production-grade: never have a code page that is both writable and executable to the same thread at the same time. MAP_JIT + pthread_jit_write_protect_np on Apple Silicon, mprotect dance elsewhere, hardware shadow stacks (Intel CET, ARM BTI) increasingly mandatory.
V8 Pointer Compression Cage
A direct ancestor of vm3's 32-bit slab index. V8 squeezes 64-bit pointers down to 32-bit offsets within a per-isolate 4 GB virtual region (the "cage"). Cut V8's heap by 43%, Chrome renderer memory by 20%.
Inko — Singly-Owned Values
Single ownership with deterministic destruction, multiple simultaneous borrows allowed, runtime borrow-count enforcement. No GC, no compile-time borrow checker, no lifetime variables. Concurrency uses `uni T` (unique values) for safe inter-process transfer.
WasmGC
Native GC primitives in a portable bytecode. Ratified in Wasm 3.0 (Sep 2025), shipped in all major browsers by Dec 2024. Dart, Kotlin, OCaml, Java/Scala/Scheme can now compile to Wasm without bundling a GC.
Scala 3 Capture Checking
Capability tracking in the type system. Each value's type may carry a capture set listing which capabilities it could reference. Foundation for capability-based effects, separation checking (System Capybara), and ownership for resources.
WebAssembly Segmented Memory (and friends)
The CG-track answer to "what's beyond a single 4 GB linear memory?" Multiple memories shipped in Wasm 3.0 (Sep 2025). Memory64 shipped at the same time. A formal "segmented memory" proposal in the MSWasm vein has not yet entered the CG track but is influencing design.
Use-After-Free Landscape: Temporal vs Spatial, kCFI, and the Proven-by-Construction Story
The 2024-2026 industry picture on temporal memory safety, kernel mitigations, and the convergence of UAF defences.
Linear Haskell
Linearity attached to function arrows, not to types. Backwards-compatible: ordinary code continues to type-check unchanged. Experimental since GHC 9.0; still labelled experimental in 9.12 / 9.15 (2024–2026).
Intel LAM (Linear Address Masking) and the x86 top-byte-tag story
Intel LAM (Linear Address Masking) and the x86 top-byte-tag story
Capability-Machine Formalism and Endorsement Relations
Cerise, the CHERI-C Coq memory model, and capability-safety logical relations as the formal model behind handle-based runtimes.
Separation Logic for Managed (GC'd) Heaps
Iris-based separation logics with space credits, tracing GC, and the 2025 IrisFit + Nextgen-Modality lines.
Scudo & friends: hardened allocators in production
Scudo & friends: hardened allocators in production
MSWasm — Memory-Safe WebAssembly
A WebAssembly extension that replaces linear memory with segments and handles. Handles are unforgeable, typed pointers carrying bounds and provenance — closely modelled on CHERI capabilities but pure software.
Jane Street OxCaml — Modes (Uniqueness, Locality, Linearity)
Orthogonal modes layered onto OCaml's type system. Mode is a property of a value, separate from its type, tracked through inference. Production in Jane Street; open-sourced as OxCaml in 2025.
curl, Daniel Stenberg, and the "Is C/C++ The Actual Problem?" Debate
Stenberg's curl CVE data, the Hyper / Rust experiment, and the unresolved 2026 question of whether memory-safe languages are the whole answer.
V8 Sandbox
A purely software in-process sandbox for the V8 JS heap. Ban raw pointers, replace with offsets into a 1 TB sandbox region and indices into out-of-sandbox pointer tables. About 1% perf cost, enabled by default in Chrome 123. Every modern JIT is moving this direction.
Swift consuming / borrowing / inout & Noncopyable Types
Swift 6.x has shipped a complete move-only/noncopyable system layered on top of ARC. Parameter conventions are explicit; the law of exclusivity (Swift's variant from 2017) supplies the static aliasing discipline.
MarkUs and quarantine-style UAF prevention
MarkUs and quarantine-style UAF prevention
Formal Models of the Rust Borrow Checker
Stacked Borrows, the 2025 Tree Borrows replacement, and the trajectory of NLL / two-phase formalisation.
Chrome Memory-Safety Data and the Rust-in-Chrome Rollout
Chrome Security's published per-quarter memory-safety data for 2024-2026, the JSON / PNG / fonts Rust rollouts, and the V8 sandbox.
V8 — Orinoco + Oilpan
Chrome's two cooperating collectors. Orinoco runs V8's young-generation JS heap in parallel; Oilpan is Blink's traced C++ GC, recently hosted inside V8 as a library, learning to do generational collection with conservative stack scanning.
Project Verona Regions
Microsoft Research's experimental concurrent-ownership language. Ownership is over **regions** (groups of objects) instead of individual objects. Cowns (concurrent owners) serialise access; behaviours schedule work over multiple cowns atomically.
Intel CET Shadow Stack + IBT
Intel CET Shadow Stack + IBT
EU Cyber Resilience Act and Memory Safety
The CRA's 2026-2027 enforcement timeline and the implicit pressure toward memory-safe languages.
CakeML and the Verified-JIT Line
The bootstrapping verified ML compiler, its 2024 PLDI agenda, and the FM-JIT verified-JIT effort that builds on it.
Pony Reference Capabilities
Six capabilities (iso, trn, ref, val, box, tag) make actor-based concurrency data-race-free at compile time. Production at WallarooLabs and Microsoft; foundation for Verona's region work.
JavaScriptCore — Riptide
WebKit's retreating-wavefront concurrent garbage collector. Marks objects while JS runs, throttles allocation when it falls behind, and uses logical versioning to skip clearing bitmaps.
DoD Safe Coding Practices and Military / Aerospace Memory-Safety Procurement (2024-2026)
The DoD's evolving acquisition posture on memory-safe languages, the SWFT framework, and aerospace coding standards.
CompCert and the Verified-Compiler Toolchain
The production-grade formally verified C compiler, the CompCertO / Owlang line, and why it matters for JIT verification.
Arm PAC + BTI
Arm PAC + BTI
White House ONCD "Back to the Building Blocks" (February 2024)
The White House Office of the National Cyber Director's memory-safety report and the C/C++-adverse federal stance.
MTE in a Managed Runtime
MTE in a Managed Runtime
MMTk and LXR
A research framework that cleanly separates GC plans from policies, plus the LXR collector that proves a stop-the-world RC+mark-region design can beat industrial concurrent GCs on tail latency.
Austral
Strict linear types as the load-bearing primitive for memory and protocol safety, plus capability-based effect control. Spec-and-compiler-small enough to read in a weekend.
Aeneas
Rust verification by functional translation: compile Rust to a pure lambda calculus, verify there.
ZGC — Generational, Colored-Pointer GC (OpenJDK)
Java's flagship low-latency collector. Sub-millisecond pauses on multi-TB heaps via colored 64-bit pointers and concurrent everything.
NSA "Software Memory Safety" Guidance (2022) and the June 2025 Reissue
The NSA's formal language-level guidance, the named-language list, and the joint CISA reissue.
Mojo (2026)
A Rust-like ownership system with simpler call-site syntax, taped onto a Python-shaped surface, sitting on MLIR, headed to open source in fall 2026.
Kani
AWS's bit-precise bounded model checker for Rust, deployed in CI on Firecracker and the standard library.
Arm MTE
Arm MTE
Lobster — Compile-Time Reference Counting
A pragmatic language by Wouter van Oortmerssen that elides 95% of refcount ops at compile time through flow-typed lifetime analysis. Cycles handled by a cleanup at program exit.
Hylo (formerly Val)
Mutable value semantics with subscript-based projection borrowing, no lifetime variables, and the Law of Exclusivity enforced at call sites.
Creusot
A deductive verifier for safe Rust that compiles to Why3 and discharges to off-the-shelf SMT solvers.
CISA Secure-by-Design Pledge and the January 2026 Memory-Safety Deadline
The voluntary US federal pledge that has set the de-facto industry baseline for memory-safety roadmaps.
CHERIoT
CHERIoT
Verus
Microsoft Research's SMT-backed Rust verifier, the leading tool for verified systems software at scale in 2025-2026.
Vale Generational References
The direct intellectual ancestor of vm3's handle design: a per-allocation generation counter, a per-reference remembered generation, and a check on every dereference. Same idea, different layer.
Roc — Perceus in production-ish
The biggest real-world deployment of Perceus reference counting, layered with Morphic alias analysis and "seamless slices" so functional code rarely allocates.
Google: Android Rust, Chrome Rust, V8 Sandbox
Google's published 2022-2026 data on memory-safety progress — Android's 76% → <20% trajectory, the CVE-2025-48530 near-miss, the V8 sandbox.
Arm Morello
Arm Morello
RustBelt and Iris
Foundational separation-logic verification of Rust's safe / unsafe core, and its 2024-2026 RefinedRust successor.
Rust Polonius (2026)
The state of Rust's borrow checker as the Polonius "alpha" lands behind a nightly feature gate, and what a non-ownership language can still steal from it.
Perceus (Koka)
"Garbage-free" precise reference counting with reuse — in-place updates without locks, statically inserted at compile time.
Microsoft "70% of CVEs Are Memory Safety" Statistic
The canonical industry data point on memory-safety vulnerability prevalence, and every follow-up through 2026.
CHERI (Next Generation)
CHERI (Next Generation)
Industry, Policy, and Deployment Data
Microsoft 70%, Google/Android Rust, CISA Secure-by-Design (Jan 2026), NSA CSI, ONCD, DoD SWFT, EU CRA, Chrome CVE data, curl, UAF landscape.
Formal Verification and Mechanized Safety
RustBelt/Iris, Verus, Creusot, Kani, Aeneas, CompCert, CakeML, Stacked/Tree Borrows, separation logic for managed heaps, capability-machine logics.
Runtime Techniques and Sandboxed Memory
Perceus/Koka, Roc, Lobster, generational ZGC, MMTk LXR, JSC Riptide, V8 Oilpan/Sandbox, MSWasm, WasmGC, V8 cage, W^X / JIT hardening, Spectre/JIT mitigations.
Ownership, Borrowing, Reference Modes
Rust+Polonius, Vale generational references, Hylo, Mojo, Austral, Pony, Project Verona, Swift, OxCaml, Linear Haskell, Scala 3 capture checking, Inko.
Hardware Capability Machines and Tagged Memory
CHERI, Morello, CHERIoT, MTE, Apple MIE, PAC/BTI, Intel CET, MarkUs, Scudo, Intel LAM.
Overview
Broad research substrate for MEP-41: a 12-thread literature/systems survey of memory-safety advances 2023-2026.
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).