Blame-Preserving Secure Compilation
summary
Proposes a new secure-compilation criterion, Blame-Preserving Compilation, that refuses trivial proofs when the source language (e.g., C) cannot robustly satisfy a safety like temporal memory safety; it labels trace actions as context or component and requires violations to be attributable to the context (a blameful trace) before the compiler can be excused. Gives C→Rust and pointer-provenance examples, outlines formal two-criterion approach (property preservation plus operational correspondence) and connects to prior RSC/compartmentalization work.
AI-written summary · about
chapters (10)
- 0:00Introduction
- 1:26Whole-program compiler correctness
- 3:12Robust compilation framework limits
- 7:30Trivial premises in robust compilation
- 10:39Blame-preserving compilation
- 13:07Blameful property satisfaction
- 16:37Blame-preserving criteria
- 19:26Two secure compilation criteria
- 20:51Alternatives to blame-preservation
- 24:05Q&A
related talks
18mBlame-aware Recomposition for Formally Secure Low-level Compiler Backends
15mMy Journey in Secure Compilation
25mComposing Secure Compilers
18mWP-Preserving Compilation -- Preserving Weakest Preconditions For End-to-End Verification
26mSecurePtrs: Proving Secure Compilation with Data-Flow Back-Translation and Turn
20mLifting Compiler Security Properties to Stronger Attackers: the Speculation Cas...
20mFully Composable and Adequate Verified Compilation with Direct Refinements betwe...
37mMemory Safety Everywhere with Both Rust and Carbon