Context-free language (CFL) reachability is a standard approach in static analyses, where the analysis question is phrased as a language reachability problem on a graph $G$ wrt a CFL L. While CFLs lack the expressiveness needed for high precision, common formalisms for context-sensitive languages are such that the corresponding reachability problem is 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 $d$ and a rank $r$. We show the utility of MCFL reachability by developing a family of MCFLs that approximate interleaved Dyck reachability, a common but undecidable static analysis problem. We show that MCFL reachability be computed in $O(n^{2d+1})$ time on a graph of $n$ nodes when $r=1$, and $O(n^{d(r+1)})$ time when $r>1$. Moreover, we show that when $r=1$, the membership problem has a lower bound of $n^{2d}$ based on the Strong Exponential Time Hypothesis, while reachability for $d=1$ has a lower bound of $n^{3}$ based on the combinatorial Boolean Matrix Multiplication Hypothesis. Thus, for $r=1$, our algorithm is optimal within a factor $n$ for all levels of the hierarchy based on $d$. We implement our MCFL reachability algorithm and evaluate it by underapproximating interleaved Dyck reachability for a standard taint analysis for Android. Used alongside existing overapproximate methods, MCFL reachability discovers all tainted information on 8 out of 11 benchmarks, and confirms $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.

翻译：上下文无关语言（CFL）可达性是静态分析中的标准方法，其中分析问题被表述为图$G$上关于CFL L的语言可达性问题。虽然CFL缺乏实现高精度所需的表达能力，但上下文相关语言的常见形式化方法使得相应的可达性问题不可判定。是否存在适用于静态分析的有用上下文相关语言可达性模型？本文提出多上下文无关语言（MCFL）可达性作为静态程序分析的一种表达力强且可处理的模型。MCFL构成由维度$d$和秩$r$参数化的轻度上下文相关语言的无限层次结构。我们通过构建近似交错迪克可达性（一种常见但不可判定的静态分析问题）的MCFL族来证明MCFL可达性的实用性。我们证明在$r=1$时，MCFL可达性可在$n$个节点的图上以$O(n^{2d+1})$时间计算，在$r>1$时以$O(n^{d(r+1)})$时间计算。此外，我们证明当$r=1$时，基于强指数时间假说，成员判定问题的下界为$n^{2d}$；而当$d=1$时，基于组合布尔矩阵乘法假说，可达性下界为$n^{3}$。因此对于$r=1$的情况，我们的算法在基于$d$的所有层次上均达到$n$倍内的最优性。我们实现了MCFL可达性算法，并通过在Android标准污点分析中下近似交错迪克可达性进行评估。与现有上近似方法结合使用时，MCFL可达性在11个基准测试中的8个上发现了所有污点信息，并在剩余3个测试中确认了上近似方法报告的94.3%可达对。据我们所知，这是首次针对该挑战性基准集实现高覆盖率且可证明覆盖范围的报告。