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)
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 pc secure program that is not constant-time secure
- Type system for cryptographic constant-time programming
- Final theorems: noninterference and constant-time security
- Speculative constant-time
- Speculative constant-time security definition
- Example CCT programs that are insecure under speculative execution
- Selective SLH transformation
- 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 sel_slh
- Monadic interpreter for speculative semantics (optional)