Compositional, Monotone, and Non-linear Program Analysis

Abstract

The presence of bugs in deployed software can lead to great economic and or human cost. One strategy for mitigating these losses is to prove the functional correctness of programs---or sometimes aspects of a program's functional correctness---during development. With an appropriate analysis technique, one can guarantee that deployed software will satisfy important properties for all possible inputs.

This dissertation presents several lines of research that advance the state-of-the-art in the topic area of automatically characterizing program behavior to prove functional correctness. More specifically, this dissertation focuses on building program-analysis techniques and tools that exhibit some combination of (1) producing non-linear invariants, (2) reasoning compositionally by building up more complex program summaries from simpler ones, and (3) being predictable by satisfying a monotonicity property.

The first line of research presented in this dissertation gives a program-analysis technique that is compositional and produces non-linear invariants. The key feature of the method is how it analyzes loops. To analyze loops, loop bodies are abstracted with the newly introduced wedge abstract domain. Furthermore, wedges admit a recurrence-extraction procedure that results in a set of c-finite recurrence relations that are implied by the original loop body. In this dissertation, we solve these c-finite recurrences using a technique based on operational calculus. In combination, these advancements yield a program-analysis tool that is able to produce program summaries that include equalities and inequalities between expressions that include polynomial, exponential, and logarithmic terms. Experimental results show that our method is able to generate precise non-linear summaries that are able to prove more programs correct in comparison to other state-of-the-art tools.

The second line of research presented in this dissertation focuses on automatically improving the precision of a base compositional analysis by modifying the way the base analysis summarizes loops. Specifically, this line of research presents a method that automatically rewrites a program-analysis problem to a semantically sound alternative problem, with the goal of achieving a more-precise analysis result. In pursuit of this goal, we introduce the notion of a pre-Kleene algebra (PKA) as model for reasoning about analysis precision. A key property of PKAs is that they have a monotonicity property. Our method then refines a program-analysis problem with respect to the laws of PKAs. Then, as long as the base analysis satisfies the axioms of PKAs, our method guarantees that the refined program-analysis problem will yield a result that is at least as good as (and often better than) the result obtained from the original analysis formulation. Although this result is technically a "no-degradation" result, an experimental evaluation showed that our method allows for an analysis to prove roughly 25% more programs correct at the expense of an approximately 50% increase in analysis time.

The third line of research presented in this dissertation introduces the optimal symbolic-bound synthesis (OSB) problem. In short, an instance of the OSB problem has as input a term t and a formula phi, and asks to find a symbolic term t* such that (i) phi implies that t* upper-bounds t, and (ii) t* exhibits some "term-desirability" properties. We present a heuristic method for finding a symbolic term t* when t and phi may contain non-linear terms. Our method works by extracting an implied cone of polynomials from phi and then reducing t by the cone of polynomials to obtain a sound upper bound t*. At a high level, our method makes use of Groebner-basis techniques for reducing with respect to equations, and a novel local-projection method for reducing with respect to inequalities. To show the utility of our method, we apply our techniques to the setting of bounding relevant terms, such as those representing the value of some financial asset, in Solidity smart contracts.

The fourth line of research presented in this dissertation gives another compositional program analysis that is able to produce non-linear invariants. The method follows a similar structure to the method from the first line of research; however, the subsequent method has the additional benefit of being monotone. We implemented our monotone technique in a tool named Abstractionator. Instead of wedges, Abstractionator uses solvable transition ideals as an intermediate abstraction of a loop. Abstractionator then uses a summarization technique inspired by prior complete methods based on solvable polynomial maps to summarize abstracted solvable transition ideals. Thus, by utilizing an abstraction procedure for solvable transition ideals, Abstractionator brings to bear prior complete polynomial-invariant-generation methods to the setting of programs with a more general syntactic structure. Experiments show that Abstractionator compares favorably with other program-analysis tools, especially in the case where non-linear invariants are required.