Step 5: Verifying Assignments to Checked Objects

As described in Section 2, complete mediation requires verification that a variable is not re-assigned between an authorization and a controlled operation. From the CQUAL perspective, the right hand side (RHS) of an assignment takes one of four forms:

1. An unchecked object.

2. A checked object.

3. A structure member (e.g. dentry->d_inode).

4. An explicit type cast (e.g. (struct inode*)0xc2000000). Since explicit casts in the Linux source obviously don't include our qualifiers, CQUAL treats them as unqualified.

CQUAL correctly handles the first two cases, as the objects are qualified. If the left hand side (LHS) of the assignment is checked then CQUAL will raise a type violation for the first case and allow the second case.

In the third case, however, the structure member has no type qualifiers to cause type violations. With no other information, CQUAL will therefore infer that the RHS has the same qualified type as the LHS, and report no errors. As an example of how this can produce false-negatives, consider the code fragment below.

void func_a(struct inode * $checked
inode);

void func_b(struct inode * $checked
inode)
{
...
inode = dentry->d_inode;
...
func_a(inode);
}

The variable inode in func_b has already passed security check since it has a checked qualifier. However, it is assigned a value dentry->d_inode, before being passed to func_a which expects a checked inode. Clearly we would like CQUAL to raise a type violation, since dentry->d_inode is not an authorized variable. However, according to CQUAL inference rule, CQUAL will infer that dentry->inode is checked and allow the function call.

The solution is to treat dentry->d_inode as an unauthorized local variable by typecasting it to unchecked. At present we have not implemented the interim solution and so this source of false-negatives remains in our results.

The fourth case fails to report type violations for the same reason. Explicit casts in the Linux kernel do not include our type qualifiers, therefore, CQUAL infers their type. To address this problem, we wrote a PERL script that scans the source for explicit casts, and inserts the unchecked qualifier. Any assignment of such an expression to a checked variable or parameter will result in a type violation.