一句话：提出基于新型模拟关系的证明方法，统一保证编译器变换在推测语义下保持非干扰，并修复寄存器分配引入的安全缺陷。
本文研究编译器变换在推测执行语义下保持非干扰（non-interference）的问题。作者提出一种新的模拟关系作为证明方法，它作用于刻画攻击者控制微体系结构状态的指令（directives），并处理变换可能改变微体系结构状态对执行影响的情况。用该方法证明了死代码消除的正确性；在尝试证明寄存器分配时发现一个此前未知的弱点会引入非干扰违规，并在主流编译器的 libsodium 代码上确认。为恢复安全性，作者提出一种在源程序与寄存器分配后程序乘积上运行的静态分析，给出对现有寄存器分配实现的自动修复，并证明修复后的寄存器分配正确。
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.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{abs-2407-15080,
title = {SNIP: Speculative Execution and Non-Interference Preservation for Compiler Transformations},
author = {Sören van der Wall and Roland Meyer},
journal = {Proceedings of the ACM on Programming Languages},
volume = {9},
number = {POPL},
year = {2025},
doi = {10.1145/3704887}
}