CQUAL is employed to perform the central task of statically
verifying that all inter-procedural paths from any initializing
function to any controlling function, contain an authorization of the
controlled object (steps 6 and 7 from Section 2). This
is achieved using the lattice configuration shown
in Figure 3. Figure 4 shows a graphical
depiction of our approach. All controlled objects are initialized with an
unchecked
qualifier. The parameters to controlling functions that
are used in controlled operations are specified as requiring
checked
qualified objects (as func_a
was above). Authorizations
change the qualified type of the object they authorize to checked
.
Using these qualifiers, CQUAL's type inference and analysis will report a
type violation if there is any path from an initializing function (where
the object is unchecked
) to a controlling function (where the object
must be checked
) that does not contain an authorization (a cast
from unchecked
to checked
).
There are three requirements for this solution (equivalent to steps 1, 2, and 3, in the previous section):
unchecked
.
checked
.
checked
.
If the number of controlled objects and controlling functions was small, we could manually annotate the source (as was done by Wagner et. al. to detect format string vulnerabilities using CQUAL [14]). Unfortunately, both are far too numerous for manual specification to be feasible. Therefore, we use a modified version of GCC and a set of PERL scripts to automate this process.
In the following subsections we detail our approach to each of the seven steps outlined in the previous section.