Non-Interference Preserving and Optimising Compilation with Hyperproperty Simulations
summary
Presents a formal framework that generalizes compiler simulation proofs to arbitrary k‑trace hyperproperties and claims preservation of indistinguishability-based security (two traces) and higher‑order leaks (up to four traces). Introduces hyperproperty simulations (case/indistinguishability simulations) and implements a leakage‑aware dead code elimination pass that preserves non‑interference even with secret branches by using local fallbacks. All proofs are mechanically checked in the Coq proof assistant; implemented and verified for a toy language and proven correct.
AI-written summary · about
chapters (11)
- 0:00Introduction
- 2:12Dead code elimination breaks non-interference
- 3:55Leakage transformers and constant time
- 5:19Research contributions
- 6:44Generalizing simulation proofs
- 10:00Case simulations with traces
- 13:08Simulations from simulations
- 15:36Secret branch indistinguishability
- 16:39Dead code elimination in practice
- 19:37Conclusion and future work
- 21:00Q&A
related talks
14mNon-interference Preserving Optimising Compilation
22mSNIP: Speculative Execution and Non-Interference Preservation for Compiler Transformations
25mComposing Secure Compilers
59mTowards static analyses and abstract domains for hyperproperties
20mLifting Compiler Security Properties to Stronger Attackers: the Speculation Cas...
25mExploits as Insecure Compilation
08mShort Talk: Generalising secure compilation criteria
14mCollapsing Towers for Side-Channel Security