Verifying compilers.
On the other hand,
compilers and mitigation tools are better suited to verify or
enforce relative NI properties:
The compiler guarantees that its output program contains no
new leakages as compared to its input program.
This way, developers can reason about their
programs assuming a sequential model, and the compiler will mitigate any
speculative effects.
For instance, if a program \(p\)  is already sequentially constant-time \(\mathit {NI}({\llbracket \,\cdot \, \rrbracket ^{\text{seq}}_{\text{ct}}})\) ,
then a compiler that enforces
\(\mathit {NI}({\llbracket \,\cdot \, \rrbracket ^{\text{seq}}_{\text{ct}} \Rightarrow \llbracket \,\cdot \, \rrbracket ^{\text{pht}}_{\text{ct}}})\)  will compile \(p\)  to a program
that is speculatively constant-time \(\mathit {NI}({\llbracket \,\cdot \, \rrbracket ^{\text{pht}}_{\text{ct}}})\) .
Similarly, if a program is properly sandboxed under sequential execution \(\mathit {NI}({\llbracket \,\cdot \, \rrbracket ^{\text{seq}}_{\text{arch}}})\) , and is compiled
with a compiler that introduces no new \(\mathit {arch}\)  leakage, the resulting program will
remain sandboxed even speculatively.
Indeed, these
propositions are proven in [1]}.
