CHERI C semantics
summary
Project produces a mechanized CHERI C semantics implemented in Coq executable semantics and exposes a runnable model (Docker + Compiler Explorer). Memory model changes account for ~90–95% of edits and the group runs 90–94 tests across Clang/LLVM (moral and RISC‑V formats) and GCC at multiple optimization levels. Key design choices: address-only equality for ==, tag-clearing on bytewise pointer writes, and handling optimizer-driven differences (O2/O3) that change whether out‑of‑bounds writes fault; only minor compiler incompatibilities are found.
AI-written summary · about
chapters (12)
- 0:00CHERI C semantics intro
- 2:05Goals of formal semantics
- 4:56Pointer equality and integrity
- 6:23Out of bounds access
- 8:27Pointer modification and tags
- 9:55Capability derivation and arithmetic
- 11:20Executable CHERI semantics
- 12:45Testing semantics across compilers
- 13:28Comparison with C memory models
- 14:10Future work on formalization
- 14:53Publications and resources
- 15:58Q&A on pointers and atomics
related talks
28mSECOMP2CHERI: Securely Compiling Compartments from CompCert C to a Capability M...
16mCompositional Symbolic Execution for the Next 700 Memory Models
15mMy Journey in Secure Compilation
23mVellvm: Formalizing the Informal
01h 11mProgramming language memory models: Problems, solutions, and directions
22mReconciling High-level Optimizations and Low-level Code in LLVM
01h 06mVerifying a compiler through equational means- 01h 06mVerifying a compiler through equational means