Composing Secure Compilers
summary
Formal results show that composing compilers preserves concrete classes of hyperproperties: sequential and upper composition guarantee that two compilers that are robust compilation preserves intersections yield a composed compiler that preserves the intersection of their preserved classes. Swapping robust optimization passes (common subexpression elimination, copy propagation) remains safe for properties. Introducing a source instrumentation that both preserves and enforces (example: SoftBound style checks plus fence to stop speculative leaks) defines a secure enforcement both preserves and enforces and composing a robust compiler with such an enforcement yields the intended union of guarantees (examples: uCaml lambda form → assembly, C/Fortran via GCC).
AI-written summary · about
chapters (7)
- 0:00Start
- 0:12Composing Secure Compilers
- 1:57Formal Preliminaries
- 3:39Attacker Model
- 15:09Secure Enforcements
- 19:39Takeaways
- 24:29Using the Same Trace Model at each Level
related talks
25mUniversal Composability is Secure Compilation
12mFully Abstract and Robust Compilation and How to Reconcile the Two, Abstractly
23mSecure Composition of SPECTRE Mitigations
15mMy Journey in Secure Compilation
14mNon-interference Preserving Optimising Compilation
22mComputational-Bounded Robust Compilation and Universally Composable Security
20mLifting Compiler Security Properties to Stronger Attackers: the Speculation Cas...
26mNon-Interference Preserving and Optimising Compilation with Hyperproperty Simulations