Information Flow Types, Runtime Monitors, and Gradual Typing
summary
Describes a concrete design that connects static information‑flow types and dynamic monitors: a two‑point lattice (L/H), typing rules that check explicit flows and join branch labels into a pc stack, and a runtime monitor that aborts on violations (NSU style) or refines imprecise labels expressed as interval labels (the unknown ? becomes a lattice interval). Claims: gradual typing lets the compiler statically reject provable leaks and the monitor enforce unresolved checks at runtime, preserving termination‑insensitive noninterference and the gradual guarantees.
AI-written summary · about
chapters (18)
- 0:00Intro
- 2:02Information flow security: an example
- 3:24Information flow security: goals/security properties
- 5:05Information flow security: security model
- 9:45Strava example
- 10:58Information flow in programs
- 13:23Enforcing information flow policies
- 14:30Information flow type systems
- 23:23Information flow runtime monitors
- 24:31Monitor assignment rules
- 26:54Monitor branching
- 31:10Security definition
- 32:18Noninterference
- 36:23Gradual information flow typing
- 37:08Gradual information flow types
- 42:36Gradual guarantees
- 43:39Summary
- 44:46References
related talks
15mStructural Information Flow: A Fresh Look at Types for Non-Interference
19mGradually Typed Languages Should Be Vigilant!
28mType-directed Program Transformation for Constant-Time Enforcement
32mSubstructural Information Flow via Polymorphism
26mType-directed Program Transformation for Constant-Time Enforcement
57mSequential Information Flow
15mLiquid Information Flow Control
22mReconciling Progress-Intensive Noninterference and Declassification