  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.
