Check out the new USENIX Web site. next up previous
Next: Approach Up: Approach Previous: Approach

CQUAL Background

CQUAL is a type-based static analysis tool that assists programmers in searching for bugs in C programs. CQUAL supports user-defined type qualifiers which are used in the same way as the standard C type qualifiers such as const.

The following code segment shows an example of a user-defined type qualifier: unchecked. We use this qualifier to denote a controlled object that has not been authorized. This declaration states that the file object (filp) has not been checked.

struct file * $unchecked filp;

Typically, programmers specify a type qualifier lattice which defines the sub-type relationships between qualifiers and annotate the program with the appropriate type qualifiers. A lattice is a partially ordered set in which all nonempty finite subsets have a least upper bound and a greatest lower bound. For example, Figure 3 shows a lattice with two elements, checked and unchecked, and the subtype relation $ <$ as the partial order. Here it means checked is a subtype of unchecked.

Figure 3: A lattice of type qualifiers.
\begin{verbatim}partial order {
$checked < $unchecked

CQUAL has a few built-in inference rules that extend the subtype relation to qualified types. For example, one of the rules states that if Q1 < Q2 (meaning qualifier Q1 is a subtype of qualifier Q2) then type Q1 T is a subtype of Q2 T for any given type T. Replacing Q1 and Q2 with checked and unchecked respectively, we have that checked T is a subtype of unchecked T. From an object-oriented programming point of view, this means that a checked type can be used wherever an unchecked type is expected, but using an unchecked type where a checked type is expected results in a type violation. The following code segment shows a violation of the type hierarchy. Function func_a expects a checked file pointer as its parameter, but the parameter passed is of type unchecked file pointer.

void func_a(struct file * $checked filp);

void func_b( void )
  struct file * $unchecked filp;

Using the extended inference rules, CQUAL performs qualifier inference to detect violations against the type relations defined by the lattice. For a more detailed description of CQUAL, please refer to the original paper on CQUAL [9].

next up previous
Next: Approach Up: Approach Previous: Approach
Catherine Zhang 2002-05-13