Mechanized Logical Relations for Termination-Insensitive Noninterference
summary
Paper proves that a rich information‑flow type system (recursive and existential types, System F impredicative polymorphism, label polymorphism, higher‑order state) implies termination‑insensitive noninterference for a call‑by‑value ML‑like language. The semantics is a binary logical relation built inside Modal Weakest Preconditions and implemented on top of Iris + Coq, including a confinement (unit) relation, mechanized proofs, and examples showing compositional linking of syntactically ill‑typed but semantically safe components.
AI-written summary · about
chapters (11)
- 0:00Intro
- 1:03The problem
- 1:57This work
- 4:38Language
- 6:44Typing judgment
- 7:17Type system
- 11:10Our approach cont'd cont'd
- 12:07Semantic model
- 14:09Semantic typing
- 17:08Value-dependent classification cont'd
- 17:58Conclusion
related talks
15mStructural Information Flow: A Fresh Look at Types for Non-Interference
23mSecurity Reasoning via Substructural Dependency Tracking
58mAutomating Relational Verification of Infinite-State Programs
57mSequential Information Flow
32mSubstructural Information Flow via Polymorphism
18mVMSL: A Separation Logic for Mechanised Robust Safety of Virtual Machines Communicating(…)
21mHyper Separation Logic
22mQuest Complete: The Holy Grail of Gradual Security