Program Analysis via Multiple Context Free Language Reachability

Context-free language (CFL) reachability is a standard approach in static analyses, where the analysis question (e.g., is there a dataflow from 𝑥 to 𝑦?) is phrased as a language reachability problem on a graph 𝐺 wrt a CFL L. However, CFLs lack the expressiveness needed for high analysis precision. On the other hand, common formalisms for context-sensitive languages are too expressive, in the sense that the corresponding reachability problem becomes undecidable. Are there useful context-sensitive language-reachability models for static analysis?

In this paper, we introduce Multiple Context-Free Language (MCFL) reachability as an expressive yet tractable model for static program analysis. MCFLs form an infinite hierarchy of mildly context sensitive languages parameterized by a dimension 𝑑 and a rank 𝑟 . Larger 𝑑 and 𝑟 yield progressively more expressive MCFLs, offering tunable analysis precision. We showcase the utility of MCFL reachability by developing a family of MCFLs that approximate interleaved Dyck reachability, a common but undecidable static analysis problem.

Given the increased expressiveness of MCFLs, one natural question pertains to their algorithmic complexity, i.e., how fast can MCFL reachability be computed? We show that the problem takes 𝑂 (𝑛 2𝑑+1 ) time on a graph of 𝑛 nodes when 𝑟 = 1, and 𝑂 (𝑛 𝑑 (𝑟 +1) ) time when 𝑟 > 1. Moreover, we show that when 𝑟 = 1, even the simpler membership problem has a lower bound of 𝑛 2𝑑 based on the Strong Exponential Time Hypothesis, while reachability for 𝑑 = 1 has a lower bound of 𝑛 3 based on the combinatorial Boolean Matrix Multiplication Hypothesis. Thus, for 𝑟 = 1, our algorithm is optimal within a factor 𝑛 for all levels of the hierarchy based on the dimension 𝑑 (and fully optimal for 𝑑 = 1).

We implement our MCFL reachability algorithm and evaluate it by underapproximating interleaved Dyck reachability for a standard taint analysis for Android. When combined with existing overapproximate methods, MCFL reachability discovers all tainted information on 8 out of 11 benchmarks, while it has remarkable coverage (confirming 94.3% of the reachable pairs reported by the overapproximation) on the remaining 3. To our knowledge, this is the first report of high and provable coverage for this challenging benchmark set. CCS Concepts: • Software and its engineering → Software verification and validation; • Theory of computation → Theory and algorithms for application domains.