Endangered by the Language But Saved by the Compiler: Robust Safety via Semantic(…)
summary
Shows a hardening compiler that makes a C‑like source (Rec) robustly safe only after compilation to a CHERI‑style capability machine (Cap); proves a separation logic, Reckon, that is unsound for raw Rec but sound for Rec→Cap compiled code; introduces semantic back‑translation via the DimSum multi‑language framework to relate arbitrary low‑level contexts to semantic source contexts; all proofs and artifacts are mechanized in Rocq and artifacts are available.
AI-written summary · about
chapters (12)
- 0:00Introduction
- 1:05Robust safety and undefined behavior
- 3:13Hardening compilers and security
- 4:15Capability machines and memory protection
- 6:04Formalizing compiler correctness
- 8:53Introducing Reckon program logic
- 12:04Verifying Reckon with compiler
- 14:10Back translation and semantic proofs
- 15:57Defining UNIF and SIM with Dim Sum
- 18:46Semantic back translation proof overview
- 20:33Summary and future directions
- 21:14Questions and answers session
related talks
25mA Semantic Approach to Robust Property Preservation
17mProving capability safety in the presence of indirect sentries
28mSECOMP2CHERI: Securely Compiling Compartments from CompCert C to a Capability M...
08mShort Talk: Generalising secure compilation criteria
15mMy Journey in Secure Compilation
23mMorello-Cerise: A Proof of Strong Encapsulation for the Arm Morello Capability Hardware(…)
24mSecure Calling Conventions for CHERI Capability Machines in Practice (Work in Pr...
16mCerisier: A Program Logic for Attestation in a Capability Machine