Modular Information Flow Through Ownership
summary
Repurposes Rust ownership and lifetimes to give a modular, static information flow analysis that requires no extra annotations, with a formal soundness proof via embedding a dependency calculus into Oxide and a noninterference theorem. Builds Flowistry and a VS Code slicer that analyzes arbitrary Rust functions in seconds and flags flows; evaluated on 400k LOC with a 94% match to whole‑program results, 1500 downloads and 1000 stars, and limits around unsafe/FFI and interior mutability.
AI-written summary · about
chapters (8)
- 0:00Start
- 1:34Defining information flow
- 2:25Implementing a practical information flow analysis for C++
- 4:37Memory unsafety arises from pointers and mutation
- 5:27Borrow checking protects memory safety
- 6:18Ownership types enable borrow checking
- 13:38Flowistry: a practical information flow
- 14:58Experiments showed the analysis is reasonably precise
related talks
32mStatic Information Flow Control Made Simple
18mCocoon: Static Information Flow Control in Rust
15mStructural Information Flow: A Fresh Look at Types for Non-Interference
32mSubstructural Information Flow via Polymorphism
38mBuilding Secure Systems in Haskell
17mFoundations for a Rust-Like Borrow Checker for C
35m"Memory Safety is Merely Table Stakes [...]"
45mBuilding Safe and Secure Systems in Rust