Jif provides the ability to label information manipulated by programs with security policies, enabling the compiler to enforce the security of that information. However, this core capability is not enough to make language-based information flow a viable approach. Jif has several additional features that are important for building interesting programs in a security-typed language:
Jif is not completely a superset of Java. Certain features have been omitted to make information flow control tractable. Also, Jif does not eliminate all possible information leaks (particularly, various kinds of timing channels).
Like Java programs, Jif programs are sequences of Unicode characters. Certain
parts of Jif syntax may be written using either ASCII characters or Unicode
characters. The Unicode characters are the preferred presentation form. The Jif
compiler expects files to be in UTF-8 encoding, which means that
pure ASCII input will work correctly, and that editors supporting UTF-8
(e.g., vim) will
display any Unicode characters correctly. Standard Java Unicode escapes
(starting with \u) are also supported.
The non-ASCII characters that are special lexical tokens for Jif are the following: ⊥, ⊤, →, ←, ⊓, ⊔. They are used for writing label expressions.
In Jif, every value has a labeled type that consists of two parts:
an ordinary Java type such as int,
and a label that describes how
the value can be used.
Any type expression t
may be labeled with any label expression l.
This labeled type expression is written t{l}; for example, the
labeled type int{p→}
represents an integer that principal p owns
and that only p can read.
A variable may be declared with this labeled type:
int{p→} x = 2;
This labeled type may also be written as int{p->} or
int{p:}. The syntax of labels is described earlier (see Label syntax in Jif).
The compiler permits information to flow between locations with different labels only if that information flow does not lose policy restrictions. In particular, if information is able to flow from a location with label L1 to a location with label L2, the label L2 must be more restrictive than L1, or equally restrictive. In other words, the compiler checks that L1 ⊑ L2.
When computation combines several input values to produce a result,
the result may reveal information about
any of the inputs. For example, when two variables
x and y are added, the sum
x+y may reveal information about both
x and y. Conservatively,
the label of the result is the union of the policies
in the labels of the inputs. This union is the
join or least upper bound
of the input labels. For example, if the label of
x is {p→q} and the label of
y is {a→b; p→q,r}, the
label of the result is {p→q; a→b; p→q,r},
which is equivalent to {p→q; a→b}.
In a program, a policy component of a label
may take a few additional forms. One such
form is a variable name, which denotes the set of policies
in the label of the variable named. For example, suppose
that a is a variable and hence has a labeled type.
The label expression {a} contains a single component expression;
this label means that value it labels should be as restricted as the
contents of a are. The more complex
label expression {a; o→r} contains two policy components,
indicating
that the labeled value should be as restricted as a is, and also that
the principal o restricts the value to be read by at most
the principal r.
Other kinds of label components are introduced later.
The type and label parts of a labeled type act largely independently. The notation S ≤ T is used here to mean that the type S is a subtype of the type T. The intuitive behavior of subtyping is that it operates independently on the type and label: for any two types S and T and labels L1 and L2, S ≤ T and L1 ⊑ L2 iff S{L1} ≤ T{L2} (as in [VSI96])
A labeled type may occur in a Jif program almost anywhere a type may occur in a Java program. If the label is omitted from a type, the Jif compiler automatically generates a label for that type according to certain rules. In particular, labels on local variables are automatically inferred by the Jif compiler in a way that satisfies the constraints on information flow, if possible. Not all omitted labels are inferred; other labels, such as on method arguments, are generated automatically using defaults (see Default labels).
For example, in the following code the label on the variable y
is inferred automatically as {Bob→Alice}:
int{Bob→Alice} x;
int{Bob→Alice} z;
int y = x;
z = y;
Usually, it is not necessary to annotate local variables with labels. The labels appearing in method signatures are enough to infer their labels.
actsfor
Jif supports principals as defined in the DLM (see
Principals).
The acts-for relationship between two principals can be tested in a Jif program
using the built-in actsfor operator. The boolean expression
p actsfor q evaluates to true if the specified
relationship exists. Within the body of an if statement
conditioned on this test (see Run-time tests of labels and principals), the compiler
makes use of the knowledge that the relationship exists when checking
information flows and comparing security policies.
Jif also provides support for user-defined principals and user-defined authentication mechanisms.
The label of an expression's value varies depending on the evaluation context. This is needed to prevent leaks through implicit flows: channels created by the control flow structure itself. To prevent information leaks through implicit flows, the compiler associates a program-counter label (pc) with every statement and expression, representing the information that might be learned from the knowledge that the statement or expression was evaluated.
For example, consider the following program, which is obviously
equivalent to the statement l = h, assuming
h and l are boolean variables:
l = false;
if (h) {
l = true;
}
If l contains public (low confidentiality) information
and h contains secret (high confidentiality) information,
this program is not secure. The solution is that by conditioning on
the variable h, the if statement makes the
pc of the assignment to l at least as restrictive
as {h}. Assume no information can be learned from the
fact that the program is executed, and that the program executes with
the highest possible integrity (that is, initially
pc = {*←*}). In this case, the value
of pc during the consequent clause is {h}. After
the if statement, it is again true that pc =
{*←*}, because no information about h can be
deduced from the fact that the statement after the if
statement is executed. (It is not true in general that the value of
pc reverts after if statements, but is true here
because this if statement always terminates without
throwing an exception.) The label of a literal expression (e.g.,
true) is the same as its pc, or {h}
in this case. So the assignment is permitted only if the label
{l} is at least as restrictive as the label
{h}. This would not be true if l were public
and h secret.
One way to think about the program-counter label is that there is a distinct pc for every basic block in the program. In general, the flow of control within a program depends on the values of certain expressions. At any given point during execution, various values vi have been observed in order to decide to arrive at the current basic block; therefore, the labels of these values affect the current pc. The Jif type system ensures that the pc label is at least as restrictive as the labels of all the variables on which the program counter depends.
A related issue is the transmission of information through
the termination or non-termination of a program.
Consider the execution of a while statement
while (h != 0) { ... }.
According to the Jif type system,
assuming that initially pc={*←*}, then
after the statement terminates, pc={*←*}, using the
same reasoning as for the if statement. This
labeling might seem strange, because we
know the value of h when we arrive at the final basic block.
However, arriving at the final block gives no
information about the value of h before the code started.
Therefore,
Jif does not attempt to control information transfers through
termination channels. It also ignores timing channels, which are
an issue for concurrent programming languages. Jif does not support
the Java thread model for concurrent programming.
Jif method declaration syntax extends Java syntax; there are a few optional annotations, including annotations for controlling information flow and for managing code authority.
In a Jif method declaration, the return value, the arguments, and the exceptions may each be annotated with a label. There are additionally two optional labels in a method declaration called the begin-label and the end-label. The begin-label specifies an upper bound on pc at the point of invocation of the method. The begin-label allows information about the pc of the caller to be used for statically checking the implementation, thereby preventing assignments within the method from creating implicit flows of information.
For example, a Jif version of the Java classVector looks like the following:
public class Vector[label L] extends AbstractList[L] {
private int{L} length;
private Object{L}[]{L} elements;
public Vector() ...
public Object elementAt(int i):{L; i}
throws IndexOutOfBoundsException {
...
return elements[i];
}
public void setElementAt{L}(Object{L} o, int{L} i) ...
public int{L} size() { return length; }
public void clear{L}() ...
...
}
This code provides several examples of Jif method
declarations. The class is generic with respect to a label
parameter L, permitting Vectors to be used to
store information of any one desired label. (See
Parameterized classes
for information on parametric polymorphism over labels).
The method setElementAt has a declared begin-label,
{L}, occurring between the method name and the list of
arguments. The begin-label ensures that the method can be called only
if the pc of the caller is no more restrictive than
{L}; the begin-label also ensures that the method can
only update locations with a label at least as restrictive as
{L} (such as the elements array). These two
restrictions combined ensure that there will not be implicit
information flow via invocation of the method.
The labels of the formal arguments o and i
of the method setElementAt are {L}, meaning
that {L} is an upper bound on the label of any actual
arguments. Argument labels are discussed more fully in the following
section.
The end-label of a method specifies the pc at the point of termination
of the method, and is an upper bound on the information that
may be learned by observing whether the method terminates normally.
Individual exceptions and the return value itself
also may have their own distinct labels, allowing static
label checking to track information flow at fine granularity. For
example, the end-label of the elementAt method,
{L;i},
means that the pc following normal termination of the
method is at least as
restrictive as both the label parameter L and the label
of the argument i. This
end-label is necessary because when the index-out-of-bounds exception is
thrown, an observation has been made of both the instance variable
elements and the argument i.
Therefore, knowledge of the termination path of the method
may give information about the contents of these two variables.
The labels on local variables are inferred automatically by the compiler. However, most of the time you do need to write down labels for fields and method signatures. These labels include the begin-label, the end-label, the return value label, and the labels of the arguments. When these labels are omitted, default labels are assigned using some simple rules:
{}
{}. This label is the least
confidential, and the least trusted. This conservatively ensures that
no confidential or trusted data can be stored in the field.
{*:}
{*→}
{*→}, the most restrictive label, meaning
that the method has no side effects.
{*←*}.
{}
{}
is assumed. Thus, for example, the array type int[] is
equivalent to the array type int{}[], that is, an array of int{}.
A method executes with some authority that has been granted to it. The authority is essentially the capability to act for some set of principals. The authority of a principal is required to perform actions that may compromise the security of a principal, such as downgrading information. This simple authority mechanism can be used to build more complex access control mechanisms.
For any given method body, the compiler understands the method body to have the authority of some set of principals; the static authority of the code at that point. The actual authority may be greater, because the known principals may be able to act for other principals. The static authority can never exceed the actual authority unless revocation occurs while the program is running.
There are two ways for method code to acquire authority. First, the
class containing the code may declare that it has the
authority of some principal using an authority
clause. A method of the class can then claim and use that
authority if its signature includes a where authority
clause of its own. It is easy to identify the code to which
principal p has directly granted its authority
because of these clauses. For example, in the following code
the class Game has the authority of the
principal referee:
class Game authority(referee) {
void start() where authority(referee) {
// this entire method body has the authority of referee
...
}
void halftimeShow() {
// this method body does not have the authority of referee
// (no "where authority" clause)
...
}
}
Note that if a principal parameter appears in the
authority clause of a class, such as in the example
below, then any code that calls a constructor of the class must have the authority of the instantiation principal.
class C[principal P] authority(P) {
void m() where authority(P) {
...
}
}
...
// this code requires the authority of Alice to construct a C[Alice] object
C[Alice] foo = new C[Alice]();
The second way for a method to acquire authority is for the method to
receive authority passed from another method. If the receiving method
signature contains a clause of the form where caller(p),
then it can be called only from code that is statically known to have
the authority of principal p. For example, in the
following code, the method m executes with the authority
of Alice, and the principals P
and prin, whose identities are not yet determined at
compile time.
class C[principal P] {
void m(principal prin)
where caller(P, Alice, prin)
{
// the method body has the authority of P, Alice, and prin
...
}
}
These mechanisms can be used to implement access control security within a program and are similar in expressiveness to the Java stack inspection mechanism, while avoiding the run-time overhead. Of course, Jif offers more security assurance than stack inspection because it also controls information flow.
Jif's label checking ensures that security policies are enforced on information as the information flows through a program. However, many applications need to weaken the security policies of information as part of their intended functionality. For example, a login program must declassify some information about the (confidential) password when it accepts or rejects the user's login attempt.
Jif provides mechanisms to downgrade the confidentiality and the
integrity of information, via explicit program annotations. The
expression declassify(e, L1 to
L2) relabels the result of an expression
e from the initial label
L1 to the label
L2, where the integrity specified by
L2 must be at least as restrictive as
the integrity specified by L1. That
is, a declassify expression can weaken only the
confidentiality, not the integrity, of information. Similarly, the
expression endorse(e, L1 to
L2) relabels the result of an expression
e from L1 to
L2, where the confidentiality specified
by L2 must be at least as restrictive
as the confidentiality specified by
L1. It is possible to omit the label
L1 in the expression, though
this form is deprecated.
A program may also downgrade the program-counter label pc. This
functionality is provided by the Jif statements
declassify(L1 to L2)
S and endorse(L1 to
L2) S, which each execute the
statement S using the program-counter label
L2. A declassify
statement can weaken only the confidentiality of the program-counter
label, whereas an endorse statement can weaken only the
integrity. Again, it is possible to omit the label
L1 in the expression, though
this form is deprecated. For example, the following is an example of
a declassify statement.
int{Alice→;Alice←*} b;
int{Alice→Bob;Alice←*} y = 0;
if (b) {
// pc is at level {Alice→;Alice←*} at this point.
declassify ({Alice→;Alice←*} to {y}) {
// at this point, pc has been declassified to the label of the local
// variable y (that is, {Alice→Bob;Alice←*} ) permitting the
// assignment to y
y = 1;
}
}
This program declassifies the implicit flow
from b into y. For the duration of
the assignment into y,
the program-counter label is relaxed until it is no more restrictive than
y itself.
Checked endorse.
Many programs need to validate untrusted data and then treat it as more
trustworthy. Jif provides a special form of the endorse
statement to support this pattern. The checked endorse statement
(added in Jif 3.1)
endorses data only if it passes a validation check. It considerably
reduces the awkwardness of performing input validation.
A checked endorse has the following form:
endorse (x, L to L')
if (e) S else S'
where x is a local variable, and
L and L' are labels. The
alternate branch (else S') is optional.
The local variable x has label L'
in the scope of expression e and statement
S, but has its standard label in the scope
of S'. The local variable x
cannot be updated in e or S.
The declassify and endorse expressions and
statements weaken security policies, and as such are powerful and
potentially dangerous mechanisms. To limit the misuse of these
mechanisms, Jif imposes limitations upon their use, to enforce the
security conditions of selective downgrading and
robustness.
Selective downgrading [ML00,PC00] combines access control with
downgrading, ensuring that any downgrading performed by a program has
appropriate authorization. For Jif, this means that any downgrading
expression or statement that weakens a policy owned by a principal
p must have the authority of p. The Jif
compiler checks selective downgrading statically, using the static
authority at the point of downgrading.
Intuitively, robustness [ZM01,MSZ04,CM06] is the property that a principal is unable to affect the release of information to the principal. That is, a principal cannot influence what information is released to him, or when that information is released.
The Jif compiler can statically check constraints that enforce
robustness against all possible principals. When invoking the Jif
compiler, if the flag -robust is specified, then
additional constraints are checked at every declassify
and endorse expression or statement. In brief, these
additional constraints ensure the pc label at any
declassification or endorsement has sufficiently high integrity, and
moreover, the label of any information being declassified must also be
of sufficiently high integrity. More information is provided in [CM05]
and in the Label Checking
section.
Auto-Endorsement. Enforcing robustness requires that both the information to be
downgraded and the decision to downgrade are of sufficiently high
integrity. However, in some situations a principal may be willing to
downgrade information regardless of the integrity of the decision to
downgrade. For example, an application may be prepared to declassify
the average age of all employees when requested, regardless of which
user has requested it. Jif thus contains an auto-endorsement
mechanism, whereby a principal p may automatically vest
the body of a method m with p's trust. The
method body will execute with higher integrity, due to the addition of
p's trust.
Auto-endorsement is specified with a clause where
endorse(L). A method declaration with method body
S and an auto-endorsement clause where
endorse(L) is similar to a method declaration with body
endorse(L0 to L) S, where
L0 is the method's begin
label. However, robustness constraints are not enforced on an
auto-endorsement; only selective downgrading constraints are.
That is, the method requires the authority of any principal whose
security policy is weakened by the auto-endorsement.
Selective downgrading and robustness against all attackers are orthogonal: each provides separate guarantees regarding the downgrading of information. The access control mechanism of selective downgrading interacts with robustness via the auto-endorsement of methods, as a method can only be auto-endorsed if it has sufficient authority.
Libraries of reusable code make up the bulk of most program code. Jif supports various kinds of polymorphism to make it possible to write reusable code that is not tied to any specific security policy.
The most common form of polymorphism is over the labels of
arguments to a method.
When an argument label is omitted, the method is generic
with respect to the label of the argument. Consider
implementing a cosine method cos:
double cos(double x);
Omitting the label on the argument x means that
this method can be applied to an argument x
with any label.
Without label polymorphism, there are two strategies: reimplement it for every argument label ever used, or implement it using run-time labels (see Dynamic labels and principals). The former approach is clearly infeasible. Implicit labels have the advantage over run-time labels that when they provide adequate power, they are easier and cheaper to use.
When formal variables have declared labels, the method is
still polymorphic with respect to the label of the argument;
however, the declared label serves as an upper bound on the allowed
argument labels.
For example, in the following method
signature, the method m returns a String whose
label is the same as the label of the argument a.
String{a} m(int{Alice→; Bob→} a);
The label on the declaration of the argument a is
{Alice→; Bob→}. This means that the label of any actual
argument given to m can be at most as restrictive
as {Alice→; Bob→}, that is, {Alice→; Bob→} is an
upper bound on the label of any actual argument to m. The
following code that calls the method m compiles
successfully.
int{Alice→Chuck} i = 42;
String{Alice→Chuck} s = m(i);
// OK: m returns a String with the same label as i
In the body of the method m, all that is known about
the label of the formal argument a is that {Alice→; Bob→} is an upper bound for it. Thus, the first line of the method body below is illegal, while the second is legal.
String{a} m(int{Alice→; Bob→} a) {
int{Alice→} i = a; // ILLEGAL! Don't know
// that {a} ⊑ {Alice→}
int{Alice→; Bob→; Chuck→} j = a; // OK
...
}
The labels of arguments given to a method are not represented at runtime. That is, within a method body, there is no runtime representation of labels of the arguments. The following code that manipulates run-time labels is thus illegal.
void foo(int{Bob→} a) {
label lb = new label {Alice→; a};
// ILLEGAL! Label of a is not runtime representable.
if (new label {a} <= new label {Bob→Chuck})
// ILLEGAL! Label of a is not runtime representable.
{ ... }
}
If no label is specified for a formal argument, then it is assumed that there are no restrictions on the labels of the actual arguments that may be passed in. (See Default labels).
Parameterized types have long been known to be important for building reusable data structures. A parameterized class is generic with respect to some set of type parameters. This genericity is particularly useful for building collection classes such as generic sets and maps. It is even more important to have polymorphism in the information flow domain; the usual way to handle the absence of statically-checked type polymorphism is to perform dynamic type casts, but this approach works poorly when applied to information flow, because dynamic tests create new information channels.
Jif allows classes and interfaces to be parameterized by explicitly declared
label and principal parameters. The earlier example of a Vector
class demonstrated the use of a label parameter:
public class Vector[label L] extends AbstractList[L] {
private int{L} length;
private Object{L}[]{L} elements;
public Vector() ...
public Object elementAt(int i):{L; i}
throws IndexOutOfBoundsException {
...
return elements[i];
}
public void setElementAt{L}(Object{L} o, int{L} i) ...
public int{L} size() { return length; }
public void clear{L}() ...
...
}
The Vector class is parameterized on a
label L that represents the label of the
contained elements. Assuming that secret and
public are appropriately defined dynamic labels, the
types Vector[secret] and Vector[public]
would represent vectors of elements of differing sensitivity. These
types are referred to as instantiations of the parameterized
type Vector. Without the ability to instantiate
classes on particular labels, it would be necessary to reimplement
Vector for every distinct element label.
A class may also be parameterized with respect to principals, as in this example:
class ParamCell[principal P, principal Q] {
int{P→Q; P←Q} contents;
void m(principal x, principal y) where P actsfor x, Q actsfor y { ... }
}
This class may be instantiated with any two principals
p and q. For example, the instantiation
ParamCell[Bob,Amy] has a field contents with
the label {Bob→Amy; Bob←Amy}, and method
m that requires that parameter principal P
can act for runtime principal x, and parameter principal
Q can act for runtime principal y.
The Jif compiler automatically infers label and principal parameters for local
variables. This makes programming in Jif more convenient, because it is not
necessary to explicitly instantiate parameterized classes in most places where
these types can be mentioned. For example, code using the Vector
or ParamCell classes may declare variables without providing the
parameters:
ParamCell cell; Vector v; cell.m(Alice, Bob); // cell inferred to be of type ParamCell[Alice,Bob] v.setElementAt(null, cell.contents); // v inferred to be of // type Vector[{Alice→Bob}]
Parameters can always be supplied explicitly, which may make the code clearer or may help with debugging.
Some
parameters must still be supplied explicitly. For field declarations
with parameterized types, parameters must be supplied. Parameters must
be provided explicitly for classes and interfaces appearing in an
extends clause, and in method and constructor signatures.
Formal parameters must always be declared, as in the class definition
of Vector and ParamCell. These restrictions
exist because parameter inference in Jif is local to a single method.
When a parameterized or unparameterized type inherits from a superclass, or implements an interface, the supertype may be an instantiated class. The supertype that is inherited from or implemented must be a legal type within the scope of the class that is inheriting from or implementing it. This is a specific instance of a more general rule in Jif: within a parameterized class or interface, the formal parameters of the class may be used as actual parameters to instantiations of parameterized types within its scope.
The presence of label and principal parameters means
instantiations of parameterized classes are simple dependent types,
because types depend on values. To ensure that these dependent types have
a well-defined meaning, only “final”
expressions may be used as parameters;
since they are immutable, their meaning cannot change. An alternative approach
would be to allow all variables to
be used as parameters; however, in that case two different types that
mention the same variable would have different meanings if an assignment
to the variable occurred between them.
Subtyping is ordinarily invariant on class parameters. For example,
even if {*public} ⊑ {*secret}, it is not the case
that Vector[public] ≤ Vector[secret].
(The label ordering is denoted here as ⊑,
and the subtype relation is denoted by ≤.) This subtype
relation would be unsound because Vector is mutable.
When such a subtype relation is sound, the parameter may be declared
as a covariant label rather than as a label. Covariant label parameters
are made sound by placing additional restrictions on their use,
as follows.
A covariant label parameter may not be used to construct the label for
a non-final instance variable. It also may
not be used as an actual parameter to a class whose formal parameter
is a (non-covariant) label. However,
immutable (final) instance variables and method arguments and return
values may be labeled using a covariant parameter.
Although Jif does not support user-defined type parameters, it does support one
type with a type parameter: the built-in Java array type, which is used as the
type of the instance variable elements in the Vector
example. Arrays are parameterized with respect to both the type of the
contained elements and the label of those elements. In the example for
Vector, the type of the instance variable elements is
Object{L}[] which represents an array of Object where
each element in the array is labeled with L. The array type
behaves as though it were a type array[T,L] with two parameters:
an element type and an element label; in this case T =
Object. The label parameter may be omitted, in which case it
defaults to {}. For example, the types int[] and
int{}[] are equal.
All class parameters are represented and accessible
at run time. Thus, the following code,
which uses the parameters L and P at runtime,
is permitted.
class C[label L, principal P] {
private final label{this} lb = L; // runtime use of L
private void m() {
label foo = new label {L; Alice→}; // runtime use of L
principal bar = P; // runtime use of P
}
}
When a parameter is treated as an ordinary value, its label is the label
{this}. That is, the information that may be conveyed by
knowing the run-time value of a parameter is the same as the
information that may be conveyed by the reference to the current
object. Thus, if the label of the final field lb in the
example above was not at least as restrictive as the label
{this}, the example would not compile.
Class parameters may also be used in static contexts, such as a static
method. However, in static contexts, there is no this
object, and so the label of parameters cannot be the label
{this}. Instead, in static contexts, class parameters are
treated as if they were an argument to the context; thus the label of
a class parameter in a static context is essentially unknown.
Labels and principals can be used as first-class values, represented at runtime. These “dynamic” labels and principals can be used in the specification of other labels, and used as the parameters of parameterized classes. (Thus, Jif's type system has dependent types.) Consider the following example.
class C[label L] { ... }
...
void m() {
final label lb = new label {Alice→Bob; Alice←*};
int{*lb; Bob→} x = 4;
C[lb] foo = null;
C[{*lb}] bar = foo;
}
Here we see a local variable lb, of type
label. At runtime, this variable will contain a
representation of the label {Alice→Bob; Alice←*}. The type of the
variable x is declared to be int{*lb; Bob→},
that is, an integer whose label the policy {Bob→} joined
with the value stored in the variable lb. This is
an example of a dynamic label being used in another label.
The variable foo is of type C[lb], that
is, its type is the class C instantiated with the label
that is stored in the variable lb. This type is
equivalent to the type C[{*lb}], since the label stored
in the variable lb is equivalent to the label {*lb}.
Jif allows more than just local variables of type
label and principal to be used to construct
new labels and types. in fact, any final access path expression
may be used. A final access path expression is an expression of the
form r.f1.f2. ... .fn, where
r is either a final local variable, or the expression
this, and each fi is an access to a
final field. (An access path of the form
f1.f2. ... .fn is equivalent to
this.f1.f2. ... .fn.) Thus, the following are all examples of legal
uses of dynamic labels and principals.
class C[label L, principal P] {
final label lb;
final principal q;
final C[lb, Alice] next;
public C() { ... }
void m(principal pp) throws NullPointerException {
final C[next.lb, pp] foo = new C[this.next.lb, pp]();
C[{Alice→foo.q}, P] quux = null;
int{foo.next.q→; *this.lb} x = 8;
}
}
Unlike in Java, formal arguments in Jif are always implicitly
final, meaning that formal arguments may always be used
as the root of final access path expressions. This simple change does
not remove any significant power from the language, since code that
assigns to an argument variable always can be rewritten to use a
non-final local variable instead.
Final access paths appearing in labels and types may act as covert
channels. For example, an access path may throw a null pointer
exception, or the value stored in a particular variable may reveal
sensitive information. The Jif type system must account for the
information that may be revealed whenever a final access path in a label
or type is evaluated at runtime. Final access paths occurring in a
label may be evaluated at runtime when a new label
expression is evaluated; final access paths occurring in a type may be
evaluated at runtime during the evaluation of casts to a parameterized
type, instanceof checks against a parameterized type,
construction of a new object of parameterized type, or a call to a
static method of a parameterized type.
In the following example, an instanceof check is
performed against a parameterized type,
C[{this.f.p→}]. The evaluation of this expression
requires the evaluation of the access path expression
this.f.p, which may throw a
NullPointerException if this.f is
null. Thus, whether or not a NullPointerException is
thrown may reveal information at level {this;
Alice→} (which is the label of the expression this.f).
Thus, if the assignment to the local variable
x occurs, information with the label {this;
Alice→} is flowing, and thus the label of the variable
x must be at least {this; Alice→}.
class C[label L] { ... }
class D {
final D{Alice→} f;
final principal{} p;
...
void m(Object{} o) {
try {
boolean{Alice→; this} x = (o instanceof C[{this.f.p→}]);
}
catch (NullPointerException e) {
// may be thrown by the evaluation of "this.f.p"
}
}
}
A label expression new label {L}
is an explicit run-time representation of the label L. Several examples of valid label expressions are
shown below, where L is a label parameter,
lbl is a dynamic label, and and pr is a
dynamic principal.
new label {Alice->Bob; Alice<-Chuck}
new label {*lbl; Alice→Bob}
new label {L; pr->Alice}
new label {*lbl meet L; Bob->Alice&pr}
new label {*→*; _←_; *←*}
Some labels are not run-time representable, and thus cannot appear
in label expressions. Polymorphic argument labels, and the
this label are not run-time representable.
Jif provides a mechanism for comparing runtime labels, and also a mechanism for comparing runtime principals. Both mechanisms use a syntax similar to that of if statements.
An if-label statement allows the runtime comparison of labels. It has the following form:
if (L1 <= L2) {
...
}
else {
...
}
If the label L2 is at least as restrictive as
the label L1, then the code in the then
branch is executed; otherwise, the code in the else
branch is executed. The else branch is
optional. During the label checking of the then
branch, it is assumed that the label L2 is indeed at least as restrictive as
the label L1. Thus, the following code compiles correctly.
void m(int{*lbl} i, label{} lbl) {
int{Alice→} x;
if (lbl <= new label {Alice→}) {
x = i; // OK, since {*lbl} ⊑ {Alice→}
}
else {
x = 0;
}
}
Note that this construct replaces the switch-label construct that existed in previous versions of Jif.
An actsfor statement allows the runtime comparison of principals. It has the following form:
if (P1 actsfor P2) {
...
}
else {
...
}
If the principal P1 can act for the principal
P2, then the code in the then branch is
executed; otherwise, the code in the else branch is
executed. The else branch is optional. During the label
checking of the then branch, it is assumed that the
principal P1 can act for the principal
P2. Thus, the following code compiles correctly.
void m(int{Alice→pr} i, principal{} pr) {
int{Alice→Bob} x;
if (Bob actsfor pr) {
x = i; // OK, since {Alice→pr} ⊑ {Alice→Bob}
}
else {
x = 0;
}
}
Note that this construct replaces the actsfor { ... } else { ... } construct that existed in previous versions of Jif.
More generally, the dynamic tests for labels and principals can be
used as arbitrary boolean-valued expressions. However, the Jif
compiler will only be able to reason about the additional information
flows permitted by the dynamic tests if the tests occur as a conjunct
of the condition of an if statement, and the operands are
either constants, new label {...} expressions, or final
access paths.
void m(int{Alice→pr} i, principal{} pr, int{*lbl} i, label{} lbl) {
// dynamic label and actsfor tests can be used as boolean-valued
// expressions
boolean b = (lbl <= new label {Alice→pr} || Alice actsfor pr);
int{Alice→Bob} x;
if (8 < 4 || Bob actsfor pr) {
x = i; // BAD: actsfor test is not a
// conjunct of the condition of an if-statement
}
if (lbl <= new label {Alice→pr} && Bob actsfor pr) {
x = i; // OK, compiler can reason that lbl ⊑ {Alice→}
// and Bob actsfor pr
}
}
Jif provides an open-ended mechanism to allow applications written in
Jif to define their own principals. The Jif interface jif.lang.Principal
is used to represent principals, and Jif programs may implement this
interface to define their own principals.
Objects of type jif.lang.Principal can be implicitly
cast to the type principal, and vice-versa.
The interface jif.lang.Principal is defined
as follows:
public interface Principal {
String{this} name();
boolean{this;p;this←*} delegatesTo(principal p);
boolean equals(Principal p);
boolean{authPrf; closure; lb; *lb; this; this←*}
isAuthorized{this←*}(Object authPrf,
Closure[this, lb] closure,
label lb) where authority (this);
ActsForProof{this;p;this←*;p←*}
findProofUpto{this←*}(Principal p, Object searchState);
ActsForProof{this;q;q←*;this←*}
findProofDownto{this←*}(Principal q, Object searchState);
}
The method name() returns the name of the
principal. The equals(Principal p) method is used to
determine if the receiver object is the same as the principal p;
principals p and q are regarded as
equal only if p.equals(q) && q.equals(p).
The method delegatesTo(principal p) returns true if the
principal represented by the receiver object has delegated its
authority to the principal p (and thus p can
act for the principal represented by the receiver object).
The methods findProofUpto(Principal p, Object
searchState) and findProofDownto(Principal p, Object
searchState) are used to search for an
ActsForProof object. An ActsForProof is in
essence a sequence of principals p1, ...,
pn, such that each pi
delegates its authority to pi+1, and is thus a
proof that pn can act for
p1. (In order to handle conjunctive and
disjunctive principals, an ActsForProof has slightly more
structure than simply a chain; however, this implementation detail is
hidden from Jif programmers.)
The parameter searchState is used to prevent infinite
recursion when searching for ActsForProofs;
Implementations of the Principal interface can ignore the
structure of the searchState object, and are just
required to pass it as an additional parameter when recursively trying
to find an ActsForProof (i.e., when calling the method
jif.lang.PrincipalUtil.findActsForProof(Principal p, Principal
q, Object searchState)).
The authority of principals is required for certain operations, such as downgrading information. The authority of principals whose identity is known at compile time may be obtained by these principals examining and approving the code that requires authorization. However, for dynamic principals, whose identity is not known at compile time, a different mechanism is required. Jif provides a mechanism for dynamically authorizing closures.
An authorization closure is an implementation of the
interface jif.lang.Closure, shown below. The
Closure interface has a single method
invoke, and is parameterized on a principal P. Any
code that calls the invoke method must have the authority of
principal P, indicated by the where caller(P) annotation.
public interface Closure[principal P, label L] authority(P) {
Object{this} invoke{L}() where caller(P);
}
The method Principal.isAuthorized(Object authPrf, Closure[this, lb]
closure, label lb) is used to authorize closures,
It takes two arguments: a Closure object instantiated
with the principal represented by the this object, and an
application-specific proof of authentication and/or authorization. The
proof might be a password, or a checkable proof that
the closure satisfies certain safety requirements. The implementation
of the isAuthorized method examines the closure and the proof
object, and returns true if the principal grants its
authority to the closure.
If a principal grants its authority to a closure, the Jif run-time
library constructs a capability, an instance of the class
jif.lang.Capability (shown below) which encapsulates the
closure along with the authority of the appropriate principal. Code
without the authority of the principal may invoke the capability,
which will execute the invoke method of the contained
closure. Thus, obtaining a capability for a closure corresponds to
obtaining a principal's authority to execute the closure. A capability
can only be obtained by calling the method
jif.lang.PrincipalUtil.authorize(principal p, Object authPrf,
Closure[p, lb] c, label lb), which returns a Capability to
execute the closure if the method p.isAuthorized(authPrf, c,
lb) returns true, and null
otherwise.
public final class Capability[principal P, label L] authority(P) {
private Capability(Closure[P,L]{this} closure) { this.closure = closure; }
private final Closure[P, L]{this} closure;
public Closure[P,L]{this} getClosure() { return closure; }
public Object{closure; L} invoke{L}() where authority(P) {
if (closure == null) return null;
return closure.invoke();
}
}
The class jif.lang.AbstractPrincipal (found in the
$JIF/lib-src directory) is an abstract implementation of
jif.lang.Principal that many principal implementations
will find useful. The class jif.lang.PrincipalUtil
contains several utility methods to help in searching for
ActsForProof objects and also for obtaining capabilities to execute
closures.
External principals (e.g., the principals Alice and
Bob mentioned in Jif code; see $JIF/tests/jif/lang/Alice.jif) are
implemented using the class jif.lang.ExternalPrincipal
(found in the $JIF/lib-src directory). You can create your own
external principals in a similar way. See the README file in $JIF/tests for more
information about creating external principals.
NOTE: implementations of the Principal
interface should ensure that the Jif runtime system is notified of any
change in the delegation of authority. In particular, when a principal
adds a delegation, the method
PrincipalUtil.notifyNewDelegation should be called, and
when a delegation is revoked, the method
PrincipalUtil.notifyRevokeDelegation should be
called. These notifications allow the Jif runtime system to correctly
cache acts-for relations. The class
jif.lang.AbstractPrincipal provides convenience methods
for adding and revoking delegations; these convenience methods
correctly notify the Jif runtime system.
Method declarations may contain where clauses, which
may be assumed to hold true during the execution of the method body,
and which the compiler guarantees are true at the method call
sites. We have already seen several of these clauses, in particular,
authority declarations
(authority(p) andcaller(p) clauses), and auto-endorsements. There are two additional
method constraints that may be specified: actsfor clauses, and label
clauses.
An actsfor clause is of the form where p actsfor
q, and specifies that the principal p is able to
act for the principal q. Code in the method body may assume
that this relationship between p and q holds, and code
that calls the method must prove that the relationship holds, possibly
through a dynamic actsfor
test. A variant of an actsfor clause is of the form where
p equiv q, which is equivalent to where
p actsfor q,q actsfor p, that is,
it states that p acts for q and vice versa.
An label clause is of the form where L1 <=
L2, and specifies that the label
L1 is the same or less restrictive than the label
L2. Code in the method body may assume that this
relationship between L1 and L2
holds, and code that calls the method must prove that the relationship
holds, possibly through a dynamic label
test. The clause where L1 equiv
L2 is equivalent to where
L1 <= L2, L2 <=
L1, that is, it states that L1 and
L2 are equivalent labels.
int{*lbl} m{*lbl}(label{*lbl} lbl, principal{*lbl} p, int{Alice→p} i)
where {Alice→Bob} <= lbl, Bob actsfor p
{
// since Bob actsfor p, {Alice→p} <= {Alice→Bob},
// and since {Alice→Bob} <= lbl, the label of the argument i
// is <= {*lbl}. Therefore, we can return i+1.
return i+1;
}
Jif allows the base type of an array to be declared constant, meaning
that the contents of the array cannot change after initialization. The base
type of an array is declared constant by writing const before the
brackets.
// foo is a const array
int{Alice→} const [] foo = {1, 2, 3};
foo[0] = 2; // BAD: cannot assign to an element of
// a constant array
The const modifier applies to all array dimensions. That is, either all
the dimensions of an array are constant, or none of them are.
int const[][] foo = {{1,2,3}, {4,5,6}};
foo[0] = null; // BAD, const applies to all dimensions
foo[0][0] = 4; // BAD, const applies to all dimensions
int [] const [] bar; // BAD, either all or no dimensions
// should be const
New arrays can be cast to either const or non-const arrays.
This includes new arrays created by calling the clone() method of arrays. Note that
Jif ensures that calls to the clone() method on arrays
perform deep copies of the arrays. That is, if
clone() is called on a multi-dimensional array, then the
clone() method is called on each sub-array.
// Same new array expression can be cast
// to both const and non-const arrays
int{} [] foo = {1, 2, 3};
int{} const [] foo2 = {1, 2, 3};
int{} const [] bar = foo.clone(); // OK, since foo.clone()
// is a new array
Constant arrays cannot be cast to non-const arrays, nor vice-versa.
int{} const[] foo = {1, 2, 3};
int{}[] bar = foo; // BAD, cannot assign from a const
// array to a non-const array
foo = bar; // BAD, cannot assign from a non-const
// array to a const array
Constant arrays are covariant, meaning that the label of the base type
of the array may change covariantly. This means, for example, that
the base type of a constant array can have the label {this}, which
is not allowed with a non-constant array.
int{Alice→Bob} const[] foo = {1,2,3};
int{Alice→} const[] bar = foo; // OK, since const arrays
// are covariant and
// {Alice→Bob} <= {Alice→}
// use of the {this} label for base types is ok
final int{this} const[]{this} bar = {1,2,3};
final int{this}[]{this} baz = {1,2,3}; // BAD, cannot use
// the {this} label for base type
// of non-const array
Jif makes several less significant changes to Java that are necessary in order to reason securely about information flow.
Static fields of classes are supported in Jif, subject to the following restrictions.
this (as this is not valid in a static context).In Java, subclasses of RuntimeException (such as
NullPointerException, ClassCastException,
and ArrayIndexOutOfBoundsException) are unchecked;
they may be thrown by a method without being declared in the
throws clause of the method signature. Unchecked
exceptions can serve as covert channels. To control this covert
channel, Jif requires subclasses of
RuntimeException to be checked.
To reduce the additional programming burden of handling runtime
exceptions, Jif has two simple dataflow analyses: a not-null analysis,
which tracks whether local variables and final access paths are
definitely not-null; and a runtime class analysis, which tracks the
precise runtime class of local variables and final access paths via
casts and instanceof tests.
Thus, in the following example, the method m(Object,
String) cannot throw either a NullPointerException
or a ClassCastException, and does not need to declare
that it does.
class C {
final String{} f = "a string";
C another;
void m(Object{} o, String{} s) {
if (s == null) {
return;
}
s.length(); // OK, s known to be not-null
if (o instanceof String) {
// At this point, o is known to be a non-null String object
((String)o).length(); // OK, o cannot be null,
// and the cast will always succeed
}
if (f != null) {
f.length(); // OK, this.f is known to be non-null here.
}
if (another != null) {
try {
String foo = another.f;
}
catch (NullPointerException e) {
// need to catch the NPE, since this.another is not a
// final access path, and the analysis does not track
// if it is non-null
}
}
}
}
In Java, it is possible to observe final fields of an object before
they have been initialized. This is not acceptable in Jif,
where final fields of type label or
principal may define the security requirements
for other information. To ensure that final fields really
are final, Jif constructors are required to initialize all
final fields explicitly before the call to the superclass
constructor. For example, a constructor might look like the
following:
class B extends A {
final principal p;
String {p→} name;
B(principal{} q, String{q→} n) {
p = q;
super(n);
name = n;
}
}
In Jif, the field p must be initialized
before the call to super. In Java, no code is allowed to
precede the call to super.
Note that this example has an assignment from n (with label
{q→}) to the field name (with label
{this.p→}). The assignment is permitted because
the Jif compiler knows from the assignment p=q that these
principals are equal. It uses this fact to determine that
the assignment from n to name is
secure. In general, the Jif compiler can perform this kind of
reasoning only for final fields of type label or
principal that are initialized in a constructor, and
for final local variables of type label or
principal with an initializing expression.