Overview
The Saturn project is exploring techniques for highly scalable and precise
analysis of software, with applications to both bug-finding and verification.
Saturn is based on three main ideas:
-
Saturn is summary-based:
the analysis of a function f is a summary of f's behavior.
At call sites for f, only f's summary is used.
- Saturn is also constraint-based: analysis
is expressed as a system of constraints describing how the
state at one program point is related to the state at adjacent
program points. The primary
constraint language used in Saturn is boolean satisfiability, with each
bit accessed by a procedure or loop represented by a distinct boolean variable.
- Program analyses in Saturn are expressed in a logic programming
language with some extensions to support constraints and function summaries.
In combination, these ideas give Saturn the ability to succinctly express precise analyses while also providing the ability to scale to very large programs.
The use of constraints and logic programs allows succinct analyses, which are easier to understand and verify correct than analyses written at a lower level of abstraction.
Bit-level path-sensitive analysis gives precision, while analyzing a single function at a time and summarization give scalability.
As a result, we are able to routinely run whole-program Saturn analyses on the entire Linux kernel (with more than 6MLOC) and other large open source
projects. Collectively these analyses have found thousands of previously unknown bugs in such projects,
including projects that are already routinely checked by commercial bug-finding tools.
The current version of Saturn is a complete rewrite of the
original system, which was developed starting in early 2004. As a result, the locking and
memory leak bug-finding analyses, which were written in the old
version, are not currently supported in the new version. The new
version does provide a parallel implementation, allowing multiple
functions to be analyzed at the same time; we generally use clusters
of 25-80 processors, depending on program size and the computational
intensity of the analysis. All Saturn analyses are currently for C
programs, though the ideas could be applied to other languages.
Saturn is supported by NSF grants CCF-0430378 (which is partly funded by DARPA), CNS-050955, and SA4899-10808PG-1, and gifts or fellowships from IBM, Intel, and Microsoft.