Structural Information Flow: A Fresh Look at Types for Non-Interference
summary
Type system separates data abstraction from information flow, turns single labels into dependency sets, and encodes quantifiers as existentials so module implementations can erase sensitive dependencies (example: password module sets its password dependency to empty) yielding principled declassification without unsafe casts. Core claim ties information flow to hybrid logic and proves non-interference with a logical-relations proof; a full paper, proofs, and artifacts available back the implementation and examples.
AI-written summary · about
chapters (9)
- 0:00Information flow types
- 1:03Dependency tracking from scratch
- 2:06Data abstraction vs flow properties
- 3:10Password checker and declassification
- 5:15Non-interference practically
- 6:18Existentials via Girard encoding
- 8:25Password checker implementation
- 10:09Dependency elision and list functions
- 11:37Q&A
related talks
32mSubstructural Information Flow via Polymorphism
32mStatic Information Flow Control Made Simple
47mInformation Flow Types, Runtime Monitors, and Gradual Typing
19mMechanized Logical Relations for Termination-Insensitive Noninterference
26mType-directed Program Transformation for Constant-Time Enforcement
57mSequential Information Flow
38mBuilding Secure Systems in Haskell
15mFlowCFL: Generalized Type-Based Reachability Analysis: Graph Reduction and Equivalence of CFL-Based