SECOMP2CHERI: Securely Compiling Compartments from CompCert C to a Capability M...
summary
Extension of CompCert implements CompCert with compartments that enforces interfaces, disables cross-compartment inlining/tailcalls, and updates Coq correctness proofs; a RISC-V semantics adds a shadow stack to check cross-compartment calls and returns; security proof follows secure-compilation methodology but recomposition looks hard to scale. Work targets a CHERI capability backend using initialized and directed capabilities, privilege wrappers and integer pointers for intra-compartment data, aiming for machine-checked guarantees while preserving optimizations.
AI-written summary · about
chapters (9)
- 0:00Start
- 1:59A mitigation: compartmentalization
- 3:55Our goal: scaling up to C
- 5:00CompCert+Compartments
- 5:48Compartments and interfaces
- 8:58Compartments at the RISC-V level
- 12:39Correctness proof
- 18:48Conclusion
- 23:03Towards a security proof
related talks
15mMy Journey in Secure Compilation
24mSecure Calling Conventions for CHERI Capability Machines in Practice (Work in Pr...
16mMitigating Transient-Execution Attacks with CHERI Compartments
24mSecure Calling Conventions for CHERI Capability Machines in Practice (Work in P...
11mFast and fine-grained compartmentalisation in CHERI
12mLibrary-based Compartmentalisation on CHERI
26mEndangered by the Language But Saved by the Compiler: Robust Safety via Semantic(…)
19mCHERI C semantics