Scalable Program Analysis: Abstract Interpretation Techniques and Practical Applications

Abstract

Static program analysis aims to infer how a program behaves by reasoning about its source code under a formal semantics, without executing it. It is a core technique for software verification, compiler optimization, and security analysis; key applications include establishing memory safety guarantees, inferring numerical invariants, and detecting unsafe information flows. A central challenge is the precision--scalability trade-off: coarse abstractions scale but generate many false alarms, while highly precise methods often struggle on large codebases. This thesis develops sound and automated static analyses in the context of abstract interpretation, to achieve sufficient precision for formal verification while maintaining scalability on practical verification tasks.

The thesis presents three contributions. First, for memory safety verification, which requires inferring invariants to prove the validity of spatial memory accesses (i.e., that accessed buffer offsets remain within the bounds of their allocated buffer), we build a new abstract domain for reasoning about object invariants, where memory objects sharing common properties are abstracted relationally (i.e., summarized into a single abstract representation). However, such summarization causes precision loss when the properties of the summarized objects are temporarily violated during updates. To mitigate this, we introduce a new memory abstraction that separates recently manipulated objects from unchanged objects (i.e., summary objects). The new domain combines simpler subdomains for objects and scalars, so each part stays small and the whole analysis scales; the parts then exchange information through domain reduction to recover the precision that splitting them would otherwise lose. Second, for inferring numerical invariants, we propose a new numerical domain, Template Difference-Bounded Matrices (tDBM), to capture a useful subset of Two Variable Per Inequality (TVPI) constraints needed for bounds checking. By extending the matrix with additional dimensions via ghost variables that represent variables with scaled coefficients, tDBM provides a practical middle ground between lightweight weakly relational domains and expensive fully relational domains. Third, for information-flow security, we present a field-sensitive taint analysis that combines pointer analysis and data-flow analysis, and further integrates abstract-interpretation-based value reasoning to prune infeasible flows and reduce false positives. To improve precision in heap reasoning, we also introduce a refined variant of pointer analysis that better preserves field sensitivity while retaining scalability.

Overall, this thesis develops abstract domains tailored to the property being verified and kept lightweight without sacrificing the precision each task needs. Together, they prove memory safety and information-flow security while scaling to real-world programs.