Quest Complete: The Holy Grail of Gradual Security
summary
Claims a language 𝜆★IFC that satisfies both noninterference and the gradual guarantee by removing the unknown label ★ from runtime security labels, keeping type-guided classification and the standard no-sensitive-upgrade for mutable references. Presents a coercion-calculus semantics (coercions compressible for space efficiency), mechanizes the gradual guarantee and most of the noninterference proof in Agda mechanization, provides 𝜆★IFC with mutable refs, first-class functions and conditionals, and releases reusable artifacts. coercion calculi
AI-written summary · about
chapters (14)
- 0:00Gradual information flow control
- 1:04Dynamic vs static enforcement
- 5:19Gradual approach with unknown labels
- 6:49Gradual guarantee in security typing
- 8:14Counterexamples in prior IFC work
- 12:58Removing unknown labels for guarantees
- 13:41Calculus design for gradual IFC
- 15:49Proving non-interference and guarantee
- 16:30Conclusion and future directions
- 16:50Q&A: Leakage quantification
- 17:54Q&A: Algebraic data types
- 18:36Q&A: Side-channel prevention
- 19:40Q&A: Compiler vs runtime
- 20:24Q&A: Complex control flows
related talks
22mReconciling Progress-Intensive Noninterference and Declassification
23mGradual Verification for Smart Contracts
19mGradually Typed Languages Should Be Vigilant!
25mSecRef*: Securely Sharing Mutable References between Verified and Unverified Code in F*
21mSecurely Compiling F* Programs With IO and Then Linking Them Against Weakly-Typ...
21mSecuring Verified IO Programs Against Unverified Code in F*
32mStatic Information Flow Control Made Simple
19mMechanized Logical Relations for Termination-Insensitive Noninterference