Скачать или смотреть [PriSC'25] SNIP: Speculative Execution and Non-Interference Preservation for Compiler(…)

SNIP: Speculative Execution and Non-Interference Preservation for Compiler Transformations (Video, PriSC 2025)
Sören van der Wall, and Roland Meyer
(TU Braunschweig; TU Braunschweig)

Abstract: We address the problem of preserving non-interference across compiler transformations under speculative semantics. We develop a proof method that ensures the preservation uniformly across all source programs. The basis of our proof method is a new form of simulation relation. It operates over directives that model the attacker's control over the micro-architectural state, and it accounts for the fact that the compiler transforma- tion may change the influence of the micro-architectural state on the execution (and hence the di- rectives). Using our proof method, we show the correctness of dead code elimination. When we tried to prove register allocation correct, we identified a previously unknown weak- ness that introduces violations to non-interference. We have confirmed the weakness for a mainstream compiler on code from the libsodium cryptographic library. To reclaim security once more, we develop a novel static analysis that operates on a product of source program and register-allocated pro- gram. Using the analysis, we present an automated fix to existing register allocation implementations. We prove the correctness of the fixed register allocations with our proof method.


Presentation at the PriSC 2025 workshop, January 19, 2025, https://popl25.sigplan.org/home/prisc...
Sponsored by ACM SIGPLAN