Better Not Together: Staged Solving for Context-Free Language Reachability
Context-free language reachability (CFL-reachability) is a fundamental formulation for program analysis with many applications. CFL-reachability analysis is computationally expensive, with a slightly subcubic time complexity concerning the number of nodes in the input graph.
This paper proposes staged solving: a new perspective on solving CFL-reachability. Our key observation is that the context-free grammar (CFG) of a CFL-based program analysis can be decomposed into (1) a smaller CFG, L, for matching parentheses, such as procedure calls/returns, field stores/loads, and (2) a regular grammar, R, capturing control/data flows. Instead of solving these two parts monolithically (as in standard algorithms), staged solving solves L-reachability and R-reachability in two distinct stages. In practice, L-reachability, though still context-free, involves only a small subset of edges, while R-reachability can be computed efficiently with close to quadratic complexity relative to the node size of the input graph. We implement our staged CFL-reachability solver, STG, and evaluate it using two clients: context-sensitive value-flow analysis and field-sensitive alias analysis. The empirical results demonstrate that STG achieves speedups of 861.59x and 4.1x for value-flow analysis and alias analysis on average, respectively, over the standard subcubic algorithm. Moreover, we also showcase that staged solving can help to significantly improve the performance of two state-of-the-art solvers, POCR and PEARL, by 74.82x (1.78x) and 37.66x (1.7x) for value-flow (alias) analysis, respectively.
Thu 19 SepDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
13:30 - 14:50 | Static analysisTechnical Papers at EI 9 Hlawka Chair(s): Dominik Helm University of Duisburg-Essen; TU Darmstadt; National Research Center for Applied Cybersecurity ATHENE | ||
13:30 20mTalk | Precise Compositional Buffer Overflow Detection via Heap DisjointnessACM SIGSOFT Distinguished Paper Award Technical Papers Yiyuan Guo Hong Kong University of Science and Technology, Peisen Yao Zhejiang University, Charles Zhang Hong Kong University of Science and Technology DOI Pre-print | ||
13:50 20mTalk | Finding Cuts in Static Analysis Graphs to Debloat Software Technical Papers Christoph Blumschein Hasso Plattner Institute; University of Potsdam, Fabio Niephaus Oracle Labs, Codrut Stancu Oracle Labs, Christian Wimmer Oracle Labs, Jens Lincke Hasso Plattner Institute; University of Potsdam, Robert Hirschfeld Hasso Plattner Institute; University of Potsdam DOI Pre-print | ||
14:10 20mTalk | Scalable, Sound, and Accurate Jump Table Analysis Technical Papers Huan Nguyen Stony Brook University, Soumyakant Priyadarshan Stony Brook University, R. Sekar Stony Brook University DOI | ||
14:30 20mTalk | Better Not Together: Staged Solving for Context-Free Language Reachability Technical Papers Chenghang Shi Institute of Computing Technology at Chinese Academy of Sciences; University of Chinese Academy of Sciences, Haofeng Li Institute of Computing Technology at Chinese Academy of Sciences, Jie Lu Institute of Computing Technology at Chinese Academy of Sciences, Lian Li Institute of Computing Technology at Chinese Academy of Sciences; University of Chinese Academy of Sciences DOI Pre-print |