A CHERI C Memory Model for Verified Temporal Safety

Watch this 27-minute conference talk from CPP 2025 exploring how CHERI architecture addresses temporal memory safety issues in C programming. Learn about a systematic examination of temporal memory safety within CHERI C, a dialect of the C programming language designed for CHERI architecture. The presentation covers five existing capability revocation mechanisms and their impact on CHERI C semantics, introduces a specialized object memory model, presents a new CHERI-specific pointer provenance tracking scheme, and formally defines security guarantees with Coq-proven correctness. Delivered by researchers from the Universities of Cambridge and Edinburgh, this talk addresses critical memory safety concerns that continue to be major sources of security vulnerabilities in modern systems, with particular focus on how CHERI's fine-grained memory access control through unforgeable hardware capabilities can be leveraged for improved security.