Liquid Information Flow Control
summary
Claims a new DSL called Lifty domain-specific language that encodes information-flow policies as liquid refinements and enforces them with a TIO-style security monad, an SMT-backed type checker, and type-driven patch synthesis. The system statically verifies rich, data-dependent policies automatically, finds leaks quickly in real programs, and on three literature case studies synthesizes patches that repair all discovered leaks within reasonable time. The implementation and web demo are available.
AI-written summary · about
chapters (5)
related talks
38mBuilding Secure Systems in Haskell
32mSubstructural Information Flow via Polymorphism
32mStatic Information Flow Control Made Simple
15mStructural Information Flow: A Fresh Look at Types for Non-Interference
44mInfoflow LSM
47mInformation Flow Types, Runtime Monitors, and Gradual Typing
15mA Domain-Specific Language for Filtering in Application-Level Gateways
57mSequential Information Flow