Loop summarization

Based on our analysis of security-critical applications and experimentation with manually guided model checkers using loop invariants, we developed a new program abstraction technique. Our abstraction technique exploits the idea of loop summarization and guides program analysis towards security vulnerabilities.

Traditional abstract interpretation-based static analyzers iterate over the program, transforming sets of abstract variable values until a fix-point is reached. These computations often take numerous iterations to complete this task. E.g., on large benchmarks, a thousand iterations is commonly observed, even when using simplistic abstract domains. Thus, many tools implementing abstract interpretation apply widening in order to accelerate convergence. Widening, however, may yield imprecision, and thus, the abstract fixpoint may not be strong enough to prove the desired property.

We developed a novel technique to address this problem, which uses a symbolic abstract transformer. A symbolic abstract transformer is a relation over a pair of abstract states s, s' that holds if a given program statement transforms s into s'. The transformer can be applied to perform sound summarization, i.e., to replace parts of the program by a smaller representative. Our technique uses the transformer to summarize loops and (recursion-free) function calls.

Our new algorithm calculates the abstract fix-point over a loop in only one iteration, while at the same time performing precise computation. A loop-free abstraction of the input program is obtained by replacing all loops in the control flow graph of a program by their abstract fix-point. Checking reachability properties in the abstract program is much more efficient than in the concrete program. Since the abstract program may be verified using traditional, counterexample producing techniques like Bounded Model Checking, our technique can also generate diagnostic (leaping) counterexamples. This is a major advantage over any other tool based on abstract interpretation. For example this page shows a leaping counterexample from one of our experiments with the new technique. The example details a (previously known) buffer-overflow vulnerability in the Apache HTTP server. This diagnostic information is very helpful for understanding the nature of the problem, and is a major benefit for program analysis tools.

Due to over-approximation introduced by symbolic abstract transformers, our algorithm may report false positives - a disadvantage over model checkers that we seek to remedy in the future. However, since our algorithm of calculating the abstract fix-point is precise, the number of false positives is very low, when compared with other static analysis tools. We observed that it can be kept very small by guiding our technique using property- and program-specific abstract domains. Furthermore, our technique can use multiple abstract domains and thus localizes the computation with respect to a particular program structure. Also, it tailors a set of abstract domains to specific types of program properties, eventually guiding the verification tool to particular security vulnerabilities. We implemented the described algorithm in a tool named Loopfrog and successfully demonstrated that this approach scales to large-scale software and that it reports far fewer false positives than other static analysis tools, even when only a small number of abstract domains is employed. The loop summarization algorithm and its evaluation on the security benchmarks have been described in the paper [1]

References