A possible extension to CQUAL would enable us to correctly verify mediation between the controlled operations and all security-sensitive operations. The CQUAL team has an interim solution and are looking into a general solution [8]. We describe the problem here.
Currently, structures in CQUAL are treated as a collection of fields,
so there is no relationship between a structure and its member fields.
For example, in the code below, var->bar would not have type
checked even though var does. Since structures are
used extensively in the kernel, we believe it would greatly enhance
the tool if CQUAL supports user-defined rules for inferring the types
of member fields from the types of structures.
struct foo {
int bar;
};
$checked struct foo *var;
For instance, for case 3 in Section 3.2.5, we would want the
inode that is extracted
from a checked dentry to be checked as well. In the
case that a dentry is unchecked, the inode of the dentry is implicitly
unchecked as well.
In addition, with current version of CQUAL, all instances of a
structure type share the same qualifer type. For
example, if bar is qualified as a
checked type, all instances of foo would have a
checked field for bar. What we want is to assign
qualifier types to members on a per-instance basis.
For verifying that the controlled operations mediate the
security-sensitive operations, we would also want any structure field
accessed through a checked type to be checked as well.
This would enable us to propagate authorizations through the structure
completely. Then, we could find any members of a security-sensitive
data type that is not accessed through a controlled data type.
Note that this approach is not always applicable depending on the semantics of the qualifications. This would not be appropriate for the type of qualifiers used by Wagner et. al. [14].