In theory, once an authorization is performed on a controlled
object, its qualified type is changed from unchecked to
checked. However, the current version of CQUAL we use is
flow-insensitive, i.e., the qualifier type of a variable remains the
same throughout its scope (e.g., the scope of a local variable is its
defining block, typically the function). To get around this
limitation, following an authorization, we declare a new,
checked qualified variable with the same base type as
the object authorized. All uses of the original controlled variable
following the authorization are replaced by the new variable. This
process is automated using a PERL script that replaces uses of the
original variable via simple pattern matching.
The simple approach of replacing all uses of the variable on
source lines following the authorization makes two assumptions
about the function's control-flow graph that must be verified.
Firstly, that there are no back-edges from below the authorization
to above it. This ensures that the authorization is not inside
a loop and that there are no goto statements below
the authorization that jump to above the authorization.
Secondly, that there is no control-flow path from above to below
the authorization that does not execute the authorization. This
ensures that the authorization is not inside a conditional
or switch statement.
These assumptions are verified by adding code to GCC to build the function's control-flow graph from its register transfer language (RTL) description. Once the graph is created, the two properties described above are verified. While the vast majority of authorizations possess these properties, exceptions do exist. Fortunately, the number of exceptions is small enough that they can be handled manually.