This section describes code verification and label inference in more detail. It
demonstrates that basic block labels, labels on local variables,
and labels in declassify
expressions can be inferred efficiently and
automatically, making it much more convenient to write properly
annotated code. We present a small example of this process.
As described earlier, procedure verification is a twostep process that first determines basic block labels by propagating the labels of branchdetermining expressions, and then checking all the statements in the program in the context of their basic blocks. While the expressions that control branch decisions can be identified statically, their labels depend on the label of the basic block in which they occur. We seem to have a chickenandegg problem.
The difficulty can be resolved by creating a label constraint system and solving for all the inferred labels simultaneously. We start by inventing fresh labels L_{i} for each of the branch expressions in blocks B_{i}. These labels are propagated according to the rules for determining basic block labels, and fed into the statement verification stage. Verifying each statement requires checking of corresponding constraints involving labels. To verify code, we collect all the constraints that are demanded by the various statements, and solve them as a system. If the constraints are inconsistent and generate a contradiction, the program contains an information leak.
Solving the constraint system is tractable because the constraints all take a particularly simple form. Each constraint has either a label or a join of labels on both the left and righthand sides, e.g., L_{1} L_{2} L_{3} L_{4}. This equation is equivalent to the two equations L_{1} L_{3} L_{4} and L_{2} L_{3} L_{4}, and in general, we can convert the constraints to a canonical form in which there is only one label (variable or constant) on the lefthand side.
Explicitly declared labels (whether constants or firstclass labels) and implicit argument labels are treated as constants; basic block labels and undeclared labels on local variables are treated as variables. The goal of verification is to determine whether there are assignments to the local variable labels and basic block labels that satisfy all the constraints. This problem is similar in form to the problem of satisfying propositional Horn clauses; in fact, a lineartime algorithm for satisfying Horn clauses [DG84, RM96] can be adapted easily to this problem. If, on the other hand, we had permitted use of both the and operators in constructing label expressions, the label satisfaction problem would have become NPcomplete [RM96].
The algorithm works by keeping track of conservative upper bounds for each unknown label. Initially, all the upper bounds are set to . The algorithm then iteratively decreases the upper bounds, until either all equations are satisfied or a contradiction is observed. At each step, the algorithm picks an equation that is not satisfied when all variables are substituted by their upper bounds. If the unsatisfied equation has a constant label on its lefthand side, a contradiction has been detected. Otherwise, the upper bound estimate for the variable label on the lefthand side is adjusted to be the meet () of its current upper bound and the value of the righthand side. In evaluating the righthand side, all variables are replaced with their current upper bound estimates.
Like the algorithm for satisfying Horn clauses, this algorithm requires a number of iterations that is linear in the total size of the constraints; the total size of the constraints is at worst quadratic in the length of the code. Therefore, this inference algorithm seems very practical.
The labels found by this algorithm are the most
restrictive labels that satisfy the constraints. However, the actual
values that the inference algorithm finds are irrelevant, because they
are never converted to firstclass values of type label
. What is
important is that there is a satisfying assignment to all the labels,
proving that the code is safe.
check_password(db: array[pinfo{}], user: string, pwd: string) returns (ret: bool{user pwd db}) % Return whether "pwd" is the password of "user" i: int := 0 % match: bool := false % while i < db.length() do % L1 if db[i].names = user & % L1 db[i].passwords = pwd then % match := true % L1L2 end % i := i + 1 % L1 end % ret := false % if_acts_for(check_password, chkr) % ret := declassify(match) % end end check_password
Figure 8 shows the code for a more flexible
version of the check_password
procedure that was presented earlier.
This version of check_password
is usable by any client principal.
Because the arguments db
, user
, and pwd
have no declared labels,
their labels are implicit parameters to the routine.
Note that the local variables i
and result
do not explicitly declare
their labels. The resulting
procedure is as safe as the previous version of check_password
, and
easier to implement and use.
Let us now walk through the verification process for this code.
The first step in verification is to construct the basicblock diagram
and propagate fresh labels that represent branch expressions. The comments
in Figure 8 show the value of the
basic block labels for each basic block, in terms of the two branchexpression
labels
L_{1} and L_{2}
(for the if
and while
, respectively.)
Next, the code is analyzed to generate
the set of label constraints shown in Figure 9,
which include inequalities corresponding to
the statements in the program, plus some equalities that bind the basicblock
branchexpression labels to the labels for the corresponding expressions.
The equalities can be transformed into a pair of
constraints to preserve the canonical constraint form.
Note that the use of declassify
generates an additional
constraint, introducing a new variable L_{d} that represents the
label of the declassified result. This procedure provides a good example
of why it is important for declassification to be able to apply to just
one component of a join, as discussed in Section 3.4.
The fact that declassification works
at all in this procedure, let alone is possible to verify automatically,
is due to this property of the declassification rule.
i := 0
 i
 
match := false
 match
 
while
 i db
 =  L_{1} 
if

i
user
pwd
db
{chkr: chkr}
L_{1}
pwd
db
 =  L_{2} 
match := true
 L_{1} L_{2}  match
 
i := i + 1
 i L_{1}
 i
 
ret := false
 user pwd db
 
declassify
 match
 L_{d} {chkr: Ø}
 
ret := ...
 L_{d}  userpwddb

Applying the constraintsolving algorithm described above, a single backward pass through the canonical forms of these constraints yields labels that satisfy them, as shown in Figure 10.
i  =  user
pwd
db
{chkr: Ø}

L_{d}  =  user
pwd
db

Next: 7 Related Work Up: A Model for Decentralized Previous: 5 Application to a
Andrew C. Myers, Barbara Liskov