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 (
) following the
authorization with a new variable (
). 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 () then it is mediated, otherwise a warning
is generated.