paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Restart and Refine: Scalable IFDS Taint Analysis across Memory Budgets

重启与精化:跨内存预算的可扩展 IFDS 污点分析
PLDI 10(PLDI)2026匹配度 3/10 · 该论文研究经典 IFDS 污点分析在内存受限下的可扩展性,属于传统静态程序分析,与用户核心关注的 LLM/Agent 与静态分析交叉、浮点程序分析或贝叶斯程序分析无直接关联。虽有形式化证明和工程评估,但研究目标不涉及 AI/LLM,因此匹配度较低。引用 0 inbox
Yujiang Gui, Yonggang Tao, Jingling Xue
crossref: 2026-09-10

AI 速览

一句话:提出 ReFine 迭代重启-精化框架,在内存受限下实现可扩展且可靠的 IFDS 污点分析。

污点分析常被建模为流敏感、上下文敏感的 IFDS 分析;为获得字段敏感,IFDS 将堆位置表示为 k 限访问路径,但面临三次时间与二次空间复杂度,在真实内存预算下易 OOM 或超时。现有改进多依赖充足内存,资源受限时仍脆弱。本文提出 ReFine 迭代重启-精化框架:内存耗尽时,复用已终止运行的部分结果作为可靠下近似来引导后续迭代;重启发生在部分分析点,利用污点传播在字段扩展下的单调性,将较长访问路径安全摘要为前缀。作者将其形式化为积半格上的不动点计算,并证明可靠性、正确性与终止性。在 31 个真实 Android 应用上对比先进 IFDS 污点分析,16 GB 下多分析 5.0 倍应用,800 GB 下多 2.4 倍,最高加速 52.5 倍。

问题
字段敏感的 IFDS 污点分析具有三次时间与二次空间复杂度,在现实内存预算下频繁发生内存溢出或超时。
方法
提出 ReFine 迭代重启-精化框架,复用部分分析结果作为可靠下近似,并利用字段扩展下污点传播的单调性对访问路径进行摘要与精化,形式化为积半格上的不动点计算并证明其可靠性、正确性与终止性。
评估
在 31 个真实 Android 应用上与先进 IFDS 污点分析对比,16 GB 内存下可多分析 5.0 倍应用,800 GB 下多 2.4 倍,最高加速 52.5 倍。
原文摘要(Abstract)

Taint analysis, widely used for bug and vulnerability detection, is typically formulated as a flow- and context-sensitive IFDS analysis. To achieve field sensitivity, IFDS models heap locations as k-limited access paths but suffers from cubic time and quadratic space complexity, leading to prohibitive costs under realistic memory budgets and frequent out-of-memory failures or timeouts. Existing improvements target scalability or precision under abundant memory but remain fragile under constrained resources. We present ReFine, an iterative restart-and-refinement framework that enables scalable IFDS taint analysis across diverse memory budgets. When memory is exhausted, ReFine reuses partial results from terminated runs as sound under-approximations to guide subsequent iterations. Each restart occurs at a partial-analysis point, where results are abstracted and refined by leveraging that taint propagation is monotonic under field extension—allowing longer access paths to be safely summarized by their prefixes. We formalize this process as a fixpoint computation over product semilattices and prove soundness, correctness, and termination. Evaluated on 31 real-world Android apps against a state-of-the-art IFDS taint analysis, ReFine wraps it in a restart-and-refinement framework, analyzing 5.0x more apps under 16 GB and 2.4x more under 800 GB, with up to 52.5x speedup. By turning partial analyses into progressive refinement, ReFine delivers sound, precise, and highly scalable IFDS taint analysis across diverse memory budgets.

链接与引用

DOI 原文 · PDF(开放获取) ·

BibTeX
@article{paperbot3772,
  title = {Restart and Refine: Scalable IFDS Taint Analysis across Memory Budgets},
  author = {Yujiang Gui and Yonggang Tao and Jingling Xue},
  journal = {Proceedings of the ACM on Programming Languages},
  volume = {10},
  number = {PLDI},
  year = {2026},
  doi = {10.1145/3808326}
}