Loopfrog

As a part of the "Detection of Security Flaws and Vulnerabilities by Guided Model Checking" project we implemented the tool called Loopfrog - an Abstract Interpretation based static analyzer for C programs.

Loops in programs are the Achilles' heel of static analysis. A sound analysis of all program paths through loops requires either an explicit unwinding or an over-approximation (of an invariant) of the loop. Unwinding is computationally too expensive for many real programs, and the computation of sufficiently strong invariants is an art.

The traditional approach to over-approximating program behavior is iterative application of an abstract transformer to every statement in the program. A set of abstract states, drawn from an abstract domain, is maintained for every program location, and the abstract transformer updates them until a fix-point is reached. For complex programs, this procedure may require many iterations until the fix-point is reached. Widening is a remedy for this problem, but it introduces further imprecision, yielding spurious errors. Model Checking, on the other hand, can perform a precise analysis, but comes at the cost of possibly enormous resource requirements. On the other hand, Model Checkers return diagnostic counterexamples, which are invaluable when it comes to understanding and fixing a bug.

We present Loopfrog, a static analyzer for ANSI-C programs. In contrast to traditional static analyzers, it does not calculate the abstract fix-point of a program by iterative application of an abstract transformer. Instead, it calculates symbolic abstract transformers for program fragments (loops in our case) using an algorithm presented in [1]. For an arbitrary program, Loopfrog computes abstract transformers starting from the inner-most loops, which results in linear (in the number of the looping constructs) run-time of the summarization procedure and which is often considerably smaller than the traditional saturation procedure of abstract interpetation.

After the summarization is completed, the summarized program is passed to a Model Checker, which enables us to return a counterexample in case the property fails (we call it leaping counterexample). The precision of the abstraction is controlled by a choice of an abstract domain, which is used in Loopfrog for the construction of the abstract transformers. The choice of domain can be localized with respect to a particular program loop.

Loopfrog was applied to various benchmarks ranging from specially created test cases to large-scale ANSI-C programs [2]. In our experiments we used a library of abstract domains, implemented as a part of Loopfrog. The benchmarks and experimental results can be found here.

Loop Summarization using Abstract Transformers talk was given at ATVA'08 conference.

[3]

References