2.2 Type Qualifiers and Subtyping

To find format string bugs, we use a type qualifier system with two qualifiers, tainted and untainted. We mark the types of values that can be controlled by an untrusted adversary with tainted. All other values are given types marked untainted. This is similar to the concept of tainting in Perl [32,42].

Intuitively, cqual extends the type system of C to work over qualified types, which are the combination of some number of type qualifiers with a standard C type. We allow type qualifiers to appear on every level of a type. Examples of qualified types are $\texttt{int}{}$, $\texttt{tainted}\;\texttt{int}{}$, $\texttt{untainted}\;\texttt{char}\;*$ (a pointer to an untainted character), and $\texttt{char}\;*\;\texttt{untainted}$ (an untainted pointer to a character).

The key idea behind our framework is that type qualifiers naturally induce a subtyping relationship on qualified types. The notion of subtyping most commonly appears in object-oriented programming. In Java, for example, if B is a subclass of A (which we will write $B<A$), then an object of class B can be used wherever an object of class A is expected.

Consider the following example program:

(1)	void f(tainted int); untainted int a; f(a);

In program (1), f, which expects tainted data, is passed untainted data. In our system, this program typechecks. Intuitively, if a function can accept tainted data (presumably by doing more checks on its input), then it can certainly accept untainted data.

Now consider another program:

(2)	void g(untainted int); tainted int b; g(b);

In this case, g is declared to take an untainted int as input. Then g is called with a tainted int as a parameter. Our system should complain about this program: tainted data is being passed to a function that expects untainted data.

Putting these two examples together, we have the following subtyping relation:

$$\texttt{untainted}{}\;\texttt{int}{} < \texttt{tainted}{}\;\texttt{int}{}$$

As in object-oriented programming, if $T_1 \leq T_2$ (read $T_1$ is a subtype of $T_2$), then $T_1$ can be used wherever $T_2$ is expected, but not vice-versa. We write $T_1 < T_2$ if $T_1 \leq T_2$ and $T_1 \neq T_2$.