Giving Semantics to Program-Counter Labels via Secure Effects
summary
Provides monadic semantics for program-counter labels by translating type-and-effect languages into pure ones using indexed monads and a more general productor relation, and proves a modular security result called non-interference half-off. Shows a single semantic framework handles state, exceptions and nontermination (recovering termination-sensitive noninterference), gives concrete typing rules and translations, and proves when the pc is (and is not) a lower bound on observable effects, with counterexamples and sufficient syntactic conditions.
AI-written summary · about
chapters (12)
- 0:00Intro
- 0:35Core Idea
- 2:43ProgramCounter Labels
- 6:36Type and Effect Systems
- 8:38Multiple Effects
- 9:21Exceptions in State
- 10:23Productors
- 11:03Semantic Framework
- 13:26Security Theorem
- 14:18Noninterference
- 17:19Other Effects
- 20:03Summary
related talks
25mExorcising Spectres with Secure Compilers
23mSecurity Reasoning via Substructural Dependency Tracking
20mLifting Compiler Security Properties to Stronger Attackers: the Speculation Cas...
08mShort Talk: Generalising secure compilation criteria
19mDo You Even Lift? Strengthening Compiler Security Guarantees Against Spectre Attacks
32mSubstructural Information Flow via Polymorphism
27mUniversally Composable Security for Program Partitioning
26mEndangered by the Language But Saved by the Compiler: Robust Safety via Semantic(…)