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 transformation may change the influence of the micro-architectural state on the execution (and hence the directives). 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 weakness 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 program. 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.

翻译：我们研究了在推测语义下保持编译器转换间非干扰性的问题。我们提出了一种证明方法，确保该性质在所有源程序上得到一致保持。该证明方法的基础是一种新型模拟关系，其通过建模攻击者对微架构状态控制的指令进行操作，并考虑编译器转换可能改变微架构状态对执行（及相应指令）的影响。利用该证明方法，我们证明了死代码消除的正确性。在尝试证明寄存器分配正确性时，我们发现了一个先前未知的缺陷，该缺陷会破坏非干扰性。我们已在主流编译器对libsodium密码库代码的处理中确认了该缺陷。为重新确保安全性，我们开发了一种在源程序与寄存器分配程序的乘积空间上操作的新型静态分析。基于该分析，我们提出对现有寄存器分配实现的自动化修复方案，并利用我们的证明方法验证了修复后寄存器分配的正确性。