Coursera Flash Sale
40% Off Coursera Plus for 3 Months!
Grab it
This conference talk explores the critical issue of preserving speculative constant-time security properties during program compilation. Learn how researchers Santiago Arranz Olmos, Gilles Barthe, Lionel Blatter, Benjamin Gregoire, and Vincent Laporte from Max Planck Institute, IMDEA Software Institute, and INRIA discovered that compilers often weaken or eliminate protections against side-channel attacks. Examine concrete examples where GCC and Jasmin compilers fail to maintain speculative constant-time properties, potentially introducing vulnerabilities to Spectre-v1 attacks. Discover the team's solution: a proof-of-concept compiler verified with Coq that preserves these crucial security properties. The presentation also covers practical applications, showing how cryptographic implementations in Jasmin can be fixed with minimal modifications to maintain protection against speculative execution attacks. This 18-minute talk was presented at the PriSC 2025 workshop sponsored by ACM SIGPLAN.
