FlowCFL: Generalized Type-Based Reachability Analysis: Graph Reduction and Equivalence of CFL-Based
summary
A new dynamic semantics tracks chains between stack variables (flow from a parameter in one context to a return in another) and turns points-to reasoning into reachability between stack nodes; graph reduction via reference immutability builds G_RI by omitting inverse edges except for mutable receivers (no inverse edges for proven-immutable refs). Experiments on Java/Android tainting (including DroidInfer and a Zillow case) show 20–80% fewer variables flow to sinks versus the standard bi-directional graph G_BI, and the paper proves equivalence of CSFI-plus and FlowCFL.
AI-written summary · about
chapters (9)
- 0:00Intro
- 1:173 CFL-Reachability
- 3:12Type-Based Analysis
- 4:25Motivation
- 5:55Dynamic Semantics
- 8:22Graph Reduction
- 12:18Equivalence
- 13:03Zillow* App Example
- 14:05Related Work
related talks
15mStructural Information Flow: A Fresh Look at Types for Non-Interference
23mFlowCog: Context-aware Semantics Extraction and Analysis of Information Flow Leaks in Android Apps
26mType-directed Program Transformation for Constant-Time Enforcement
19mScalable Language Agnostic Taint Tracking using Explicit Data Dependencies
32mStatic Information Flow Control Made Simple
34mSymbolic Abstract Heaps for Polymorphic Information-flow Guard Inference
32mSubstructural Information Flow via Polymorphism
57mSequential Information Flow