Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

SNIP: Speculative Execution and Non-Interference Preservation for Compiler Transformations

Sören van der Wall, Roland Meyer

TL;DR

A proof method is developed that ensures the preservation uniformly across all source programs of non-interference across compiler transformations under speculative semantics and a novel static analysis is developed that operates on a product of source program and register-allocated program.

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 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.

SNIP: Speculative Execution and Non-Interference Preservation for Compiler Transformations

TL;DR

A proof method is developed that ensures the preservation uniformly across all source programs of non-interference across compiler transformations under speculative semantics and a novel static analysis is developed that operates on a product of source program and register-allocated program.

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 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.
Paper Structure (22 sections, 12 theorems, 24 equations, 3 figures, 2 tables)

This paper contains 22 sections, 12 theorems, 24 equations, 3 figures, 2 tables.

Table of Contents

  1. Introduction
  2. Background
  3. Contributions
  4. Language Model
  5. Non-intereference Properties
  6. Proving Speculative Non-Interference Preservation
  7. Simulation with Directive Transformation
  8. Snippy simulations
  9. Case Study: Dead Code Elimination
  10. Fixing Weaknesses in Register Allocation
  11. Register Allocation
  12. Register Allocation is not SNIP
  13. Poison-Tracking Product
  14. Static poison analysis of the product
  15. Fixing Register Allocation
  16. ...and 7 more sections

Key Result

Lemma 1

If two same-point states $\mathit{S}_1 \mathrel{define.samepoint} \mathit{S}_2$ execute with the same directives and leakages, $\mathit{S}_1 \mathrel{\mathrel{{\mathcolor{NavyBlue}{ \mathrel{{\raisebox{-1.6pt}{$\mathcolor{NavyBlue}{\xrightarrow{{d}\mkern1mu{:}\mkern1mu{l}}}$}}} }}}\mspace{-6mu}^{*}}

Figures (3)

  • Figure 1: Constant-time cubes. Left: leakage transforming; Right: directive transforming ($\mathrel{\triangleleft}$).
  • Figure 2: An execution of $P\,{::}\,[{P}]^{\mathsf{ra}}$ on \ref{['code:ra']}. Updated values are highlighted. Dead registers are gray.
  • Figure 3: The shape of $\Phi$-intervals. Teal and red paths form separate intervals.

Theorems & Definitions (20)

  • Lemma 1: Program-Counter-Leakage
  • Lemma 2: Directive-Determinism
  • Definition 1: $\mathsf{SNi}$
  • Definition 2
  • Definition 3: $\mathsf{SNiP}$
  • Theorem 1
  • Definition 4: $\mathsf{dt{-}sim}$
  • Definition 5
  • Lemma 3
  • Definition 6
  • ...and 10 more