Label checking

In addition to the standard type-checking performed by Java compilers, the Jif compiler performs label checking, ensuring that programs respect the security policies contained in the labels of information. The label checking rules are intended to enforce the following two properties.

  1. The apparent label of every expression is at least as restrictive as the actual label of every value it might produce.
  2. The actual label of a value is at least as restrictive as the label of any value that might affect it (modulo downgrading).
This section describes informally the label checking rules used in the Jif compiler.

Key concepts

Program counter labels

Every program point has a program counter label pc (introduced in Implicit flows and program-counter labels). For any given program point, pc is an upper bound on the information that may be deduced by knowing that program execution reaches the program point. Equivalently, pc can be regarded as an upper bound on the labels of all values that have affected the control flow of the program to reach the program point.

Normal and exceptional termination

The evaluation of an expression or statement may result in the throwing of an exception. As described in Runtime exceptions, exceptions are a covert information channel, and label checking must therefore carefully track the information encoded in the presence or absence of exceptions. For every expression and statement in a program, a label is associated with every subclass of Exception; this label is an upper bound on the information that may be deduced by observing that the expression or statement throws an object of that class. (Equivalently, the label is an upper bound on the labels of all values that may influence the throwing of the exception.) In addition, a label is associated with the normal termination of each expression and statement, that is an upper bound of the information that may be deduced by the termination of the expression or statement without an exception.

For example, consider the following (compound) statement.

if (i == 0) x = o.foo; else x = x/a;

The statement throws a NullPointerException only if the local variable i is zero and the local variable o is null. The statement throws an ArithmeticException only if the local variable i is non-zero and the integer variable a is zero. The statement will terminate normally if i and a are non-zero, or if i is non-zero and o is not null. Therefore, the label associated with normal termination is {i;a;o}pc, where {i;a;o} is the join of the labels of the local variables i, a, and o, and pc is the program counter label associated with the program point at the start of this statement. Similarly, the label associated with a NullPointerException being thrown is {i;o}pc, and the label associated with an ArithmeticException is {i;a}pc. The statement cannot throw any other exception. Note that the labels for normal termination and the exceptions do not mention the variable x, which appears in the statement, but does not affect whether an exception is thrown. In general, the label associated with normal termination is at least as restrictive as the label associated with each possible exception, as an expression or statement terminates normally only if it does not throw an exception.

Note that in Jif, unlike Java, all subtypes of Exception are checked. That is, subtypes of RuntimeExceptions must be either caught or declared to be thrown.

Normal value label

Label checking also determines for every expression an upper bound on the label of any value that the expression may evaluate to. This label is called the normal value label of the expression (or often, the label of the expression) and is in general at least as restrictive as the normal termination label of the expression, since the expression will only evaluate to a value it does not throw an exception.

Label environments

Each program point in a Jif program also has a label environment associated with it. A label environment records the relationships statically known to hold between labels, as well as the actsfor relationships statically known to hold between principals. Relationships between labels and between principals are known to hold statically through the use of label and actsfor method constraints, and through the use of runtime tests of label and principal relationships. All label checking constraints are checked using the label environment at the program point where the constraint arises. For example, in the following code, label checking requires that at the assignment, the label of y is no more restrictive than the label of x. Due to the actsfor relation contained in the label environment at that point, this constraint does indeed hold.

int{Alice→Bob} x;
int{Alice→Chuck} y;
if (Bob actsfor Chuck) {
    x = y; // OK, since {Alice→Chuck} ⊑ {Alice→Bob} is
           // deducible from the label environment at this point
}

Basics of label checking

Label checking closely follows the operational semantics of Java. As an example, consider label checking an integer division expression e1/e2, assuming that pc0 is the program counter label for this expression. This expression is evaluated by first evaluating e1, then evaluating e2, and then performing the division operation. Label checking this division expression requires first label checking e1, using pc0 as the program counter label. Since e2 will be evaluated only if e1 terminates normally, the program counter label for checking e2 is the normal termination label for e1, which is at least as restrictive as pc0. If the evaluation of e2 terminates normally, then the division operation occurs. Integer division will throw an ArithmeticException if e2 evaluates to 0. Thus, label checking associates the normal value label of e2 with the ArithmeticException that may be thrown by the division operation.

What exceptions can be thrown by the expression e1/e2, and what labels are associated with these exceptions? Clearly, e1/e2 may throw any exception thrown by e1, or e2, and the division operation itself may throw an ArithmeticException. Thus, the label associated with an ArithmeticException is the normal value label of e2, joined with the label associated with ArithmeticException by e1, joined with the label associated with ArithmeticException by e2. Similarly, for any other exception type T, the label associated with it is the label associated with T by e1, joined with the label associated with T by e2.

The normal termination label of e1/e2 is an upper bound on information that may be gained by knowing e1/e2 terminates normally, which happens if e2 terminates normally, and evaluates to a non-zero value. Thus, the normal termination label of e1/e2 is the normal termination label of e2 joined with the normal value label of e2.

The normal value label of e1/e2 is an upper bound on the information that may be gained by knowing what value the expression evaluates to. The value of e1/e2 depends on the values of e1 and e2, and thus the normal value label of e1/e2 is the normal value label of e1 joined with the normal value label of e2.

The example of label checking e1/e2 highlights two general principles used in Jif's label checking rules.

Jif's label checking rules preserve several invariants.

The label checking rules used in Jif are in large part explained by applying the general principles presented above to the operational semantics of Java, while ensuring that the invariants are preserved. In the presentation of the label checking rules in the remainder of the section, unless otherwise stated, these principles and invariants should be assumed to apply.

An additional label checking rule permits increased precision in checking expressions and statements. The single path rule states that if an expression or statement e can only terminate normally (that is, e cannot throw any exceptions, and does not contain any return statements), then the normal termination label of e is the program counter label of e. In the following example, even though an exception may be thrown depending on the value of i, the try-catch block can only terminate normally: no additional information is gained by knowing that execution of the try-catch block terminates successfully. Thus, by the single path rule, the normal termination label of the try-catch block is the same as the program counter label.

try {
    if (i < 0) 
        throw new Exception();
}
catch (Exception e) { }

Literals, binary and unary operators

The normal value label of a literal expression (including numeric literals such as 42, 0.5f, and 'r', and string literals such as "Hello world") is the pc label at the program point where the expression occurs. Since literal expressions cannot throw exceptions, the label of normal termination label of a literal expression is just the pc label.

A binary expression e1e2 is evaluated by first evaluating e1, then evaluating e2, and then performing the binary operation. For short-circuit evaluation operators && and ||, the evaluation of e2 depends on the value of e1, and so the pc label for e2 is the normal value label of e1; for all other binary operators the pc label for evaluating e2 is the normal termination label of e2.

Unless a simple dataflow analysis is able to prove that the value of e2 is non-zero, Jif conservatively assumes that any division or modulo operation may throw an ArithmeticException. Thus, the label of such an ArithmeticException is the normal value label of e2.

Pre- and post-increment and decrement operators are label checked as if they were assignments. For example e++ is label checked as if it were e+=1.

Label checking for other unary expressions, such as !e, ~e, and -e, is identical to label checking for the subexpression e.

Local variable declarations

Declarations of local variables may optionally contain a label annotation, called the declared label of the local variable. The label of the local variable is the join of the declared label with the program counter label for the declaration. If no declared label is supplied, then the local variable's label is inferred.

A local variable declaration may contain an initializing expression. Similar to assignments, the label-checking rules require that the normal value label of the initializing expression is no more restrictive than the label of the local variable. The label checking rules for array initializing expressions are described under Arrays.

If the local variable is declared final and is of type label, principal, or a subclass of jif.lang.Principal, and the initializing expression is a final access path, then the label environment is extended to record that the local variable is equivalent to the label or principal denoted by the initializing expression.

Variable access

A local variable access, such as the expression x, cannot throw an exception, and so the normal termination label of a local variable access is just the program counter label. The normal value label of a local variable access is the label of the local variable joined with the program counter label. Accesses to formal arguments are just a special case of local variable accesses, where the label of a formal argument is a polymorphic argument label.

A field access e.f may throw a NullPointerException if the target e is null. The Jif compiler uses a simple intra-procedural dataflow analysis to track whether local variables and final access path expressions are known to be non-null. If this dataflow analysis is unable to determine that the target e is definitely non-null, then the label associated with the NullPointerException is the normal value label of the target e. The normal termination label of a field access is thus the normal value label of the target e.

The normal value label of a field access e.f is the join of the normal value label of the target e with the label of the field f. Let L be the declared label of the field f; the label of the field f is obtained by substituting all occurrences of this appearing in the access paths of dynamic label or principals with e, as well as substituting actual label and principal parameters for formal label and principal parameters as appropriate. For example, consider the following declaration of the class C.

class C[principal P] {
    label{} lbl;
    int{P→Alice; *this.lbl} foo;
}

...

C[Bob] c = ...;
int x = c.foo;

When the field foo is accessed in the field access c.foo, the label of the field foo is {Bob→Alice; *c.lbl}. Thus, the normal value label of the field access is join of the normal value label of c and {Bob→Alice; *c.lbl}.

Variable assignment

Variable assignments include assignments to both local variables and to fields. Assignments to elements of arrays are described below.

For a local variable x, an assignment x=e is evaluated by first evaluating the expression e, and then performing the assignment. The label checking of x=e is straightforward: the expression e is label checked using the same program counter label as the assignment itself, and the normal value label of e is required to be no more restrictive than the label of x. See Local variable declarations for the definition of the label of a local variable. The assignment x=e throws only the exceptions thrown by e. The normal and exception termination labels are therefore the same as that for e. The normal value label of the assignment expression is also the same as that of e.

An assignment x op= e for local variable x (such as x*=4+y) is label checked as if it were the assignment x = x op e . In particular, if op is the division ('/') or modulo ('%') operator, then label checking conservatively assumes that an ArithmeticException may be thrown (unless a simple dataflow analysis can prove that e is non-zero), and the label associated with this exception is the normal value label of the expression e. The normal value label for the right hand side of the assignment is the label of x joined with the normal value label of e.

An assignment to a field, e1.f = e2, is evaluated by first evaluating e1, then evaluating e2. At this point, if e1 evaluated to null, then a NullPointerException is thrown. Otherwise, the assignment proceeds. Label checking a field assignment first label checks e1 using the same program counter label as the program counter label for the assignment itself. The normal termination label of e1 is then used as the program counter label to label check e2. If Jif's not-null dataflow analysis is unable to determine that the expression e1 is always non-null, then a NullPointerException may be thrown, and the label associated with it is the normal value label of e1 joined with the normal termination label of e2. The normal termination label of a field assignment (and also its normal value label) is thus the join of the normal value label of e1 and the normal termination label of e2.

We require that the information that may be revealed by the assignment occurring is allowed to flow into the field location. That is, the normal value labels of e1 and e2 must be no more restrictive than the label of the field e1.f, which is defined to be the declared label of f with appropriate substitutions applied. That is, any formal label parameter or principal parameter occurring in the declared label of f is substituted based on the type of the expression of the target e1, and any occurrence of this in the final access paths of dynamic labels or principals is replaced with e1. Since an assignment to a field may be observable in other scopes, the label of the field e1.f must be bounded below by the start-label of the current method, which is a lower bound on observable side-effects of the method.

The label checking of an assignment e1.f op= e2 is identical to the label checking of the assignment e1.f = e1.f op e2.

Assignments to fields that occur in a constructor prologue (that is, in a constructor body prior to the call to super(...)) are label checked slightly differently. Refer to Constructors for more details.

Arrays

Array types may be used in Jif programs, with some restrictions. Arrays must always have a labeled type as their base type. When declaring a local, field, or method argument with an array type, if no label is given for the base type, then the default label for the base type is the empty label {}.

Jif allows constant arrays: the contents of a constant array cannot be changed after initialization. Constant arrays have less restrictive label checking requirements. In particular, the base type of a non-constant array cannot contain the {this} label, or a covariant label parameter; this restriction does not apply to constant arrays.

Jif does not support instanceof and run-time casts to array types.

An array initialization expression new T[] {e1, ..., en} or {e1, ..., en} is evaluated by evaluating each array initialization expression e1 to en. Label checking proceeds similarly, label checking each expression in turn. In addition, Jif checks that each array element expression ei can be assigned into the array, that is, that the normal value label of ei is no more restrictive than the label of the array's base type.

Every array has a special length field. An expression e.length is evaluated like a normal field access, where the label of the pseudo-field length is {this}, and thus the normal value label of e.length is just the normal value label of e. A NullPointerException will be thrown if e evaluates to null, and the label associated with this exception is the normal value label of e.

An array access ea[ei] is evaluated by evaluating the array expression ea, and then evaluating the index expression ei. Then, if ea evaluated to null, a NullPointerException is thrown. If ea is not null, but ei is not a valid index into the array, an ArrayIndexOutOfBoundsException is thrown. Otherwise, the expression evaluates to the appropriate element of the array. Label checking of array access expressions associates the normal value label of ea with the NullPointerException, and the join of the normal value labels of ea and ei with the ArrayIndexOutOfBoundsException. The normal termination label of the array access expression is thus the join of the normal value labels of ea and ei. The normal value label of the array access expression is the join of the normal value labels of ea and ei and the label of the base type of the array.

An assignment to an array location ea[ei]=e is evaluated by first evaluating ea, then evaluating ei, and then e. At this point, if ea evaluated to null, a NullPointerException is thrown. If ea is not null, but ei is not a valid index into the array, an ArrayIndexOutOfBoundsException is thrown. If the base type of the array is a non-primitive type, and the type of the value that e evaluated to is not a subtype of the array's base type, an ArrayStoreException is thrown. Otherwise, the assignment then occurs. To label check an array assignment, the expressions ea, ei, and e are label checked in turn. The label associated with the NullPointerException is the normal termination label of e joined with the normal value label of ea. The label associated with the ArrayIndexOutOfBoundsException is the join of the normal termination label of e, the normal value labels of ea and ei. The label associated with the ArrayStoreException is the join of the normal termination label of e, and the normal value labels of ea, ei, and e. Let n be the normal termination label of the assignment, which is the join of the labels associated with each exception that can be thrown. We require that n is no more restrictive than the label of the array base type, and also (since the assignment is an observable side-effect), the label of the array base type must be bounded below by the current method's start-label, which is a lower bound on the method's side-effects.

An op= assignment to an array location, ea[ei] op= e, is similar to an array assignment, but different exceptions are thrown at different times. Evaluation proceeds by first evaluating ea, and then ei. At this point, the value in the location is read, which may result in a NullPointerException or ArrayIndexOutOfBoundsException being thrown. The right hand side e is then evaluated, after which the assignment occurs. Jif conservatively assumes that all /= and %= may throw an ArithmeticException when the assignment occurs, unless a simple dataflow analysis can prove that the operand is non-zero. The label associated with this exception is the normal value label of e joined with the label of termination reaching the assignment without throwing an exception. Note that no ArrayStoreException can be thrown, since the base type of the array must be a primitive type.

Subtyping

Many statements in Jif require checking a subtype relationship between two types. For example, the type of the right hand side of an assignment must be a subtype of the assigned location's type; the type of expression e in a statement return e; must be a subtype of the method's return type. Checking subtype relationships in Jif may require checking label relationships.

An array type T{L}[] is a subtype type of array type T'{L'}[] if and only if L and L' are equivalent (that is, LL' and L'L) and the types T and T' are equivalent (that is, T is a subtype of T' and vice versa).

Suppose C is a class with a label parameter Q occurring as the ith parameter. If Q is an invariant label parameter (the default), then C[..., L, ...] is a subtype of C[..., L', ...] if and only if L and L' are equivalent. On the other hand, if Q is a covariant label parameter, then C[..., L, ...] is a subtype of C[..., L', ...] if and only if LL'.

Consider the following example.

class C[covariant label L, label M] { } 
class D[covariant label L] extends C[L, {Alice→}] { }

If the class C has a principal parameter as the ith parameter, then C[..., p, ...] is a subtype of C[..., p', ...] if and only if p and p' are equivalent, that is, if and only if p can act for p', and vice versa.

Compound statements

A block {S1 ... Sn} is a sequence of zero or more statements. The first statement in the block is label checked using the same program counter label as the block itself, and the program counter label used to label check each subsequent statement is the normal termination label of the previous statement. A block may throw any exception that its statements may throw; the label associated with an exception thrown by a block is the join of the labels associated with that exception by each constituent statement.

A conditional statement if (e) St else Sf executes one of St and Sf dependent on expression e. The expression e is label checked using the same program counter label as for the conditional statement. The program counter label for label checking both St and Sf is the normal value label of e. The label environment for label checking St may be extended as a result of label tests and actsfor tests appearing in expression e. The normal termination label of the conditional statement is the join of the normal termination labels of St and Sf. The label for an exception is the join of the label of the exception for St with the label of the exception for Sf. Note that if neither St or Sf can throw an exception (or execute a return statement), then the single path rule applies, and so the normal termination label of the conditional statement would be the initial program counter label for the statement, since no information can be gained by observing that the conditional statement terminates normally.

To evaluate a loop while(e) S, the expression e is evaluated, and if it is true, then the statement S is evaluated; if S terminates normally, the evaluation of the loop repeats. To label check a while statement, we define a label pcloop, which is the program counter label immediately before the evaluation of the loop guard e. The loop guard e is label checked using pcloop as the program counter label. The loop body S is label checked using the normal value label of e as the program counter label. We require that pcloop is at least as restrictive as both the program counter label of the while statement, and normal termination label of the loop body S. The normal termination label a while statement is the normal termination label of the loop guard joined with the normal termination label of the loop body. Note that if neither the loop guard or the loop body can throw an exception, then the single path rule applies, and the normal termination label of the while statement is the same as the program counter label for the while statement (which may be less restrictive than pcloop). Thus, Jif's label checking is termination insensitive, since the normal termination label of the while statement may not be as restrictive as the normal value label of the loop guard.

A do S while(e); loop is very similar to a while loop. To label check a do-while loop, we define a label pcloop, which is the program counter label immediately before the evaluation of the loop body S. The loop body S is label checked using pcloop as the program counter label. The loop guard e is label checked using the normal termination label of S as the program counter label. We require that pcloop is at least as restrictive as both the program counter label of the do-while statement, and normal value label of the loop guard e. Like while loops, the normal termination label a do-while statement is the join of the normal termination labels of the loop guard and the loop body.

A loop for (Sinit; e; Sinc) S is label checked as if it were the code Sinit; while(e){S; Sinc;}.

A switch(e){S1 ... Sn} is executed by evaluating the expression e, then, considering each statement Si in turn, if the statement is case ei: and ei evaluates to the switch value, then the statements from the point onwards are executed. A default: statement may also be included in the switch body, which matches all possible switch values. Label checking of a switch statement first label checks the switch expression e; the program counter label used to label check e is as the same program counter label for the switch statement. Each statement in the switch body is then label checked, using the join of the normal value label of e and the normal termination label of the previous statement for the program counter label. This correctly tracks the information flow that may occur due to jumping to an appropriate case statement, or by "falling through" from a previous case. The normal termination label of a switch statement is the join of the normal termination label of the final statement in the switch body with the program counter labels of all the break statements that occur in the switch body. (This is just the standard label checking for branch statements, described below: the program counter label of the target of a break statement must be at least as restrictive as the program counter label of the break statement itself.)

Goto-like statements

Several Java statements transfer control non-locally. We discuss Exceptions in a separate section.

The statement return e; evaluates the expression e, and if the evaluation terminates normally, returns from the current method body. The program counter label for the label checking of expression e is the same as the program counter label for the return statement. The normal termination label of the expression e must be no more restrictive than the end-label of the current method. Similarly, the normal value label of e must be no more restrictive than the join of the current method's end-label and the current method's return value label. Since a return statement cannot terminate normally, it has no normal termination label.

A variant of the single path rule applies to statements which can only terminate by return statements. If the execution of a statement S can only terminate via return statements, then no additional information is gained by knowing that the statement exited by executing a return. Thus the requirement that the normal termination label of the expression e must be no more restrictive than the end-label of the current method can be weakened. For example, the following code is sound, and passes label checking, even though the program counter label for the return statements is more restrictive than the method's end-label.

int{secret} m{*<-*}(boolean secret):{*<-*} {
    // method body can only exit by return
    // statements, no exceptions possible
    if (secret) {
        // normal termination label of the return
        // expression is {secret}, which is more
        // restrictive than the end-label {*<-*}
        return 7;
    }
    else {
        return 42;
    }
}

The evaluation of the branch statement continue l; very simply jumps to the top of the loop labeled l. Similarly, the branch statement break l; jumps to the end of the loop labeled l. If no branch label l is specified, the innermost loop is used. (A break; statement's target may also be the end of a switch statement.) Label checking of branch statements is similarly straightforward: the program counter label of the branch statement must be no more restrictive than the program counter label at the program point where control will jump to. Jif's label checking uses the label environment track to the program counter labels for all possible continue and break targets. Since branch statements do not terminate normally, they have no normal termination label.

Exceptions

An exception may be explicitly thrown by a throw e; statement. A throw is evaluated by first evaluating the expression e. If e evaluated to null, a NullPointerException is thrown; otherwise the Throwable object that e evaluated to is thrown. Whichever exception is thrown, the label associated with it is the normal value label of e. Jif's not-null dataflow analysis can sometimes determine that the expression e cannot evaluate to null, in which case the NullPointerException cannot be thrown. Since a throw statement never terminates normally, it does not have a normal termination label or normal value label.

A try-catch-finally statement (which may contain zero or more catch blocks, and an optional finally block) is evaluated as follows. First, the try block is evaluated. If the try throws an exception, then each catch block is considered in turn, and if the class of the exception thrown is a subclass of the declared catch formal, then the catch block is evaluated. The finally block is then executed, regardless of the evaluation of the try or any catch blocks. The finally block may throw an exception. Otherwise, if the finally block terminated normally, the try-catch-finally terminates as did the catch block (if one was executed) or the try block.

The try block is label checked using the program counter label for the try-catch-finally block. Label checking of the try block will determine that it may throw various exceptions, and will associate a label with each such exception.

A catch (C{L} x) { ... } block contains a formal variable x, which may have a declared label L. If the formal has no declared label, then the label for the formal will be inferred, as with a local variable declaration. The label of the formal must be at least as restrictive as the label associated with any exception in the try block that may be caught by the catch block. That is, if the try block throws an exception of class C' with label L', and either C' is a subclass of C or C is a subclass of C', then the catch block may catch the exception, and so we must have L'L. The catch block is label checked using the label L of the formal as the initial program counter label. Note that the catch block's formal variable x will always be non-null in the body of the catch block.

The finally block, if present, is label checked using the same initial program counter label as the try block (since the finally block will always be evaluated, regardless of the behavior of the try or catch blocks).

A try-catch-finally statement will terminate normally if the finally block terminates normally, and either the try block terminated normally, or the try block threw an exception that was caught by a catch block that terminated normally. Thus, the normal termination label of a try-catch-finally is the join of the normal termination labels of each of the try block, catch blocks, and finally block. A try-catch-finally will terminate with an exception if the finally terminates exceptionally, if a catch block terminates exceptionally, or the try block throws an exception that is not caught by one of the catch blocks. The label associated with an exception for a try-catch-finally is thus the join of the labels associated with it in the catch blocks, finally block, and (if it is an exception that is not caught by any catch block) the try block.

Note that in Jif, unlike Java, all subtypes of Exception are checked. That is, subtypes of RuntimeExceptions must be either caught or declared to be thrown, and thus information obtained by observing RuntimeExceptions is tracked. See the section on Runtime exceptions for more information.

Dynamic type discrimination

Java has two language features that allow dynamic type discrimination: the instanceof operator, and checked run-time type casts.

Jif places some restrictions on the comparison type T that may occur in e instanceof T expressions , and casts (T)e. The comparison type T cannot be a labeled type, such as Foo{Alice→}, but may be a parameterized class, for example, Bar[Alice, this.lbl]. The type T cannot be an array type. (This is because Jif cannot represent at runtime the label of the array's base class, leading to potential unsoundness.)

The evaluation of both e instanceof T and (T)e is performed by first evaluating e, and then by "evaluating" the type T, which means evaluating any actual parameters to the class type. For example, this.foo instanceof Bar[pr, this.lbl] is evaluated by first evaluating this.foo, then pr and this.lbl, and finally evaluating the instanceof operator.

Both e instanceof T and (T)e may throw any exception that e throws, and any NullPointerException that the final access paths of the actual parameters of T may throw. In addition, a cast operator will throw a ClassCastException if e does not evaluate to an object of type T; the label associated with this exception is the normal value label of of e joined with the normal value label of T.

The normal termination label of e instanceof T is the normal termination label of e joined with the normal termination label of T. The normal termination label of (T)e is the join of the normal value label of e and the normal value label of T (due to the possibility of a ClassCastException).

The normal value label of e instanceof T and (T)e is the normal value label of e joined with the normal value label of T.

Dynamic label and actsfor tests

Jif provides mechanisms for run-time tests of labels and principals: the <= operator for labels, and the actsfor operator for principals. Label checking for expressions using these operators is exactly as for other binary expressions.

However, label and principal tests can in addition modify the label environment used for label checking. If an expression e1<=e2 appears as a conjunct of an if statement condition, and e1 and e2 are both either new label {...} expressions, or constants or final access paths of type label, then the label environment of the true branch of the if statement will contain the fact e1e2. Similarly, if an expression e1 actsfor e2 appears as a conjunct of an if statement condition, and e1 and e2 are both either constants or final access paths of type principal or a subtype of jif.lang.Principal, then the label environment of the true branch of the if statement will contain the fact e1e2.

Label expressions

Label expressions are explicit run-time representations of labels, such as new label {Alice→Bob; *←*}. In general, a label expression may contain any run-time representable label, such as a dynamic label, a label parameter, or an integrity or confidentiality policy consisting of runtime representable principals. Label checking of label expressions consists of label checking each label component in turn. Dynamic labels and principals are final access path expressions, and may thus throw NullPointerExceptions. Constant principals (such as Alice, ⊤ and ⊥) are label checked like literals. The normal value label of a label parameter or principal parameter is {this} joined with the program counter label, except when the parameter occurs in a static context, in which case the normal value label is a polymorphic argument label whose upper bound is the top label {⊤→⊤;⊥←⊥}.

Downgrading

As described in the section on Downgrading, Jif provides a mechanism to weaken the security policies enforced on information. Jif allows the declassification (downgrading of confidentiality) and endorsement (downgrading of integrity) of expressions and statements.

Both declassifications and endorsements are required to satisfy several constraints.

The actual label constraints to enforce these requirements are given below, during the presentation of declassification and endorsement.

Declassification

Declassification is the downgrading of confidentiality. Jif has two syntactic forms of declassification: a declassify expression, and a declassify statement. Declassification expressions are used to downgrade the confidentiality of an expression, whereas declassification statements downgrade the confidentiality of both the program counter label, and the side-effects of the statement.

Declassification expressions

The expression declassify(e,Lfrom to Lto) downgrades the confidentiality of expression e from the label Lfrom to the label Lto. A declassify expression is evaluated just by evaluating the subexpression e; that is, a declassification has no run-time effect and the labels Lfrom and Lto are not evaluated at run-time. Thus, a declassification expression may throw any exception that e may throw, and label checking for a declassification expression associates the same labels to exceptions that label checking e does. The normal termination label of a declassification expression is the same as the normal termination label of e.

The normal value label of a declassification expression is Lto, and the normal value label of the subexpression e must be bounded above by the label Lfrom. Thus, a declassification expression declassifies the normal value label of an expression.

Single dimension. A declassify expression may only downgrade the confidentiality of a label. Label checking enforces this by requiring that the following constraint is satisfied.

LfromLto ⊔ {⊤→⊤; ⊤←⊤}

The label {⊤→⊤; ⊤←⊤} contains the most restrictive confidentiality policy, and the least restrictive integrity policy, and so the constraint ensures that the integrity of Lfrom is no more restrictive that the integrity of Lto.

Selective downgrading. If a declassification weakens or removes a confidentiality policy owned by principal p, then the code that performs the declassification must have the authority of p (or a principal able to act for p). If the code has the authority of principals p1, ..., pn (as described in Authority and access control), then the Jif compiler requires that declassify expressions satisfy the following constraint.

LfromLto ⊔ {p1 ←⊤ ⊔ ... ⊔ pn←⊤ ; ⊥→⊥}

This constraint represents the authority of the code as the confidentiality policy p1 ←⊤ ⊔ ... ⊔ pn←⊤, and uses this policy to limit what policies may be weakened by the declassify expression. For example, suppose Lfrom is {Alice←Bob} and Lto is {Alice←Bob,Chuck}, and the code has the authority of Alice. This declassification should be allowed, and indeed, the constraint {Alice←Bob} ⊑ {Alice←Bob,Chuck} ⊔ {Alice ←⊤} is satisfied. By contrast, if the code had the authority of Bob, but not Alice (and assuming Bob cannot act for Alice), then the constraint {Alice←Bob} ⊑ {Alice←Bob,Chuck} ⊔ {Bob ←⊤} would not be satisfied: the code would have insufficient authority to perform the declassification.

Robustness. For declassify expressions, robustness requires that both the decision to declassify, and the information being declassified are high integrity. In particular, this requires the following two constraints to be satisfied, where pc is the program counter label for the declassify expression.

LfromLto ⊔ writersToReaders(pc)
LfromLto ⊔ writersToReaders(Lfrom)

In these constraints the operator writersToReaders(L) converts the writers of the label L into readers. In particular, for all principals p, we have the property that writers(p, L) ⊆ readers(writersToReaders(p, L)).

The writersToReaders(L) operator works by first finding an upper bound L' for L, such that L' consists only of reader and writer policies. Then, the writer policies of the upper bound L' are converted into reader policies, by reversing the direction of the arrow. The writersToReaders(L) operator is defined more formally below.

writersToReaders(L1L2) ≜ writersToReaders(L1) ⊓ writersToReaders(L2)
writersToReaders(L1L2) ≜ writersToReaders(L1) ⊔ writersToReaders(L2)
writersToReaders({c;d}) ≜ {wtr(d) ; ⊤←⊤}
writersToReaders(L) ≜ writersToReaders(L') where L' is an upper bound of L, and L is a dynamic label, label parameter, or polymorphic argument label. L' is found taking the meet of all upper bounds of L' that can be found by examining the facts in the label environment.

wtr(c1c2) ≜ wtr(c1) ⊓ wtr(c2)
wtr(c1c2) ≜ wtr(c1) ⊔ wtr(c2)
wtr(pq) ≜ pq

Declassification statements

The statement declassify(Lfrom to Lto) S downgrades the confidentiality of the program counter label from Lfrom to Lto for the label checking of the statement S. Label checking of declassification statements is done completely static, so the labels Lfrom and Lto are not evaluated at run-time.

The contained statement S is label checked with the program counter label set to Lto. In addition, label checking for S assumes that Lto is the lower bound for side-effects such as field update. (The lower bound for side-effects is normally equal to the start label of the current method.) The label environment for label checking S has two new facts added to it: {this}Lto and caller_pcLto. These facts state that both the label of the reference to the this object, and the program counter label at the call site of the current method, are no more restrictive than Lto. Normally, both of these labels are bounded above by the start label of the current method.

If S can complete normally, then the normal termination label of the declassify statement is the normal termination label of S joined with the program counter label for the declassify statement (that is, the program counter label just before it is declassified). Any exception that may be thrown by the statement S may also be thrown by the declassify statement, with the same label associated with it.

The restrictions on Lfrom and Lto that are applied to declassification expressions are also applied to declassification statements. In particular: (1) a declassify statement may only downgrade confidentiality; (2) a declassify statement must have sufficient authority to perform the declassification; and (3) the declassification must be robust. More details of these constraints are given above.

Endorsement

Endorsement is the downgrading of integrity. Like declassification, Jif supports different syntactic forms of endorsement: an endorse expression, an endorse statement, and also a checked endorse statement. Endorsement expressions are used to downgrade the integrity of expressions, whereas endorse statements downgrade the integrity of both the program counter label, and the side-effects of the statement.

Endorse expressions

The expression endorse(e,Lfrom to Lto) downgrades the integrity of expression e from the label Lfrom to the label Lto. Endorsements are checked statically, so a downgrading expression is evaluated just by evaluating the subexpression e; the labels Lfrom and Lto are not evaluated at run-time. Thus, an endorse expression may throw any exception that e may throw, and label checking for an endorsement expression associates the same labels to exceptions that label checking e does. The normal termination label of an endorse expression is the same as the normal termination label of e.

The normal value label of an endorse expression is Lto, and the normal value label of the subexpression e must be bounded above by the label Lfrom. Thus, an endorse expression endorses the normal value label of an expression.

Single dimension. An endorse expression may downgrade the integrity of a label. Label checking enforces this by requiring that the following constraint is satisfied.

{⊥→⊥; ⊥←⊥} ⊓ LfromLto

The label {⊥→⊥; ⊥←⊥} contains the most restrictive integrity policy, and the least restrictive confidentiality policy, and so this constraint ensures that the integrity of Lfrom is no more restrictive that the integrity of Lto.

Selective downgrading. If an endorsement weakens or removes an integrity policy owned by principal p, then the code that performs the endorsement must have the authority of p (or a principal able to act for p). If the code has the authority of principals p1, ..., pn (as described in Authority and access control), then the Jif compiler requires that endorse expressions satisfy the following constraint.

Lfrom ⊓ {⊥←⊥; p1 →⊤ ⊓ ... ⊓ pn→⊤} ⊑ Lto

Here, the authority of the code is represented by the integrity policy p1 →⊤ ⊓ ... ⊓ pn→⊤, which is used to limit which integrity policies may be weakened by an endorse expression.

Robustness. For endorse expressions, robustness requires that the decision to endorse is high integrity. Unlike declassification, the information being endorsed is (by definition) low integrity. In particular, the following constraint must be satisfied.

Lfrom ⊓ writersOnly(pc) ⊑ Lto

The writersOnly(L) operator removes the confidentiality policy of L, and is simply equivalent to L ⊔ {⊤→⊤;⊤←⊤}.

Endorse statements

The statement endorse(Lfrom to Lto) S downgrades the integrity of the program counter label from Lfrom to Lto for the label checking of the statement S. Label checking of endorse statements is done completely static, so the labels Lfrom and Lto are not evaluated at run-time.

The contained statement S is label checked with the program counter label set to Lto. In addition, label checking for S assumes that Lto is the lower bound for side-effects such as field update. (The lower bound for side-effects is normally equal to the start label of the current method.) The label environment for label checking S has two new facts added to it: {this}Lto and caller_pcLto. These facts state that both the label of the reference to the this object, and the program counter label at the call site of the current method, are no more restrictive than Lto. Normally, both of these labels are bounded above by the start label of the current method.

If S can complete normally, then the normal termination label of the endorse statement is the normal termination label of S joined with the program counter label for the endorse statement (that is, the program counter label just before it is endorsed). Any exception that may be thrown by the statement S may also be thrown by the endorse statement, with the same label associated with it.

The restrictions on Lfrom and Lto that are applied to endorsement expressions are also applied to endorsement statements. In particular: (1) an endorse statement may only downgrade integrity; (2) an endorse statement must have sufficient authority to perform the endorsement; and (3) the endorsement must be robust. More details of these constraints are given above.

Checked endorse. Many programs need to validate untrusted data and then treat it as trustworthy. This functionality is supported by the checked endorse statement. It takes the following form:

endorse (x, Lfrom to Lto) 
    if (e) S else S'

where x is a local variable, and Lfrom and Lto are labels.

Label checking of checked endorse statements proceeds as if the checked endorse statement were equivalent to the statement

x' = endorse (x, Lfrom to Lto);
if (e[x'/x]) S[x'/x] else S'

where x' is a fresh local variable of the appropriate type, and e[x'/x] and S[x'/x] denote e and S respectively, with all occurrences of x replaced with x'. Thus, the label checking for a checked endorse statement is more like the label checking for an endorse expression, than for a standard endorse statement.

Method declarations

Jif method declarations include a number of labels. These labels are described in Method declarations. All Jif methods have these labels; if they are not specified explicitly, then appropriate defaults are used. Every Jif method declaration has the following labels.

In addition, a method may have a number of where clauses, which may take any of the following forms.

The label environment used to check the method body has all of the label and actsfor clauses added to it. Any principal that appears in am authority(p) clause of a method must also appear in the class's authority(p) clause.

The program counter label used to label check the method body is set to a special polymorphic label caller_pc. The label caller_pc represents the program counter label at the call site of the method, that is, where the method is being called from. The caller_pc is thus known to be bounded above by the method's begin-label. In addition, for every auto-endorse clause endorse(Len), the label environment contains the constraint that caller_pcLen. The label environment also contains the fact that the receiver object {this} is bounded above by caller_pc, which must be true because the method is invoked only after evaluating the receiver of the method call, and the normal value label of the receiver call is the instantiation of the label {this} for the method call.

The normal termination label for the method body must be no more restrictive than the end-label of the method joined with the caller_pc label. (Joining the end-label with the caller_pc label is more permissive while remaining sound.) Similarly, the information that is gained by knowing the method terminates via a return statement must be no more restrictive than the end-label of the method joined with the caller_pc label.

In addition, the label associated with any exception thrown by the method body must be no more restrictive than the labels for the appropriate exceptions declared in the throws clause of the method, joined with the caller_pc label. More precisely, if label checking the method body determines that the method body may throw an exception of class C with label LC, and the method declaration says that the method may throw an exception of class D with label LD, where C is a subclass of D, then we must have LCLDcaller_pc.

Any value that is returned by method body must be no more restrictive than the return value label of the method, joined with the end-label of the method, joined with caller_pc. That is, if the statement return e; appears in the method body, and label checking determines that the normal value label of expression e is Le, then it must be the case that Le is less than the join of the return value label, the end-label, and caller_pc.

Neither the method begin-label nor any of the argument labels may contain a covariant label parameter. This is because the method begin-label and argument labels appear in contravariant positions, and allow covariant label parameters to appear would introduce unsoundness.

Auto-endorse clauses downgrade the integrity of the begin-label. As such, they must satisfy the all conditions for downgrading, described above, with the exception that even if robustness checking is enabled, auto-endorse clauses do not need to satisfy the robustness constraints.

Method conformance

When a method declaration overrides or implements a method declared in a ancestor class or interface, the method declaration must conform with the previous declaration. Method conformance in Jif extends method conformance in Java, due to the addition of labels and where clauses associated with method declarations.

Any label clause L1 <= L2 or actsfor clause p1 actsfor p2 appearing in the overriding method declaration must be implied by the label clauses and actsfor clauses of the overridden method. In the following example, the label and actsfor clauses of the method D.m are implied by the clauses of C.m, but this is not true for the method D.m.

abstract class C {
    abstract void m(label lbl, principal pr) 
        where lbl <= {Alice→pr}, 
              Bob actsfor pr, 
              pr actsfor Chuck;
}
class D extends C {
    void m(label lbl, principal pr) 
        where lbl <= {Alice→Bob}, Bob actsfor Chuck
        // These where clauses are implied by
        // the where clauses for C.m
    {
        ...
    }
}
class E extends C {
    void m(label lbl, principal pr) 
        where lbl <= {pr->}, Alice actsfor Bob
        // These where clauses are NOT implied by
        // the where clauses for C.m
    {
        ...
    }
}

The return value label, end-label and exception labels of a method are covariant. This means, for example, that if Lsub is the return value label of the overriding method, and Lsup is the return value label of the overridden method, then we must have LsubLsup. By contrast, the begin-label and argument labels of a method are contravariant, meaning that if Lsub is the begin-label of the overriding method, and Lsup is the begin-label of the overridden method, then we must have LsupLsub.

Method calls

Evaluation of a method call e.m(e1, ..., en) proceeds by evaluating e, and then evaluating e1 to en in turn. Then, if e evaluated to null, a NullPointerException is thrown. Otherwise, the method m is invoked.

A static method call T.m(e1, ..., en) first "evaluates" the type T, and then the arguments e1 to en. Evaluating the type T means evaluating any actual parameters to the class type. For example, Bar[pr, this.lbl].m(2+5) is evaluated by first evaluating pr and this.lbl, then the argument 2+5, and finally invoking the method.

The principals and labels of a method signature may mention the formal arguments of the method, the formal parameters of the class, or the this object. To label check a method call, the principals and labels in the method signature have substitution performed on them: formal arguments are replaced with actual arguments, formal parameters are replaced with actual parameters based on the type of the receiver, and this is replaced with the receiver of the method call. The example below demonstrates this.

int{*foo.lbl; x; p<-*} m{*this.bound}(C foo, 
                                      principal p, 
                                      int{p→} x) { ... }
...
a.b.m(bar, Alice, y);
// after substitution, the begin-label is {*a.b.bound}, 
//    the return value label is {*bar.lbl; y; Alice<-*}, 
//    and the label of the 3rd argument is {Alice→}

For the remainder of this section, we assume that the labels of the method signature have had substitution performed on them.

The labels of the actual arguments must be no more restrictive than the labels of the arguments of the method signature. In particular, if Li is the normal value label of the ith actual argument, and L'i is the label of the ith formal argument, then we must have LiL'i.

Let pcinv be the program counter label just before the method is invoked, that is, pcinv is the normal termination label after evaluating the receiver e and arguments e1 to en (and possibly throwing the NullPointerException). We require that pcinv must be no more restrictive than the method's begin-label, since the method's begin-label is an upper bound on the program counter label at the method call. Also, the begin-label of the current method must be no more restrictive than the method's begin-label, since the current method's begin label is a lower bound on side-effects of the method, and the method's begin-label is a lower bound on the side-effects that may occur during the invocation of the method.

Any where label clauses and actsfor clauses of the callee method must be implied by the label environment at the call site.

The normal termination label of a method call is the join of pcinv and the method's end-label. The method invocation may throw an exception, in accordance with the method's throws clause. The label associated with an exception thrown by the method invocation is pcinv joined with label of the exception as declared in the method's throws clause. If the method returns a value, then the normal value label of the method invocation is the join of pcinv and the method's return value label.

Constructors

Constructing a new object by calling new T(e1, ..., en) is label checked very much like a static method call. The normal value label of a new expression is the join of the end-label of the constructor with the program counter label just before the constructor is invoked (that is, the normal termination label of en).

Label checking of constructor declarations differs from label checking method declarations. For soundness, all final fields of a class must be initialized before the call to the super class constructor. Thus, in Jif constructor declarations, code may appear before the call to super(...); this code is called the constructor prologue.

During the constructor prologue, no references to the this object are allowed to escape. This means that the this object cannot appear as the target of any method call, or as the argument to any method call, or as the value of any assignment. Because of these restrictions, label checking for the constructor prologue can be more permissive. In particular, the program counter label for checking the constructor prologue is initially the least restrictive label {⊥→⊥;⊤←⊤}, and assignments to fields of the this object are not considered side effects (since they are not observable) and so the label of the assigned field does not have to be bounded below by the constructor's begin-label.

Invoking a constructor via a super(...) call or this(...) call within a constructor declaration is label checked like a static method call. Code after the invocation of the super(...) constructor is label checked like normal Jif code.

Classes

Label checking a class requires label checking each class member, including constructor declarations, method declarations, and field declarations.

Jif supports static fields, but the declared labels of static fields cannot contain the label {this} or any label or principal parameters. If the label of a (non-static) field contains the label {this} or a covariant label parameter, then the field must be declared final. If a field declaration includes an initializing expression, then the normal value label of the initializing expression must be no more restrictive than the declared label of the field.

Jif does not currently support instance initializer blocks or static initializer blocks.

Jif classes may optionally declare an authority set (see Authority and access control). If the immediate superclass of the class being declared has the authority of a principal p, then the class being declared must also have the authority of the principal p.