Non-Interference Preserving and Optimising Compilation with Hyperproperty Simulations

Watch this conference talk from PriSC 2025 where Julian Rosemann, Sebastian Hack, and Deepak Garg present their research on hyperproperty simulations, a novel framework for secure compilation that preserves security policies during the compilation process. Learn how this approach goes beyond classical compiler correctness by addressing indistinguishability-based properties like non-interference that are characterized by multiple traces rather than individual ones. Discover how the researchers overcome limitations of existing secure compilation approaches by modeling the preservation of arbitrary k-hyperproperties, allowing for more flexible compiler optimizations while maintaining security guarantees. The presentation demonstrates the framework's expressiveness through a leakage-based non-interference-preserving dead code elimination pass, verified in the Coq proof assistant. This 26-minute talk was presented at the PriSC 2025 workshop sponsored by ACM SIGPLAN.