HypreSpectre.Lang

• Language definitions: Syntax and Semantics
  • Basics
  • Syntax and Semantics of Expressions
  • Statements (Syntax)
  • Nonspeculative Semantics
  • Speculative Always-Mispredict Semantics

HypreSpectre.Leak

• Leakage models
  • Low Equivalence
  • Observations
  • Constant-Time Leakage Model
  • Loops + Memory Leakage Model
  • Memory-only Leakage Model

HypreSpectre.Mitigation

• Mitigations and Simulation Relations
  • Intel's Mitigation - Eager Insertion of Fences
  • Relaxed Insertion of Fences

HypreSpectre.Prefix_sens

• Prefix Relation for Termination-Sensitive Leakage Equivalence

HypreSpectre.Preserve_ct

• Intel's Mitigation preserves Constant-Time Leakage Equivalence
  • The Barrier Predicate
  • Simulation and Leakage
  • comp_fence Preserves Constant-Time Leakage Equivalence

HypreSpectre.Preserve_ct_relaxed

• Relaxed Insertion of Fences Preserves Constant-Time Leakage Equivalence
  • Barrier Predicate
  • Simulation and Leakage
  • Source Relation
  • comp_relaxed Preserves Constant-Time Leakage Equivalence

HypreSpectre.Preserve_lm

• Intel's Mitigation Preserves Loops+Memory Leakage Equivalence
  • Barrier Predicate
  • Simulation and Leakage
  • comp_fence Preserves Leakage Equivalence for Loops+Memory

HypreSpectre.Preserve_mem

• Intel's Mitigation Preserves Memory-Only Leakage Equivalence
  • Barrier Predicate
  • Simulation and Leakage
  • comp_fence Preserves Leakage Equivalence For Memory

HypreSpectre.SLH

• Counterexample for Speculative Load Hardening in Loops+Memory Model
  • Modeling Speculative Load Hardening
  • Sample Program
  • Input Heaps
  • Source Traces are Leakage Equivalent
  • Target Traces are not Leakage Equivalent