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.
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.
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.
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.
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
}
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.
try {
if (i < 0)
throw new Exception();
}
catch (Exception e) { }
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 e1⊕e2 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.
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.
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 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.
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.
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,
L ⊑ L' 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 L ⊑ L'.
Consider the following example.
class C[covariant label L, label M] { }
class D[covariant label L] extends C[L, {Alice→}] { }
C[{Bob→Chuck}, {Dave→}] is a subtype of
C[{Bob→}, {Dave→}]
C[{Bob→}, {Dave→Chuck}] is not a subtype of
C[{Bob→}, {Dave→}]
C[{Bob→}, {Dave→}] is not a subtype of
C[{Bob→Chuck}, {Dave→}]
D[{Bob→Chuck,Dave}] is a subtype of
C[{Bob→Chuck}, {Alice→}]
D[lbl] is a subtype of C[{Bob→Chuck},
{Alice→}] if it can be shown that lbl ⊑ {Bob→Chuck}.
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.
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.)
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.
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.
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.
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 e1
⊑ e2. 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 e1 ≽ e2.
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
{⊤→⊤;⊥←⊥}.
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.
Declassifications may only downgrade confidentiality, and endorsements may only downgrade integrity.
All declassifications and endorsements must have sufficient authority. In particular, if a declassification or endorsement weakens or removes a policy owned by principal p, then the code that performs the downgrade must have the authority of p (or a principal able to act for p).
Robustness is a useful security condition, which ensures that both the decision to downgrade and the data to downgrade are of sufficiently high integrity that an attacker cannot abuse the downgrade operation to inappropriately view or modify information. The Jif compiler enforces label constraints for robustness, as described in [CM06], which provides details of the security condition, and the motivation for the constraints.
The actual label constraints to enforce these requirements are given below, during the presentation of declassification and endorsement.
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.
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.
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.
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.
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.
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_pc⊑Lto. 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 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.
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.
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.
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.
The writersOnly(L) operator removes the confidentiality policy of L, and is simply equivalent to L ⊔ {⊤→⊤;⊤←⊤}.
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_pc⊑Lto. 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.
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.
throws clause has a label associated with it.
void).
In addition, a method may have a number of where clauses, which may take any of the following forms.
<= L2
actsfor p2
authority(p)
caller(p)
endorse(Len)
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_pc ⊑ Len. 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 LC ⊑ LD ⊔
caller_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.
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 Lsub ⊑ Lsup. 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 Lsup ⊑ Lsub.
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 Li ⊑ L'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.
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.
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.