Controlled operations occur whenever a member of a controlled
type is read or written (all controlled data types are
structures). Controlled operations must only be performed on
checked
objects. With current version of CQUAL, we cannot specify
type requirements for variables at individual statement level,
instead, we specify type requirements on any function parameters that
are used in controlled operations within that function. This analysis
verifies complete mediation in the inter-procedural case (i.e., where
the controlling function is different from the authorizing function)
but, it cannot verify complete mediation for controlled operations
within an authorizing function. Our approach to intra-procedural
analysis is described in step 4 below.
To automate the annotation process, we again added code to GCC
to output the details of controlled operations, and then input
this information into a series of PERL scripts. These scripts
aggregate the controlled operations to the function parameters,
and add checked
qualifiers to those parameter
declarations. The type inference engine then propagates this
up the call graph, raising an error if an unchecked
local
variable is passed to a checked
parameter.
Figure 5 shows the subgraph structure that our
analysis searches for in the AST. Access to structure members
is represented in the AST by COMPONENT_REF
nodes. These
nodes have two children, the first is an expression which
specifies the variable being accessed, and the second is a
FIELD_DECL
node which specifies which field is being
accessed. The expression that specifies the variable being
accessed is a chain of INDIRECT_REF
and ADDR_EXPR
nodes corresponding to the C dereference (*) and address (&)
operators, respectively. At the end of this chain is either
a VAR_DECL
corresponding to a local variable, a
PARM_DECL
corresponding to a parameter, or a
COMPONENT_REF
if we are accessing a member of a
structure embedded in another structure.
Our analysis searches for COMPONENT_REF
nodes in the AST.
When one is found, it determines the type of the structure
being accessed (the left subgraph in Figure 5). If
this is a controlled type, then the expressions is accessing
a member of a controlled type, and the location information
(file, function, and line number) is reported. We also output
whether this operation is on a local variable (VAR_DECL
)
or a parameter (PARM_DECL
).
This information is then input to a series of PERL scripts. These
scripts scan the GCC output for controlled operations on
parameters (i.e., those that contain PARM_DECL
nodes). Using
the location information provided by GCC, they find the
function declaration, and annotate the parameter with the
checked
qualifier.