Top of Form
The Open Source Quality (OSQ) Project
UC Berkeley Faculty Investigators:
Alex Aiken ( ),
Tom Henzinger ( )
George Necula ( )
OSQ Project Homepage:
The OSQ project seeks to improve our ability to develop high quality software at reasonable cost. There are both experimental and theoretical facets of the project, and the project cuts across the three major disciplines for the analysis of software, namely, model checking, theorem proving, and program analysis. We have built four major software tools: CCured, CQual, BLAST, and CHIC, which are available on our web page, along with publications.
1. CCured (memory safety). CCured extends the C programming language with a classification of the pointer types according to how they can be used to violate memory safety. Furthermore, CCured provides an efficient inference mechanism to infer the optimal appropriate pointer kind for all pointers in a C program. The 'safe' pointers have the same properties as pointers in type-safe languages such as Java. CCured infers that about 80% of the pointers in a typical C program are 'safe'. Among the remaining pointers, the 'sequence' pointers have the added capability to participate in pointer arithmetic, which also means that they must be subject to bounds checking before use to ensure memory safety. Finally, C programs occasionally use type casts that make it impossible to predict statically the memory safety of the pointers involved. These pointers are of the 'dynamic' kind, and for them CCured inserts code that maintains and checks at run-time the type information.
Use of CCured has convinced us that most C programmers are quite conservative in their use of pointers, and that a relatively simple and predictable type inference system can recognize the safe use of pointers in large C programs reliably. We are able to enforce memory safety on C programs with an efficient analysis and pay only a 50% run-time overhead (on average), which is more than an order of magnitude better than commercial tools such as Purify. Using CCured we have also found memory safety bugs that cannot be caught with purely run-time-based tools such as Purify.
2. CQual (type qualifiers). CQual is a type-based analysis tool that provides a lightweight, practical mechanism for specifying and checking system-level properties of C programs. CQual extends the type system of C with extra user-defined type qualifiers. The programmer adds type qualifier annotations to their program in a few key places, and CQual performs qualifier inference to check whether the annotations are correct. The analysis results are presented with a user interface that lets the programmer browse the inferred qualifiers and their flow paths.
CQual has a number of features. First, types, and therefore type qualifiers, are a familiar way to add specifications to programs. Type qualifier inference frees the programmer from the burden of adding many annotations. Typically only a few key qualifier annotations need to be added to a program, and the rest can be automatically inferred. Second, type qualifier inference is efficient, even for whole-program analysis of large code bases. The technical idea behind CQual is constraint-based type inference. To analyze a program, CQual traverses the program's abstract syntax tree and generates a series of constraints that capture the relations between type qualifiers. A solution to the constraints gives a valid assignment of type qualifiers to the variables in the program. If the constraints have no solution, then there is a type qualifier inconsistency, indicating a potential bug. In a major experiment with CQual, we found numerous previously unknown locking errors in the Linux kernel's device drivers. Another application of CQual have found security vulnerabilities in format string usage (a common hacker attack).
3. BLAST (model checking) for C programs. BLAST’s goal is to check that software satisfies temporal safety properties, such as conformance to a specific locking discipline. BLAST uses counterexample-driven abstraction refinement to automatically construct an abstract model of a C program which is then model checked. The abstraction is constructed on-the-fly, and only to the required precision. BLAST shares with other model checkers that it is path-sensitive, meaning that it can deduce properties of individual program paths, exploiting knowledge of the logical consequences of the predicates (e.g., of conditional statements) along that path. The main novel feature of BLAST is that the construction of the abstraction and the model checking are intertwined, so that both processes perform no more work than necessary. In particular, by discovering and analyzing predicates lazily, BLAST only includes information needed to prove the goal, helping to avoid the potential for exponential blow-up inherent in path-sensitive analysis.
We have used BLAST to check numerous temporal properties of C programs, including proving the absence of null pointer dereferences, locking disciplines, and more complex properties such as that driver dispatch in Windows NT correctly handles both immediate and asynchronous devices. Lazy predicate abstraction makes a significant difference in overall performance, to the point that BLAST can be comfortably used for large program modules to check quite complex, and potentially expensive, properties. BLAST has fully automatically uncovered device driver bugs in tens of thousands of lines of C code.
4. CHIC (component interfaces). CHIC checks the compatibility between software component interfaces. We have developed 'interface automata', a formalism for specifying behavioral interfaces that may change over time. For example, the interface automaton of a file server may specify that the ‘read file’ method is available only if the ‘open file method’ has been called previously. In this way, an interface automaton provides a mechanism for specifying the assumptions that a software module makes about its environment. Two such interface automata -say, a server automaton and a client automaton- are compatible if they mutually obey each other’s environment assumptions. When two modules are checked for compatibility, this is usually done in a context in which there is yet an ‘outer environment’ that uses the composed modules. Hence compatibility checking is equivalent to deciding the outcome of a two-player game, where the outer environment tries to prevent the two interface automata from running into an error state. In other words, the compatibility check ensures that the two modules can be used together in some way.
CHIC automatically checks the compatibility between Java classes that have been manually annotated with interface automata specifying method availability constraints and call graph constraints. We have also used interface automata to uncover an incompatibility in TinyOS, an operating system for ad-hoc networks, and to verify the interfaces of hardware components such as the PCI bus.