A CHERI C Memory Model for Verified Temporal Safety
summary
Defines a CHERI C object memory model that implements a new PNVI-CHERI provenance scheme, encodes five revocation strategies, and plugs into the Cerberus executable semantics with Docker images for testing. Formalizes temporal-safety invariants and supplies a Coq proof that the model preserves them through all operations, proving absence of use-after-reallocate and preventing use-after-free in the clean state. Implementation is ~3,400 LOC with ~9,500 LOC of proofs and is validated against the existing CHERI semantics test suite.
AI-written summary · about
chapters (11)
- 0:00CHERI C memory model intro
- 1:06CHERI and memory safety background
- 4:35Pointer provenance importance
- 7:06Temporal safety revocation
- 10:18CHERI C memory model contributions
- 11:44Memory model implementation details
- 15:17PNVI-CHERI provenance tracking
- 17:24Formalizing temporal safety
- 20:14Proving temporal safety
- 21:19Summary and resources
- 22:44Questions and answers
related talks
18mWhat’s next for memory safety?
16mCerisier: A Program Logic for Attestation in a Capability Machine
25mLightning Talk: Protecting Zephyr Against Memory Safety Vulnerabilities With the New CHERI Hardware Architecture
31mMemory Safety: The Pernicious Challenge- 25mLightning Talk: Protecting Zephyr Against Memory Safety Vulnerabilities With the New CHERI Hardware Architecture
24mSecure Calling Conventions for CHERI Capability Machines in Practice (Work in P...
10mCHERI in out-of-order microarchitectures
24mSecure Calling Conventions for CHERI Capability Machines in Practice (Work in Pr...