#memory-safety

DoD Safe Coding Practices and Military / Aerospace Memory-Safety Procurement (2024-2026)

§1 Provenance US Air & Space Forces Magazine, "DOD Plans Quicker Cybersecurity Contractor Standards" (April 2025). https://www.airandspaceforces.com/dod-quicker-contractors-cybersecurity-standards/ Rob Vietmeyer (DoD Chief Software Officer) public remarks, April 2025. Industrial Cyber: "US DoD gets set to develop SWFT framework, issues RFIs to advance secure software development" . https://industrialcyber.co/regulation-standards-and-compliance/us-dod-gets-set-to-develop-swft-framework-issues-rfis-to-advance-secure-software-development-and-authorization/ CMU Software Engineering Institute. "Supporting the Use of CERT Secure Coding Standards in DoD Acquisitions" . https://resources.sei.cmu.edu/library/asset-view.cfm?assetid=28033 CISA / NSA. "The Case for Memory...

ZGC — Generational, Colored-Pointer GC (OpenJDK)

§1 Provenance OpenJDK Z Garbage Collector. Engineering lead: Per Liden (originally), Stefan Karlsson, Erik Österlund at Oracle. Key JEPs: JEP 333 (2018) — original experimental ZGC. JEP 377 (JDK 15, 2020) — production-ready. JEP 439 (JDK 21, Sep 2023) — Generational ZGC, opt-in. JEP 474 (JDK 23, 2024) — Generational mode by default; non-generational mode deprecated. JDK 25 (Sep 2025, LTS) — generational-only ZGC. Project home: https://openjdk.org/projects/zgc/ , wiki https://wiki.openjdk.org/spaces/zgc/pages/34668579/Main...

Overview

Perceus (Koka)

§1 Provenance Alex Reinking, Ningning Xie, Leonardo de Moura, Daan Leijen. "Perceus: Garbage Free Reference Counting with Reuse." PLDI 2021 , ACM SIGPLAN Conf. on Programming Language Design and Implementation, June 2021. Distinguished Paper. Extended TR: Microsoft Research MSR-TR-2020-42, Nov 2020 (v4 2021-06-07). Follow-up: Lorenzen, Leijen. "Reference Counting with Frame Limited Reuse" (ICFP 2022 / TR 2021). Most recent: Leijen, Lorenzen. "Tail recursion modulo context: an equational approach (extended version),"...

Android Scudo + MTE inside ART

§1 Provenance Scudo. Originally LLVM's hardened allocator (sub-project of compiler-rt's sanitizer family). Maintainer: Kostya Kortchinsky and others. Brought to Android by Google. AOSP doc: https://source.android.com/docs/security/test/scudo . Android Developers blog: https://android-developers.googleblog.com/2020/06/system-hardening-in-android-11.html (Scudo default from Android 11). Arm MTE. Armv8.5-A feature, mainline in Armv9. AOSP: https://source.android.com/docs/security/test/memory-safety/arm-mte . Android Developers: https://developer.android.com/ndk/guides/arm-mte . LLVM review for MTE in Scudo: https://reviews.llvm.org/D70762 . Security analyses: WOOT 2024 — "Exploiting Android's Hardened Memory Allocator" (Mao et al.);...

CISA Secure-by-Design Pledge and the January 2026 Memory-Safety Deadline

§1 Provenance CISA Secure by Design page: https://www.cisa.gov/securebydesign CISA Secure by Design Pledge: https://www.cisa.gov/securebydesign/pledge Pledge signers list: https://www.cisa.gov/securebydesign/pledge/secure-design-pledge-signers "Product Security Bad Practices" publication (Oct 2024, updated): https://www.ic3.gov/CSA/2024/241016-2.pdf ; CISA page https://www.cisa.gov/resources-tools/resources/product-security-bad-practices CISA Secure by Design Pledge Progress Reports: https://www.cisa.gov/securebydesign/pledge/progress-reports Original announcement (May 2024): "CISA Announces Secure by Design Commitments from Leading Technology Providers" . https://www.cisa.gov/news-events/news/cisa-announces-secure-design-commitments-leading-technology-providers Industry analysis: DEVOPSdigest, "Fix It or Face the Consequences: CISA's Memory-Safe Muster" . https://www.devopsdigest.com/fix-it-or-face-the-consequences-cisas-memory-safe-muster RunSafe...

CHERI (Next Generation)

Hardware capabilities: 128-bit fat pointers with bounds, permissions and an out-of-band tag, enforced by the ISA. §1 Provenance Watson, Chisnall, Clarke, Davis, Filardo, Laurie, Moore, Neumann, Richardson, Sewell, Witaszczyk, Woodruff. "CHERI: Hardware-Enabled C/C++ Memory Protection at Scale." IEEE Security & Privacy , vol. 22 no. 4, July/Aug 2024, pp. 50-61. DOI 10.1109/MSEC.2024.3396701 (IEEE CS 2024 Best Paper Award for S&P Magazine). https://www.cl.cam.ac.uk/research/security/ctsrd/pdfs/20240419-ieeesp-cheri-memory-safety.pdf Watson et al. "Capability Hardware Enhanced RISC Instructions:...

Aeneas

§1 Provenance Ho & Protzenko. "Aeneas: Rust verification by functional translation" , ICFP 2022 / PACMPL 6. https://dl.acm.org/doi/10.1145/3547647 ; arXiv https://arxiv.org/abs/2206.07185 Ho, Fromherz, Protzenko. "Sound Borrow-Checking for Rust via Symbolic Semantics" , ICFP 2024. https://icfp24.sigplan.org/details/icfp-2024-papers/17/Sound-Borrow-Checking-for-Rust-via-Symbolic-Semantics Project: https://github.com/AeneasVerif/aeneas (Inria + Microsoft Research). Frontend: Charon → LLBC. Backends: F*, Coq, HOL4, Lean (Lean is the maintainers' primary 2024-2026 target). Lean integration documentation: https://lean-lang.org/use-cases/aeneas/ Used in production: Microsoft's port of SymCrypt (the Windows...

WebAssembly Segmented Memory (and friends)

§1 Provenance WebAssembly Community Group (CG) and Working Group (WG). W3C process. Wasm 3.0 specification — W3C Recommendation, September 24, 2025. Bundles 9 features: WasmGC, exception handling, tail calls, memory64 , multiple memories , 128-bit SIMD, relaxed-SIMD, extended-const, JS Promise integration. Proposal repos: https://github.com/WebAssembly/memory64 (phase 4 → merged) https://github.com/WebAssembly/multi-memory (phase 4 → merged) https://github.com/WebAssembly/proposals (master proposal list and status) Discussion on integration: https://github.com/WebAssembly/design/issues/1036 . Status overview: https://webassembly.org/features/ . §2 Mechanism...

Separation Logic for Managed (GC'd) Heaps

§1 Provenance McCreight et al. "GCSL: A logic for low-level programs with GC interfaces" (foundational, pre-Iris). https://ieeexplore.ieee.org/document/5970244/ Madiot & Pottier. "A Separation Logic for Heap Space under Garbage Collection" , POPL 2022 / PACMPL 6. https://dl.acm.org/doi/10.1145/3498672 ; PDF https://cambium.inria.fr/~fpottier/publis/madiot-pottier-diamonds-2022.pdf Charguéraud, Moine, Pottier. "A High-Level Separation Logic for Heap Space under Garbage Collection" , POPL 2023 / PACMPL 7. https://dl.acm.org/doi/10.1145/3571218 ; PDF https://www.chargueraud.org/research/2022/space_with_gc/space_with_gc.pdf Moine, Charguéraud, Pottier. "Will It Fit? Verifying Heap...

Intel CET Shadow Stack + IBT

A hardware second stack that records return addresses, plus indirect-branch landing pads. Shipping on every modern Intel/AMD CPU, default-on in Windows 11, opt-in on Linux. §1 Provenance Intel, "Control-flow Enforcement Technology Specification." Document 334525, Rev. 3. https://kib.kiev.ua/x86docs/Intel/CET/334525-003.pdf Linux kernel "Control-flow Enforcement Technology (CET) Shadow Stack" docs (v6.14+). https://docs.kernel.org/next/x86/shstk.html LWN, "Shadow stacks for userspace." Sept 2022. https://lwn.net/Articles/913934/ Phoronix, "Glibc Updated For Recent Linux CET Shadow Stack Support." Jan 2024. https://www.phoronix.com/news/Glibc-Intel-CET-Shadow-Stack McGarr,...

Use-After-Free Landscape: Temporal vs Spatial, kCFI, and the Proven-by-Construction Story

§1 Provenance MITRE CWE Top 25. CWE-416 (Use After Free) ranked 7th in 2022, 4th in 2023, remains in the top 25 in 2024-2025. White House ONCD, "Back to the Building Blocks" (Feb 2024) — formalises spatial vs temporal vulnerability distinction. IEEE Security & Privacy 2024, "Full Spatial and Temporal Memory Safety for C" , Rutgers. https://people.cs.rutgers.edu/~sn349/papers/safety-sp-2024.pdf CMU SEI, "AI-Powered Memory Safety with the Pointer Ownership Model" . https://www.sei.cmu.edu/blog/ai-powered-memory-safety-with-the-pointer-ownership-model/ RunSafe...

V8 Pointer Compression Cage

§1 Provenance V8 team at Google. Igor Sheludko, Toon Verwaest, Tobias Tebbi et al. Blog post (canonical): https://v8.dev/blog/pointer-compression . Oilpan companion: https://v8.dev/blog/oilpan-pointer-compression . Shipped initially in V8 v8.0; default-on V8 v9.2 (shared-cage mode). Multi-cage / IsolateGroups: Dmitry Bezhetskov, https://dbezhetskov.dev/multi-sandboxes/ . Related: Node.js issue tracker #55735 on multi-cage isolate groups. §2 Mechanism V8's heap pointers used to be raw 64-bit Object* . Pointer compression replaces them with 32-bit "compressed pointers" (...

CompCert and the Verified-Compiler Toolchain

§1 Provenance Leroy. "Formal verification of a realistic compiler" , CACM 2009; full development https://compcert.org ; source https://github.com/AbsInt/CompCert ACM Software System Award 2022, ACM SIGPLAN Programming Languages Software Award. CompCertO line: Koenig & Shao, "CompCertO: Compiling Certified Open C Components" , PLDI 2021; Zhang, Wang, Wu, Koenig, Shao, "Fully Composable and Adequate Verified Compilation with Direct Refinements between Open Modules" , POPL 2024. CompCertOC (PLDI 2025): verified compilation of multi-threaded...

curl, Daniel Stenberg, and the "Is C/C++ The Actual Problem?" Debate

§1 Provenance Daniel Stenberg blog: https://daniel.haxx.se/blog/ Stenberg, "half of curl's vulnerabilities are C mistakes" , March 2021. https://daniel.haxx.se/blog/2021/03/09/half-of-curls-vulnerabilities-are-c-mistakes/ Stenberg, December 2024 follow-up post (URL pattern: https://daniel.haxx.se/blog/2024/12/12/) , discussing CVE-2024-11053 and updating the C-attributable percentage to ~40%. The New Stack, "Curl's Daniel Stenberg on Securing 180,000 Lines of C Code" . https://thenewstack.io/curls-daniel-stenberg-on-securing-180000-lines-of-c-code/ Software Engineering Radio episode 688 (Oct 2025), "Daniel Stenberg on Removing Rust from Curl" . https://se-radio.net/2025/10/se-radio-688-daniel-stenberg-on-removing-rust-from-curl/ Slideshare deck, "rust...

Jane Street OxCaml — Modes (Uniqueness, Locality, Linearity)

§1 Provenance Vendor : Jane Street Capital, in collaboration with Tarides on the upstream merge. Project : OxCaml — open-source branch of OCaml. Announced/rebranded July 2025. Repo: ocaml-flambda/ocaml-jst . Docs : https://oxcaml.org/documentation/modes/intro/ . Blog series "Oxidizing OCaml" : Locality: https://blog.janestreet.com/oxidizing-ocaml-locality/ Rust-Style Ownership: https://blog.janestreet.com/oxidizing-ocaml-ownership/ Data Race Freedom: https://blog.janestreet.com/oxidizing-ocaml-parallelism/ Data-race-freedom proposal in tree : https://github.com/ocaml-flambda/ocaml-jst/blob/main/jane/doc/proposals/data-race-freedom.md . 2025 community write-up : Tarides, "Introducing Jane Street's OxCaml Branch!", https://tarides.com/blog/2025-07-09-introducing-jane-street-s-oxcaml-branch/ . Production milestone : ICFP...

Memory Management

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...

NSA "Software Memory Safety" Guidance (2022) and the June 2025 Reissue

§1 Provenance NSA. "Software Memory Safety" Cybersecurity Information Sheet, November 2022. https://www.nsa.gov/Press-Room/News-Highlights/Article/Article/3215760/nsa-releases-guidance-on-how-to-protect-against-software-memory-safety-issues/ NSA + CISA joint CSI. "Memory Safe Languages: Reducing Vulnerabilities in Modern Software Development" , June 2025. U/OO/172709-25 | PP-25-2574. https://media.defense.gov/2025/Jun/23/2003742198/-1/-1/0/CSI_MEMORY_SAFE_LANGUAGES_REDUCING_VULNERABILITIES_IN_MODERN_SOFTWARE_DEVELOPMENT.PDF CISA alert (June 24, 2025): "New Guidance Released for Reducing Memory-Related Vulnerabilities" . https://www.cisa.gov/news-events/alerts/2025/06/24/new-guidance-released-reducing-memory-related-vulnerabilities NSA press release on the 2025 CSI: https://www.nsa.gov/Press-Room/Press-Releases-Statements/Press-Release-View/Article/4223298/ CISA / NSA joint "The Case for Memory Safe Roadmaps" (2023). Coverage: The Register, "CISA,...

WasmGC

§1 Provenance WasmGC. Proposal repo: https://github.com/WebAssembly/gc . Champions: Andreas Rossberg (Mozilla, retd.), Francis McCabe (Google). Standardised as part of WebAssembly 3.0 , W3C Recommendation, September 24, 2025. Earlier: Wasm 2.0 (Dec 2024, W3C REC); WasmGC was post-2.0 work that landed in 3.0. Browser support: Chrome 119 (Oct 2023) Firefox 120 (Nov 2023) Safari 18.2 (Dec 2024) — last to ship, unblocking GC-language deployment. §2 Mechanism WasmGC adds typed managed references...

Hylo (formerly Val)

§1 Provenance Authors : Dimitri Racordon, Dave Abrahams, Sean Parent, et al. Originally proposed in WG21 paper P2676R0 (Oct 2022), https://www.open-std.org/jtc1/sc22/wg21/docs/papers/2022/p2676r0.pdf . Project home : https://hylo-lang.org/ . Tour: https://docs.hylo-lang.org/language-tour/ . Specification: https://github.com/hylo-lang/specification/blob/main/spec.md . Renamed Jan 2024 : Val → Hylo, to disambiguate from other "Val" projects. Object-model doc for Swift designers : https://github.com/hylo-lang/Documentation/blob/main/object-model-for-swift-designers.md . Discussion on Rust comparison : https://github.com/orgs/hylo-lang/discussions/788 . §2 Core type discipline Hylo has only value types....

Runtime Techniques and Sandboxed Memory

Spectre Mitigations in Hosted JITs

§1 Provenance Spectre v1 (Bounds Check Bypass) and Spectre v2 (Branch Target Injection) disclosed Jan 2018, Kocher et al. WebKit's response: https://webkit.org/blog/8048/what-spectre-and-meltdown-mean-for-webkit/ (2018), still architecturally accurate. Chrome's response: Site Isolation (out-of-process iframes); Spectre-aware codegen in V8. Intel guidance: https://www.intel.com/content/www/us/en/developer/articles/technical/software-security-guidance/technical-documentation/runtime-speculative-side-channel-mitigations.html , https://www.intel.com/content/www/us/en/developer/articles/technical/software-security-guidance/technical-documentation/branch-history-injection.html . Linux kernel mitigations: https://docs.kernel.org/admin-guide/hw-vuln/spectre.html . Recent attacks: PB-Inception (2025), BHI variants (2024-2025), CVE-2024-28956, CVE-2025-24495. §2 Mechanism Spectre attacks induce the CPU to speculatively execute instructions that wouldn't run...

Intel LAM (Linear Address Masking) and the x86 top-byte-tag story

Let userspace stash metadata in the unused high bits of a 64-bit pointer. Intel calls it LAM; AMD calls it UAI; Arm has had TBI since v8.0. SLAM (2024) almost killed Linux's LAM support. §1 Provenance Intel SDM, Vol 3 Ch 7, "Linear Address Masking (LAM)." https://www.intel.com/content/www/us/en/developer/articles/technical/intel-sdm.html LWN, "Support for Intel's Linear Address Masking." Aug 2022. https://lwn.net/Articles/902094/ LWN, "Linear Address Masking enabling." Oct 2022. https://lwn.net/Articles/911572/ LWN, "Linear Address Masking (LAM)...

Swift consuming / borrowing / inout & Noncopyable Types

§1 Provenance Vendor : Apple. Swift Evolution. Foundational law : SE-0176 Enforce Exclusive Access to Memory (Swift 5, 2017–2018). Parameter modifiers : SE-0377 borrowing / consuming parameter ownership modifiers , https://github.com/swiftlang/swift-evolution/blob/main/proposals/0377-parameter-ownership-modifiers.md . Noncopyable foundation : SE-0390 Noncopyable structs and enums , https://github.com/swiftlang/swift-evolution/blob/main/proposals/0390-noncopyable-structs-and-enums.md . Generics : SE-0427 Noncopyable Generics , https://github.com/swiftlang/swift-evolution/blob/main/proposals/0427-noncopyable-generics.md . Pattern matching : SE-0432 Borrowing/consuming pattern matching for noncopyable types . Std lib primitives : SE-0437. 2026 review item...

Formal Models of the Rust Borrow Checker

§1 Provenance Jung, Dang, Kang, Dreyer. "Stacked Borrows: An Aliasing Model for Rust" , POPL 2020 / PACMPL 4. The original operational aliasing semantics for Rust. Villani, Hostert, Dreyer, Jung. "Tree Borrows" , PLDI 2025 / PACMPL 9 Article 188. https://dl.acm.org/doi/10.1145/3735592 ; PDF https://iris-project.org/pdfs/2025-pldi-treeborrows.pdf Distinguished Paper Award , PLDI 2025. Became the most-downloaded PACMPL paper of all time shortly after publication. Background blog: Jung, "From Stacks to Trees: A new...

Formal Verification and Mechanized Safety

EU Cyber Resilience Act and Memory Safety

§1 Provenance European Commission, Cyber Resilience Act main page. https://digital-strategy.ec.europa.eu/en/policies/cyber-resilience-act CRA Reporting Obligations page. https://digital-strategy.ec.europa.eu/en/policies/cra-reporting CRA legislative-text summary. https://digital-strategy.ec.europa.eu/en/policies/cra-summary Hogan Lovells client alert, "EU Cyber Resilience Act: Key 2026 milestones toward CRA compliance" . https://www.hoganlovells.com/en/publications/eu-cyber-resilience-act-getting-ready-for-cra-compliance-in-2026 OpenSSF analysis of the CRA. https://openssf.org/public-policy/eu-cyber-resilience-act/ Keysight, "One Year Countdown to EU CRA Compliance — September 11, 2026, Changes Everything" . https://www.keysight.com/blogs/en/tech/nwvs/2025/09/11/one-year-countdown-to-eu-cra-compliance-september-11-2026-changes-everything ScanReco, "Current state of the EU Cyber Resilience Act — and why no-one...

MEP-41 Research Substrate: Memory Safety Advances 2023–May 2026

A literature/systems review across 12 threads, with concrete adaptation notes for the vm3 handle/arena/generation model. Each topic includes canonical name + venue/year, core mechanism, production status, and a Mochi adaptation hook. This file is the broad overview produced by the parallel research sweep. Per-system deep-dive files live alongside it in: hardware/ — CHERI, Morello, CHERIoT, MTE, MIE, PAC/BTI, CET, MarkUs, Scudo, LAM. ownership/ — Rust+Polonius, Vale, Hylo, Mojo, Austral, Pony,...

Scala 3 Capture Checking

§1 Provenance Lead : Martin Odersky and the EPFL LAMP group. Capture-checking research and Capybara extension led by Oliver Bračevac. Reference docs (experimental) : https://docs.scala-lang.org/scala3/reference/experimental/cc.html . Advanced: https://docs.scala-lang.org/scala3/reference/experimental/cc-advanced.html . Nightly basics: https://nightly.scala-lang.org/docs/reference/experimental/capture-checking/basics.html . Scala Days 2025 talk : Oliver Bračevac (EPFL/LAMP), https://bracevac.org/assets/pdf/scaladays2025_annot.pdf and https://scaladays.org/editions/2025/talks/capture-checking-a-new-approach . Conference papers : "What's in the Box: Ergonomic and Expressive Capture Tracking over Generic Data Structures", OOPSLA 2025 (System Capless). https://2025.splashcon.org/details/OOPSLA/133/ ... "System Capybara: Capture...

Kani

§1 Provenance Project: https://github.com/model-checking/kani ; documentation https://model-checking.github.io/kani/getting-started.html Owned by AWS, open source under MIT/Apache-2.0. Built on the CBMC backend (CPROVER). Production-use case study: AWS Open Source Blog, "Using Kani to Validate Security Boundaries in AWS Firecracker" , 2023, https://model-checking.github.io/kani-verifier-blog/2023/08/31/using-kani-to-validate-security-boundaries-in-aws-firecracker.html Rust standard-library verification initiative (AWS-sponsored, hosted by the Rust Foundation): https://aws.amazon.com/blogs/opensource/verify-the-safety-of-the-rust-standard-library/ ESBMC integration via Goto-Transcoder (Rust Foundation announcement, 2024-2025): https://rustfoundation.org/media/expanding-the-rust-formal-verification-ecosystem-welcoming-esbmc/ Releases through 2025-2026 (Kani 0.61 through 0.66) tracked at https://github.com/model-checking/kani/releases §2...

Arm Morello

The first industrial-scale CHERI silicon: a Neoverse N1 retrofitted with 128-bit capabilities, the closeout of UK DSbD. §1 Provenance Arm Morello programme overview. https://www.arm.com/architecture/cpu/morello UKRI, "DSbD Final Impact Evaluation Report", published October 2025. https://www.ukri.org/wp-content/uploads/2025/10/IUK-131025-2025-07-04_DSbD-Final-Impact-Evaluation-Report.pdf Watson et al., "CHERI: Hardware-Enabled C/C++ Memory Protection at Scale," IEEE S&P Magazine, July/Aug 2024. https://www.cl.cam.ac.uk/research/security/ctsrd/pdfs/20240419-ieeesp-cheri-memory-safety.pdf Grisenthwaite et al., "The Arm Morello Evaluation Platform: Validating CHERI-based Security in a High-performance System." IEEE Micro , 2023. https://www.cl.cam.ac.uk/research/security/ctsrd/pdfs/202305ieeemicro-morello-platform.pdf...

Austral

§1 Provenance Author : Fernando Borretti. Reference site : https://austral-lang.org/ . Spec: https://austral-lang.org/spec . Features: https://austral-lang.org/features . Introduction post : https://borretti.me/article/introducing-austral . Implementation post : https://borretti.me/article/how-australs-linear-type-checker-works (the linear checker is <600 LOC of OCaml). Long essay on why this matters: https://borretti.me/article/type-systems-memory-safety . External comparison : https://verdagon.dev/blog/linear-types-borrowing by Evan Ovadia. HN thread : https://news.ycombinator.com/item?id=34168452 . Repo : https://github.com/austral/austral . §2 Core type discipline Austral has a single concept doing all the...

Capability-Machine Formalism and Endorsement Relations

§1 Provenance Cerise (logsem/cerise): Iris-based Coq mechanisation of a capability machine. https://github.com/logsem/cerise "Cerise: Program Verification on a Capability Machine in the Presence of Untrusted Code" , Journal of the ACM (JACM), 2023. https://dl.acm.org/doi/10.1145/3623510 Park, Pai et al. "A Formal CHERI-C Semantics for Verification" , TACAS 2023; "A CHERI C Memory Model for Verified Temporal Safety" , CPP 2025. CHERI hardware lineage: Watson et al., CHERI ISA reports, with hardware in...

CHERIoT

Microsoft's tiny CHERI: a 32-bit capability profile + RTOS that delivers complete spatial, temporal and compartment safety to microcontrollers, now in commercial silicon. §1 Provenance Amar, Chen, Chisnall, Domke, Filardo, Liu, Norton-Wright, Tao, Watson, Xia. "CHERIoT: Complete Memory Safety for Embedded Devices." MICRO 2023 . https://dl.acm.org/doi/pdf/10.1145/3613424.3614266 — and the matching uArch paper, IEEE Micro 2023. https://www.cl.cam.ac.uk/research/security/ctsrd/pdfs/202310ieeemicro-cheriot-uarch.pdf "CHERIoT Architecture Specification v1.0." https://cheriot.org/cheriot-sail/cheriot-architecture.pdf Chisnall et al. "CHERIoT RTOS: An OS for Fine-Grained...

RustBelt and Iris

§1 Provenance Original paper: Jung, Jourdan, Krebbers, Dreyer. "RustBelt: Securing the Foundations of the Rust Programming Language" , POPL 2018 (PACMPL 2). https://dl.acm.org/doi/10.1145/3158154 Underlying logic: Jung, Krebbers, Jourdan, Bizjak, Birkedal, Dreyer. "Iris from the ground up" , JFP 2018; received the 2025 Most Influential POPL Paper Award and the 2023 Alonzo Church Award. Project home: https://plv.mpi-sws.org/rustbelt/ (MPI-SWS). The ERC RustBelt project formally ended April 2021 but the line continues. Major...

Scudo & friends: hardened allocators in production

The bag-of-tricks malloc (guard pages, sized buckets, randomisation, double-free detection) that ships on every Android device and most of Chrome. §1 Provenance LLVM, "Scudo Hardened Allocator." https://llvm.org/docs/ScudoHardenedAllocator.html Android Open Source Project, "Scudo." https://source.android.com/docs/security/test/scudo Serebryany et al., "GWP-ASan: Sampling-Based Detection of Memory-Safety Bugs in Production." ASPLOS 2024 . arXiv 2311.09394. https://arxiv.org/html/2311.09394v2 Chromium Project, "GWP-ASan: Sampling heap memory error detection in-the-wild." https://www.chromium.org/Home/chromium-security/articles/gwp-asan/ Google tcmalloc GWP-ASan docs. https://google.github.io/tcmalloc/gwp-asan.html Chromium PartitionAlloc docs. https://chromium.googlesource.com/chromium/src.git/+/HEAD/base/allocator/partition_allocator/PartitionAlloc.md struct/HardenedPartitionAlloc...

Vale Generational References

§1 Provenance Author : Evan Ovadia. Canonical write-up : "Vale's Memory Safety Strategy: Generational References and Regions", https://verdagon.dev/blog/generational-references (originally Aug 2021, updated July 9 2023). Earlier v1 at https://verdagon.dev/blog/generational-references-v1 . Project page : https://vale.dev/vision/safety-generational-references and the Linear-Aliasing Model, https://vale.dev/linear-aliasing-model . Memory Safety Grimoire (Apr 24 2024): a survey of 14 memory-safety techniques, https://verdagon.dev/grimoire/grimoire . 2024 follow-up : "Zero-Cost Memory Safety with Vale Regions, Part 1: Immutable Region Borrowing", https://verdagon.dev/blog/zero-cost-borrowing-regions-part-1-immutable-borrowing ....

W^X Enforcement in Modern JITs

§1 Provenance Apple Silicon model. Apple Platform Security guide and: https://developer.apple.com/documentation/apple-silicon/porting-just-in-time-compilers-to-apple-silicon . Apple Silicon enforces per-thread W^X via the M-series memory permissions extension. Hardened Runtime entitlements. com.apple.security.cs.allow-jit , com.apple.security.cs.allow-unsigned-executable-memory , the newer jit-write-allowlist . https://developer.apple.com/documentation/BundleResources/Entitlements/com.apple.security.cs.allow-jit . JSC pioneered the MAP_JIT + pthread_jit_write_protect_np pattern in 2015; Firefox, V8, .NET, asmjit followed. Intel CET. https://www.intel.com/content/www/us/en/developer/articles/technical/software-security-guidance/technical-documentation/speculative-execution-side-channel-mitigations.html , kernel docs https://www.kernel.org/doc/html/next/x86/shstk.html . Default-enabled on Windows since W10 19H1 and Linux since 6.4 (2023). ARM...

Pony Reference Capabilities

§1 Provenance Authors : Sylvan Clebsch (founder), Sebastian Blessing, Sophia Drossopoulou; Imperial College London + Microsoft Research. Tutorial home : https://tutorial.ponylang.io/reference-capabilities/reference-capabilities.html . Foundational paper : Clebsch, Drossopoulou, Blessing, McNeil, "Deny Capabilities for Safe, Fast Actors", AGERE 2015. Subtyping : https://tutorial.ponylang.io/reference-capabilities/capability-subtyping.html . Recovery : https://tutorial.ponylang.io/reference-capabilities/recovering-capabilities.html . Practitioner intro : https://zartstrom.github.io/pony/2016/08/28/reference-capabilities-in-pony.html ; https://bluishcoder.co.nz/2017/07/31/reference_capabilities_consume_recover_in_pony.html . §2 Core type discipline Every reference in Pony has both a type T and a capability cap ....

Arm MTE

Per-16-byte 4-bit lock-and-key tags on every allocation granule, in Armv8.5-A and shipping on Pixel 8/9. §1 Provenance Arm, "Armv8.5 Memory Tagging Extension," whitepaper (2019, rev. 2023). https://developer.arm.com/documentation/108035/latest/Introduction-to-the-Memory-Tagging-Extension Serebryany et al. (Google), "MTE: The promising path forward for memory safety." Google Security Blog, Nov 2023. https://security.googleblog.com/2023/11/mte-promising-path-forward-for-memory.html Google Project Zero, "First handset with MTE on the market." November 2023. https://projectzero.google/2023/11/first-handset-with-mte-on-market.html Android Open Source Project: Arm MTE. https://source.android.com/docs/security/test/memory-safety/arm-mte Android NDK guide: Arm Memory...

Chrome Memory-Safety Data and the Rust-in-Chrome Rollout

§1 Provenance Chrome Security quarterly summaries: https://www.chromium.org/Home/chromium-security/quarterly-updates/ Q1 2024 : https://groups.google.com/a/chromium.org/g/chromium-dev/c/K_HO5LsPDKc Q2 2024 : https://groups.google.com/a/chromium.org/g/chromium-dev/c/cMM7RIc1kZI Q3 2024 : https://groups.google.com/a/chromium.org/g/chromium-dev/c/KOmfh5BW6Mw Q3 2025 : https://groups.google.com/a/chromium.org/g/security-dev/c/s-UR_4pJvOY Chromium memory-safety policy page: https://www.chromium.org/Home/chromium-security/memory-safety/ V8 Sandbox README: https://chromium.googlesource.com/v8/v8.git/+/refs/heads/main/src/sandbox/README.md 2025 vulnerability landscape: Quttera, "Inside Chrome's 2025 Vulnerability Landscape: 80 CVEs Revealed in V8 and Core Components" . https://blog.quttera.com/post/inside-chrome-80-vulnerabilities-since-jan-2025 Penligent AI, "Chrome Zero-Day Vulnerabilities Exploited in 2025" (CVE-2025-14174 analysis). https://www.penligent.ai/hackinglabs/chrome-zero-day-vulnerabilities-exploited-in-2025-a-comprehensive-analysis-of-cve-2025-14174-v8-type-confusion-and-sandbox-escapes/ §2 Data Chrome's published memory-safety rollout (selected highlights,...

Hardware Capability Machines and Tagged Memory

MMTk and LXR

§1 Provenance MMTk (Memory Management Toolkit). Stephen M. Blackburn et al., ANU. Originally a Java framework (Blackburn, Cheng, McKinley, 2004), rewritten in Rust as mmtk-core (~2018-present). https://www.mmtk.io/ , https://github.com/mmtk/mmtk-core . LXR — "Low-Latency, High-Throughput Garbage Collection." Wenyu Zhao, Stephen M. Blackburn, Kathryn S. McKinley. PLDI 2022 , San Diego, June 2022, pp. 76-91. https://www.steveblackburn.org/pubs/papers/lxr-pldi-2022.pdf . Recent follow-up: Zhao, Blackburn, McKinley, "Work Packets: A New Abstraction for GC Software Engineering, Optimization,...

MSWasm — Memory-Safe WebAssembly

§1 Provenance Michael, Gollamudi, Bosamiya, Johnson, Denlinger, Disselkoen, Watt, Parno, Patrignani, Vassena, Stefan. "MSWasm: Soundly Enforcing Memory-Safe Execution of Unsafe Code." POPL 2023 , PACMPL Vol. 7, Article 15 (not OOPSLA 2023; the prompt is in error). Earlier position paper: Disselkoen et al., "Progressive Memory Safety for WebAssembly," 2019. Follow-up: Iris-MSWasm , OOPSLA 2024 — Legoupil, Watt, Patrignani, Stefan, et al. — a fully mechanised foundation in Iris. https://dl.acm.org/doi/10.1145/3689722 ....

JavaScriptCore — Riptide

§1 Provenance Riptide. Filip Pizlo and the JavaScriptCore team at Apple. Introduced in WebKit r209827, blog post Jan 30 2017: https://webkit.org/blog/7122/introducing-riptide-webkits-retreating-wavefront-concurrent-garbage-collector/ . Companion blog from 2022: "Understanding Garbage Collection in JavaScriptCore From Scratch," https://webkit.org/blog/12967/understanding-gc-in-jsc-from-scratch/ . Related deep dive: "Concurrent JavaScript: It can work!" https://webkit.org/blog/7846/concurrent-javascript-it-can-work/ . Source: Source/JavaScriptCore/heap/ in https://github.com/WebKit/WebKit . §2 Mechanism Riptide is a concurrent, parallel, non-compacting, generational mark-sweep collector for JS objects in JSC. Key pieces: Marking concurrently...

Lobster — Compile-Time Reference Counting

§1 Provenance Lobster language. Wouter van Oortmerssen (the same author as Amiga-E, CryEngine's FlatBuffers, and several earlier ownership-RC experiments). Talk: "Compile-time reference counting & Lifetime analysis in Lobster," r/ProgrammingLanguages Meetup, Nov 22 2020, https://www.youtube.com/watch?v=WUkYIdv9B8c . Reference manual: https://aardappel.github.io/lobster/language_reference.html . Project site: https://strlen.com/lobster/ . Prior art the author cites: his own "ownership reference counting" (June 2004) and the academic Reference Escape Analysis paper (Park & Goldberg, SIGPLAN Notices 26-9, 1991, https://dl.acm.org/doi/10.1145/115866.115883)...

Industry, Policy, and Deployment Data

White House ONCD "Back to the Building Blocks" (February 2024)

§1 Provenance White House Office of the National Cyber Director. "Back to the Building Blocks: A Path Toward Secure and Measurable Software" , February 2024. 19 pages. https://bidenwhitehouse.archives.gov/wp-content/uploads/2024/02/Final-ONCD-Technical-Report.pdf Press release: https://bidenwhitehouse.archives.gov/oncd/briefing-room/2024/02/26/press-release-technical-report/ Anjana Rajan, Assistant National Cyber Director for Technology Security — primary spokesperson at release. Coverage: Tom's Hardware, "White House urges developers to avoid C and C++, use 'memory-safe' programming languages" . https://www.tomshardware.com/software/security-software/white-house-urges-developers-to-avoid-c-and-c-use-memory-safe-programming-languages The Record from Recorded Future News, "After...

Project Verona Regions

§1 Provenance Sponsor : Microsoft Research Cambridge, Microsoft Special Projects, Imperial College London. Core authors : Sylvan Clebsch (also Pony founder), Matthew J. Parkinson, Sophia Drossopoulou, Tobias Wrigstad, Juliana Franco. PM support from Mads Torgersen (C#). Project home : https://www.microsoft.com/en-us/research/project/project-verona/ . Publications : https://microsoft.github.io/verona/publications.html . Repo : https://github.com/microsoft/verona (MIT license). Key papers : Cheeseman, Parkinson, Clebsch, Kogias, Drossopoulou, Chisnall, Wrigstad, Liétar, "When Concurrency Matters: Behaviour-Oriented Concurrency", OOPSLA 2024. Arvidsson, Castegren,...

Google: Android Rust, Chrome Rust, V8 Sandbox

§1 Provenance Google Online Security Blog. "Rust in Android: move fast and fix things" (Nov 2025). https://security.googleblog.com/2025/11/rust-in-android-move-fast-fix-things.html Coverage: The Hacker News, "Rust Adoption Drives Android Memory Safety Bugs Below 20% for First Time" (Nov 2025). https://thehackernews.com/2025/11/rust-adoption-drives-android-memory.html 2024 baseline: The Hacker News, "Google's Shift to Rust Programming Cuts Android Memory Vulnerabilities by 68%" (Sep 2024). https://thehackernews.com/2024/09/googles-shift-to-rust-programming-cuts.html The Register, "Google's Rust belts bugs out of Android in Safe Coding push" (Sep 2024)....

Creusot

§1 Provenance Denis, Jourdan, Marché. "Creusot: A Foundry for the Deductive Verification of Rust Programs" , FM 2022. https://dl.acm.org/doi/10.1007/978-3-031-17244-1_6 ; preprint https://inria.hal.science/hal-03526634/document Project: https://creusot.rs ; repo https://github.com/creusot-rs/creusot ; user guide https://creusot-rs.github.io/creusot/guide/tutorial.html Underlying platform: Why3 / Coma (the new Creusot IR, replacing Why3's older WhyML emission path), targeting Z3, CVC5, Alt-Ergo 2.6.0 and others. Notable applications: CreuSAT (a verified SAT solver) and Sprout (a verified SMT solver), both Creusot case studies....

Linear Haskell

§1 Provenance Paper : Bernardy, Boespflug, Newton, Peyton Jones, Spiwack, "Linear Haskell: practical linearity in a higher-order polymorphic language", arXiv:1710.09756, POPL 2018. GHC documentation (user's guide): 9.0 intro: https://downloads.haskell.org/ghc/9.0.1/docs/html/users_guide/exts/linear_types.html 9.12 (Nov 2024): https://downloads.haskell.org/~ghc/9.12.0.20241128/docs/users_guide/exts/linear_types.html 9.15 dev (2026): https://ghc.gitlab.haskell.org/ghc/doc/users_guide/exts/linear_types.html Status in user guide every release : "currently considered experimental, with bugs, warts, and bad error messages expected". §2 Core type discipline Linearity is a property of the arrow , not the value...

MTE in a Managed Runtime

Why hardware tags don't save V8/ART/JSC, and what vm3's 12-bit generation already buys us. §1 Provenance Google V8 Team, "The V8 Sandbox." V8 blog, April 2024. https://v8.dev/blog/sandbox Groß (Project Zero), "V8 Sandbox proposal." Issue thread + 2021 design doc, ongoing. https://docs.google.com/document/d/1FM4fQmIhEqPG8uGp5o9A-mnPB5BOeScZYpkHjo0KKA8/edit Kim et al., "TIKTAG: Breaking ARM's Memory Tagging Extension with Speculative Execution." USENIX Security 2024. https://arxiv.org/abs/2406.08719 TIKTAG-v2 in V8 reproduction notes. https://www.emergentmind.com/open-problems/v8-constructible-tiktag-v1-gadget Android NDK Arm MTE guide (covers ART...

Rust Polonius (2026)

§1 Provenance Working group : Polonius WG, Rust compiler-team. Niko Matsakis (design), Jack Huey, Matthew Jasper, Amanda Stjerna (impl/PhD). Foundational papers : Matsakis et al., Non-Lexical Lifetimes RFC (RFC 2094, 2017), stabilised by default in Rust 1.63 (Aug 2022). Stjerna, Polonius Revisited (2023, Inside Rust blog). 2026 stabilisation goal : "Stabilize and model Polonius Alpha", https://rust-lang.github.io/rust-project-goals/2026/polonius.html WG page : https://rust-lang.github.io/compiler-team/working-groups/polonius/ Crate : https://github.com/rust-lang/polonius (Datafrog/Datalog reference impl, now superseded by in-tree...

MarkUs and quarantine-style UAF prevention

Defer reuse of freed memory until it's provably unreferenced. The most direct software analogue to vm3's "bump generation on slot reuse". §1 Provenance Ainsworth & Jones, "MarkUs: Drop-in use-after-free prevention for low-level languages." IEEE S&P 2020 . PDF: https://www.cl.cam.ac.uk/~tmj32/papers/docs/ainsworth20-sp.pdf MarkUs prototype code. https://github.com/SamAinsworth/MarkUs-sp2020 Wickman et al., "Preventing Use-After-Free Attacks with Fast Forward Allocation (FFmalloc)." USENIX Security 2021 . https://huhong789.github.io/papers/wickman:ffmalloc.pdf HUSHVAC: "Efficient Use-After-Free Prevention with Opportunistic Page-Level Sweeping." NDSS 2024 ....

Ownership, Borrowing, Reference Modes

V8 Sandbox

§1 Provenance Designer: Samuel Groß (formerly Google Project Zero, now leads V8 Security at Google). Talk: "The V8 Heap Sandbox," OffensiveCon 2024 — https://saelo.github.io/presentations/offensivecon_24_the_v8_heap_sandbox.pdf . Workshop paper: Groß, "The V8 Sandbox," MoreVMs 2025 (Programming 2025). Official blog: https://v8.dev/blog/sandbox . README: https://chromium.googlesource.com/v8/v8.git/+/refs/heads/main/src/sandbox/README.md . Rollout: enabled by default Chrome 123 (April 2024) on Linux/Windows/macOS/ChromeOS/Android, 64-bit only. Inclusion in Chrome's Vulnerability Reward Program (VRP): announced 2025; sandbox no longer "experimental." §2 Mechanism The...

V8 — Orinoco + Oilpan

§1 Provenance Orinoco. V8's collector family — concurrent and parallel marking, parallel Scavenger young-gen. Blog posts: https://v8.dev/blog/orinoco-parallel-scavenger , https://v8.dev/blog/trash-talk , https://v8.dev/blog/concurrent-marking . Oilpan. Blink's traced C++ GC, originally in third_party/WebKit/Source/platform/heap/ , migrated to V8 as a library since V8 v9.4 (2021): https://v8.dev/blog/oilpan-library . Design doc: https://chromium.googlesource.com/chromium/src.git/+/65.0.3283.0/third_party/WebKit/Source/platform/heap/BlinkGCDesign.md . May 2026 status overview: Andy Wingo, "The last couple years in v8's garbage collector," https://wingolog.org/archives/2025/11/13/the-last-couple-years-in-v8s-garbage-collector/ . §2 Mechanism V8 manages two heaps that...

Arm PAC + BTI

Pointer Authentication Codes sign code/data pointers in the unused high bits; Branch Target Identification confines indirect jumps to legal landing pads. Both ship on every modern Arm. §1 Provenance Arm, "Providing Protection for Complex Software: Pointer Authentication, BTI, and MTE." Learn-the-Architecture PDF. https://developer.arm.com/-/media/Arm%20Developer%20Community/PDF/Learn%20the%20Architecture/Providing%20protection%20for%20complex%20software.pdf Arm Newsroom, "Better Security at the Flick of a Compiler Switch: PAC + BTI." https://newsroom.arm.com/blog/pac-bti Liljestrand et al., "PACStack: an Authenticated Call Stack." USENIX Security 2021. https://www.usenix.org/conference/usenixsecurity21/presentation/liljestrand...

Inko — Singly-Owned Values

§1 Provenance Author : Yorick Peterse. Project home : https://inko-lang.org/ . Repo: https://github.com/inko-lang/inko (MIT license). Memory management reference : https://docs.inko-lang.org/manual/latest/getting-started/memory-management/ . Versioned: https://docs.inko-lang.org/manual/v0.13.2/getting-started/memory-management/ . Comparison page : https://docs.inko-lang.org/manual/master/getting-started/compared/ . Funded by : NLnet, https://nlnet.nl/project/Inko/ . Release notes : 0.10.0 (2022) introduced the ownership model. 0.18.1 (2025) latest stable. https://inko-lang.org/news/inko-0-18-1-is-released/ . Theoretical foundation : cites Servetto et al., "Ownership You Can Count On: A Hybrid Approach to Safe Explicit Memory Management"....

Microsoft "70% of CVEs Are Memory Safety" Statistic

§1 Provenance Miller (MSRC). "Trends, challenges, and strategic shifts in the software vulnerability mitigation landscape" , BlueHat IL 2019. Primary source for the 70% number. MSRC blog: "A proactive approach to more secure code" (Jul 2019). https://www.microsoft.com/en-us/msrc/blog/2019/07/a-proactive-approach-to-more-secure-code MSRC blog: "We need a safer systems programming language" (Jul 2019). https://www.microsoft.com/en-us/msrc/blog/2019/07/we-need-a-safer-systems-programming-language CISA. "The Urgent Need for Memory Safety in Software Products" (Dec 2023). https://www.cisa.gov/news-events/news/urgent-need-memory-safety-software-products NSA/CISA Joint Cybersecurity Information Sheet (June 2025). U/OO/172709-25...

Roc — Perceus in production-ish

§1 Provenance Roc language. Designed by Richard Feldman et al., compiler in Rust, runtime in Zig. The reference-counting + reuse pass is a direct port of Perceus (Reinking, Xie, de Moura, Leijen, PLDI 2021). Alias analysis: Morphic , a Rust library developed at UC Berkeley (Sullivan et al.). The thesis "Reference Counting with Reuse in Roc" (Utrecht student thesis, https://studenttheses.uu.nl/bitstream/handle/20.500.12932/44634/Reference_Counting_with_Reuse_in_Roc.pdf ) documents Roc-specific tweaks. Repo: https://github.com/roc-lang/roc — latest tag in...

CakeML and the Verified-JIT Line

§1 Provenance Kumar, Myreen, Norrish, Owens. "CakeML: a verified implementation of ML" , POPL 2014. https://dl.acm.org/doi/10.1145/2535838.2535841 Tan, Myreen, Kumar, et al. "A New Verified Compiler Backend for CakeML" , ICFP 2016. https://dl.acm.org/doi/10.1145/2951913.2951924 CakeML home: https://cakeml.org/ Myreen, PLDI 2024 keynote, "Much Still to Do in Compiler Verification (A Perspective from the CakeML Project)" . https://pldi24.sigplan.org/details/pldi-2024-papers/100/ Brack: A Verified Compiler for Scheme via CakeML by Lasnier, Yallop, Myreen, CPP 2026. https://popl26.sigplan.org/details/CPP-2026-papers/15/ FM-JIT...

Mojo (2026)

§1 Provenance Vendor : Modular Inc. Lead: Chris Lattner. Reference docs : https://docs.modular.com/mojo/manual/values/ownership/ . Deep dive: https://www.modular.com/blog/deep-dive-into-ownership-in-mojo . Lifetimes / provenance proposal : https://github.com/modular/modular/discussions/338 . Wikipedia summary : https://en.wikipedia.org/wiki/Mojo_(programming_language) . Production-ready milestone : Q1 2026. Open source commitment : "fall 2026" for the compiler; the standard library has been open since 2024. 2024–2025 contributor : Evan Ovadia (Vale) worked at Modular Jul 2024 – Dec 2025 on linear types, associated...

Verus

§1 Provenance Lattuada, Hance, Cho, Brun, Subasinghe, Zhou, Howell, Parno, Hawblitzel. "Verus: Verifying Rust Programs using Linear Ghost Types" , OOPSLA 2023 (PACMPL 7). https://www.microsoft.com/en-us/research/publication/verus-verifying-rust-programs-using-linear-ghost-types/ Lattuada et al. "Verus: A Practical Foundation for Systems Verification" , SOSP 2024. https://dl.acm.org/doi/10.1145/3694715.3695952 ; PDF https://www.cs.utexas.edu/~hleblanc/pdfs/verus.pdf AutoVerus (Wang et al., OOPSLA October 2025), LLM-assisted proof generation. https://www.microsoft.com/en-us/research/publication/autoverus-automated-proof-generation-for-rust-code/ VeriStruct (Sun, Sun, Amrollahi, Zhang, Lahiri, Lu, Dill, Barrett, TACAS April 2026), AI-assisted verification of data-structure modules...