Check out the new USENIX Web site. next up previous
Next: Step 4: Verifying Controlled Up: Approach Previous: Step 2: Annotating Checked

Step 3: Authorizations

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.


next up previous
Next: Step 4: Verifying Controlled Up: Approach Previous: Step 2: Annotating Checked
Catherine Zhang 2002-05-13