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
- Constant-time conditional
- Typing Constant-time Conditionals
- Now back to adding arrays
- 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 interpreter