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$ 参数化的轻度上下文相关语言的无限层次结构。我们通过构建逼近交错 Dyck 可达性（一种常见但不可判定的静态分析问题）的 MCFL 族来证明 MCFL 可达性的实用性。我们证明在 $n$ 个节点的图上，当 $r=1$ 时 MCFL 可达性可在 $O(n^{2d+1})$ 时间内计算，当 $r>1$ 时可在 $O(n^{d(r+1)})$ 时间内计算。此外，我们证明当 $r=1$ 时，基于强指数时间假说，成员判定问题具有 $n^{2d}$ 的下界；而当 $d=1$ 时，基于组合布尔矩阵乘法假说，可达性问题具有 $n^{3}$ 的下界。因此对于 $r=1$，我们的算法在 $n$ 倍因子内对于基于 $d$ 的所有层次都是最优的。我们实现了 MCFL 可达性算法，并通过在 Android 标准污点分析中下近似交错 Dyck 可达性进行评估。与现有的上近似方法结合使用时，MCFL 可达性在 11 个基准测试中的 8 个上发现了所有污点信息，并在其余 3 个基准测试中确认了上近似方法报告的 94.3% 可达对。据我们所知，这是首次针对这一具有挑战性的基准测试集获得高且可证明覆盖率的报告。