Check out the new USENIX Web site. next up previous
Next: Step 5: Verifying Assignments Up: Approach Previous: Step 3: Authorizations

Step 4: Verifying Controlled Operations Within Authorizing Functions

The analysis so far verifies mediation in the inter-procedural case, but, it does not verify intra-procedural mediation. Intra-procedural analysis is required to verify that controlled operations within an authorizing function occur after the authorization.

Our approach in step 3 makes this analysis simple. In step 3 we replaced all uses of the controlled object ($ co$) following the authorization with a new variable ($ co'$). An intra-procedural control-flow analysis verified the validity of this replacement. The intra-procedural analysis reduces to finding all controlled operations within the function that operate on local variables (parameters are handled by the inter-procedural analysis). If the local variable is an introduced variable ($ co'$) then it is mediated, otherwise a warning is generated.

Catherine Zhang 2002-05-13