Approach

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).

Figure 4: Detecting Security Violations via Type Inferencing.

There are three requirements for this solution (equivalent to steps 1, 2, and 3, in the previous section):

1. All controlled objects must be initialized to unchecked.

2. All function parameters that are used in a controlled operation must be marked as checked.

3. Authorizations must upgrade the authorized object's qualified type to 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.