Non-interference Preserving Optimising Compilation
summary
Introduces hyperproperty simulations as a new secure-compilation framework that models preservation of arbitrary k‑hyperproperties and proves a generic non‑interference preserving code transformation that applies across different leakage models and standard optimisations. Claims this reduces per‑optimisation proof burden to a minimum, instantiates the transformation on multiple leakage models and optimisations, and formally verifies results in the Rocq theorem prover; artifacts are available and functionally evaluated (DOI: 10.1145/3763101).
AI-written summary · about
chapters (8)
- 0:00Non-interference compilation intro
- 1:05Dead code elimination security
- 3:12Trace indistinguishability goal
- 4:16Stuttering simulations in verification
- 6:44Generalizing simulations to traces
- 7:27Local leakage transformers
- 9:16Conclusion and future work
- 11:45Q&A
related talks
26mNon-Interference Preserving and Optimising Compilation with Hyperproperty Simulations
25mComposing Secure Compilers
22mSNIP: Speculative Execution and Non-Interference Preservation for Compiler Transformations
08mShort Talk: Generalising secure compilation criteria
22mComputational-Bounded Robust Compilation and Universally Composable Security
25mExploits as Insecure Compilation
16mReconciling Optimization With Secure Compilation
31mPyrosome: A Framework for Modular, Extensible, Equivalence-Preserving Compilati...