Preface
Defining Secrecy and Secure Multi-Execution (Noninterference)
- Naive attempt at defining secrecy
- Noninterference for pure functions
- A too strong secrecy definition
- Noninterferent implies splittable
- Secure Multi-Execution (SME)
- Noninterference for state transformers
- SME for state transformers
- Noninterference for Imp programs without loops
- SME for Imp programs without loops
- Noninterference for Imp programs with loops
- SME for Imp programs with loops
- Termination-Sensitive Noninterference
Information-Flow Control Type Systems (StaticIFC)
Cryptographic Constant-Time and Speculative Constant-Time (SpecCT)
- Cryptographic constant-time
- Adding constant-time conditional and refactoring expressions
- Adding arrays
- Instrumenting semantics with observations
- Constant-time security definition
- Example CF secure program that is not CCT secure
- Type system for cryptographic constant-time programming
- Exercise: CCT Type-Checker
- Noninterference lemma
- Final theorem: cryptographic constant-time security
- Exercise: Adding division (non-constant-time operation)
- Speculative constant-time
- CCT programs can be insecure under speculative execution
- Speculative semantics
- Speculative constant-time security definition
- Selective SLH transformation
- Main proof idea: use compiler correctness wrt ideal semantics
- Ideal semantics definition
- Ideal semantics enforces speculative constant-time
- Correctness of sel_slh as a compiler from ideal to speculative semantics
- Speculative constant-time security for Selective SLH
- Monadic interpreter for speculative semantics (optional)