Security Reasoning via Substructural Dependency Tracking
summary
A new type system flips substructural resource reasoning from inputs to outputs and implements a suspended computation connective so effects are produced when thunks are forced. It models capabilities, quantity-sensitive leakage, and seccomp-like sandboxing via a mode lattice with affine, strict, and immobile resources, encodes examples as locks and diamond tokens and a high/drop protocol, and proves capability safety, quantity safety, and protocol safety by a single logical-relations soundness argument; artifacts and a decidability route via adjoint logic are available.
AI-written summary · about
chapters (19)
- 0:00Substructural dependency tracking intro
- 0:22Dependency tracking in security
- 1:23Substructural logic in Rust
- 3:06Input to output resource limits
- 4:51Password leakage tracking
- 6:15Authorization via resource diamonds
- 7:58Privilege drops with immobile resources
- 10:03Production resource safety
- 11:05Substructural modes and weakening
- 12:53Soundness theorem implications
- 13:37Capability safety via resources
- 14:18Quantity safety with affine locks
- 15:21Protocol safety and ordering
- 17:47Crypto semantics connection
- 18:29Unifying substructural tools
- 18:51Q&A: Non-termination & design
- 20:40Q&A: Adjoint logic & expressiveness
- 21:45Q&A: Mode lattice & modal types
- 22:05Closing remarks
related talks
32mSubstructural Information Flow via Polymorphism
19mMechanized Logical Relations for Termination-Insensitive Noninterference
17mProving capability safety in the presence of indirect sentries
22mGiving Semantics to Program-Counter Labels via Secure Effects
36mModularizing Reasoning about AI Capabilities via Abstract Dijkstra Monads
18mScalable Bug Detection for Internally Unsafe Libraries: A Logical Approach to Type(…)
36mObject Capabilities
15mStructural Information Flow: A Fresh Look at Types for Non-Interference