SNIP: Speculative Execution and Non-Interference Preservation for Compiler Transformations

This 22-minute conference talk from POPL 2025 presents research on preserving non-interference across compiler transformations under speculative execution semantics. Learn about a novel proof method developed by Sören van der Wall and Roland Meyer from TU Braunschweig that ensures security preservation uniformly across source programs. The researchers introduce a new simulation relation that handles attacker-controlled micro-architectural states and accounts for how compiler transformations affect execution. Discover how they proved the correctness of dead code elimination while uncovering a previously unknown security weakness in register allocation that affects real-world cryptographic code in the libsodium library. The presentation also covers their innovative static analysis solution that operates on product programs and provides an automated fix for existing register allocation implementations, with formal proof of correctness for the fixed approach.