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.