Symbolic Abstract Heaps for Polymorphic Information-flow Guard Inference
summary
Presents a symbolic store-less heap abstraction parameterized by relations (dumb, shallow, deep) and uses co-reachability on a deterministic symbolic finite-state system to automatically infer polymorphic information-flow guards. Implements the approach in Guardis (on Simaris), proves soundness, compares precision of the three heap domains on IFSpec, and scales to 60 ABM apps (≈22,000 methods) with only 146 analyses hitting a 5-minute/resource cutoff. Deep/field-aware relations yield noticeably tighter guards than the dumb baseline.
AI-written summary · about
chapters (15)
- 0:00Polymorphic info-flow guards
- 1:05Classical info-flow setting
- 3:15OOP low-level challenges
- 6:04Polymorphic guard inference
- 7:54Transition system generation
- 15:27Execution and violations
- 17:37Guards via weakest precondition
- 19:03Heap abstraction refinement
- 22:14Implicit flows and calls
- 23:24Tool implementation
- 24:50Scalability on Java benchmarks
- 26:15Conclusion and future work
- 27:43Q&A: loops and dependencies
- 29:15Q&A: control flow complexity
- 31:44Q&A: context sensitivity
related talks
32mSubstructural Information Flow via Polymorphism
17mProving capability safety in the presence of indirect sentries
21mHyper Separation Logic
26mType-directed Program Transformation for Constant-Time Enforcement
27mLightweight Shape Analysis based on Physical Types
22mHeapHopper: Bringing Bounded Model Checking to Heap Implementation Security
15mStructural Information Flow: A Fresh Look at Types for Non-Interference
22mQuest Complete: The Holy Grail of Gradual Security