Substructural Information Flow via Polymorphism
summary
Argues that information flow is expressible with parametric polymorphism replaces lattices, presents a prototype type system implemented in OKL/OCaml tooling (FlowCamel / okamel) that encodes dependencies as annotated types and statically simplifies lattice joins, and demonstrates it on a password/session-token auth example and a money-bag API that enforces a three-coin spend limit. Shows that dropping structural rules yields substructural interference gives capability safety and money-bag resource-limit example enforces resource counting; claims formal soundness and embeds into Granularism.
AI-written summary · about
chapters (9)
- 0:00Introduction
- 1:43Information flow basics
- 6:17Live demo
- 9:48Polymorphism foundation
- 15:28Substructural rules
- 17:36Practical applications
- 20:01Non-interference safety
- 22:51Comparison with type systems
- 27:13Q&A
related talks
15mStructural Information Flow: A Fresh Look at Types for Non-Interference
23mSecurity Reasoning via Substructural Dependency Tracking
34mSymbolic Abstract Heaps for Polymorphic Information-flow Guard Inference
47mInformation Flow Types, Runtime Monitors, and Gradual Typing
38mBuilding Secure Systems in Haskell
15mLiquid Information Flow Control
19mMechanized Logical Relations for Termination-Insensitive Noninterference
26mType-directed Program Transformation for Constant-Time Enforcement