Tags:memory safety, pointer analysis and static analysis
Abstract:
We address the problem of verifying the temporal safety of heap memory at each pointer dereference. Unlike separation-logic-based approaches, our whole-program analysis approach is undertaken from the perspective of pointer analysis, allowing us to leverage the advantages of and advances in pointer analysis to improve precision and scalability. A dereference ω, say, via pointer q is unsafe iff there exists a deallocation ψ, say, via pointer p such that on a control-flow path ρ, p aliases with q (with both pointing to an object o representing an allocation), denoted A^ψ_ω(ρ), and reaches ψ on ρ via control flow, denoted R^ψ_ω(ρ). Applying directly any existing pointer analysis, which is typically solved separately with an associated control-flow reachability analysis, will render such verification highly imprecise, since ∃ρ:A^ψ_ω(ρ) ∧ ∃ρ:R^ψ_ω(ρ) ⇏ ∃ρ:A^ψ_ω(ρ) ∧ R^ψ_ω(ρ) (i.e., ∃ does not distribute over ∧). For precision, we solve ∃ρ:A^ψ_ω(ρ) ∧ R^ψ_ω(ρ), with a control-flow path ρ containing an allocation o, a deallocation ψ and a dereference ω abstracted by a tuple of three contexts (c_o, c_ψ, c_ω). For scalability, a demand-driven full context-sensitive (modulo recursion) pointer analysis, which operates on pre-computed def-use chains with adaptive context sensitivity, is used to infer (c_o, c_ψ, c_ω), without losing soundness or precision. Our evaluation shows that our approach can successfully verify the safety of 81.3% (or 93,141/114,508) of all the dereferences in a set of 10 C programs totalling 1,166 KLOC.
Per-Dereference Verification of Temporal Heap Safety via Adaptive Context-Sensitive Analysis