Jif is an extension to the Java programming language that adds static analysis of information flow for improved security assurance. The primary goal is to prevent confidential information from being used improperly; in some versions of Jif, the goal is also to protect the integrity of trusted information.
The largest difference between Jif and Java is the addition of labels that express security policies as restrictions on how information may be used. These labels facilitate statically tracking information flow. The analysis of information flow is performed mostly statically, at compile time. However, Jif does also support some forms of run-time security enforcement.
Static checking of information flow in Jif programs is performed as part of type checking. If a Jif program type-checks, the compiler translates it into Java code that can be compiled with a standard Java compiler. The Jif compiler and run-time system are available from the Jif web site.
Jif is based on the JFlow language described in the Practical Mostly-Static Information Flow Control, published in the Proceedings of the 26th ACM Symposium on Principles of Programming Languages (POPL), pp. 228-241, January 1999, by Andrew C. Myers. Another source of documentation for Jif is Andrew Myers' Ph.D. dissertation. However, the language has evolved since that time, and some features in this version of Jif are not documented in the thesis.
Jif has a number of unique 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).
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 information 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.
For example, a variable may be declared with this labeled type:
int{p:} x = 2;
In general,
a label is written as a set of policy expressions,
separated by semicolons. For example,
the label expression
{o1: r1,r2; o2: r2,r3} contains two policy expressions.
A policy expression owner:
reader1,
reader2, ...
means that the
principal owner wants to allow the labeled
information to flow to at most the principals
readeri. Labels built from these
policies are called decentralized labels because they
enforce security on behalf of the owning principals, not on
behalf of an implicitly centralized policy specifier.
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. This is written formally as L1 ⊑ L2. (The ordering ⊑ defines a preorder on labels in which the equivalence classes form a join semilattice.)
When differently labeled inputs are
combined, 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 will be introduced later.
A labeled type may occur in a Jif program almost anywhere a type may occur in a Java program. In fact, if the label is omitted from a type, the Jif compiler automatically generates a label for that type according to rules that are discussed 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])
In the decentralized label model implemented by Jif, information is owned by, updated by, and released to principals: users and other authority entities such as groups or roles. For example, both users and groups in Unix would be modeled as principals.
Some principals may be authorized to act for
other principals. If the principal p acts for the
principal q, any action taken by p
is implicitly assumed to be authorized by q.
The acts-for relation is reflexive and transitive,
defining a hierarchy or partial order
of principals. This relation is similar to the speaks for
relation used in various authentication logics (e.g., [LABW91]);
the hierarchy of principals is also similar to a role hierarchy
[RBAC].
The acts-for relation can be used to model groups and
roles conveniently. A group principal, such as students,
is modeled by authorizing all of the principals
representing members of the group
to act for the group principal. That is, the group principal delegates
its authority to all of the group members. A
role, a restricted form of a user's authority, is modeled by
authorizing the user's principal to act for the role principal.
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 below), the compiler makes use of
the knowledge that the relationship exists when checking
information flows and comparing security policies.
As discussed below, Jif 2.0.0 adds 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 is a boolean variable:
boolean l = false;
if (h) {
l = true;
}
If l contains public (low) information and h
contains secret (high) 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 (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 exceptions.)
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 will ensure 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.
The syntax of a Jif method declaration has some extensions when compared to 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 each may be given their own individual label. There are two optional labels in a method declaration called the begin-label and the end-label. The begin-label is used to specify any restriction 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{} o, int{} 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. (Parametric
polymorphism over labels is discussed later).
The method setElementAt in this declaration
is prevented from leaking information
by its declared begin-label, {L}.
It can be called only if the pc of the
caller is no more restrictive than {L}. The labels of the
arguments o and i are written as
{}, but as discussed in the
following section, argument labels automatically
include the begin-label,
so both arguments are effectively labeled by {L}.
The end-label of a method specifies the pc at the point of termination
of the method, and captures the restrictions on the information that
can 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.
A powerful feature of Jif is automatic inference of the labels of local variables. The Jif compiler can figure out whether there is a way of labeling local variables to satisfy all the label constraints. However, most of the time you do need to write down labels of fields and method signatures, including the begin-label, end-label, result label and arguments' labels. When these labels are missing, some conservatives rules are used to assign restrictive default labels:
{}
{}, which is conservative because no
confidential data can be stored in the field.
<top>
<top>
<top>, the most restrictive label, meaning
that the method has no side effects.
{}.
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, and controls the ability to declassify data. This simple authority mechanism can be used to build more complex access control mechanisms. It is also useful for releasing information.
At any given point within a program, the compiler understands the code to be running with the ability to act for 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.
The static checker maintains a notion of the static principal
hierarchy at every point in the program. The static principal hierarchy
is a set of acts-for relations that are known to exist. The static
principal hierarchy is a subset of the acts-for relations that exist in
the true principal hierarchy.
The static authority of a method may be augmented by testing the
principal hierarchy dynamically, using the
actsfor test.
A program can use its authority to declassify information according to the the decentralized label model. Declassification weakens the policies restricting how the information can be used. It provides an escape hatch from strict information flow control, which is important for writing realistic programs. Importantly, the use of declassification is mediated by the static authority of the program.
The expression declassify(e,
L1, L2)
relabels the result of an expression e
from the initial label L1 to
the label L2.
Declassification is checked statically, using the static
authority at the point of declassification. The
declassify expression
may relax only the policies owned by principals in the static authority.
It is also possible to omit the label
L1 in the expression, though
this form is deprecated.
A program also can use its authority to declassify the program-counter
label. This functionality is provided by the Jif statement
declassify(L) S,
which executes the statement S
using the program-counter label L.
This form of declassification is
also checked statically. For example, the following is an example of
a declassify statement.
int b;
int y = 0;
if (b) {
declassify ({y}) y = 1;
}
Assuming that the label of y is not more restrictive than
the label of b, 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. The legitimacy of the declassification is
statically checked using the label of y and the static authority
of the program at this point. Note that the labels of
b and y are
both automatically inferred in this example; these automatically inferred
labels are not a problem for checking declassification statically.
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)
...
}
}
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, the following method
receives authority for a principal p that is
determined at run time and passed as an argument to the
method.
void m(principal p) where caller(p) {
// this method body has the
// authority of the dynamic principal p
...
}
}
A final annotation for method declarations is a clause of
the form where p actsfor q. When
this clause is present, the method can be called only from a
context where the specified relationship can be statically
determined to hold. The body of the method is checked under
the assumption that the specified relationship does hold.
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.
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 (discussed later). 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 a 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 the section on 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{} o, int{} 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,
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} contents;
}
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}.
When a parameterized or unparameterized type inherits from a superclass, or implements an interface, the supertype may be an instantiation. The instantiation 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.
A new feature in Jif 2.0.0 is that
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.
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};
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}. 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's 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. 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[this.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, method arguments in Jif are always implicitly
final. This change makes the use of first-class principals and labels
more convenient. 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 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"
}
}
}
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 {*lb} <= {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.
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 name();
boolean delegatesTo(principal p);
boolean equals(Principal p);
boolean isAuthorized(Object authPrf,
Closure[this, lb] closure,
label lb) where authority (this);
Principal{this;p}[] findChainUpto{p;this}(Principal p);
Principal{this;q}[] findChainDownto{q;this}(Principal q);
}
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; two
principals p and q are regarded as being
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 findChainUpto(Principal p) and
findChainDownto(Principal p) are used to search for a
"delegates chain", a chain of principals between two principals, which
is proof that the principal at the head of the chain is able to act
for the principal at the tail of the chain.
The method isAuthorized(Object authPrf, Closure[this, lb]
closure, label lb) is used to determine if the object
authCode is sufficient proof for the principal
represented by the receiver object to grant its authority to execute
the Closure. The form of the authorization proof will
depend on the principal implementation, but could be, for example, a
password, or a certificate, or some other capability.
A Closure[principal P, label L] (see
$JIF/sig-src/jif/lang/Closure.java) is code that needs the authority of
the principal P to execute, and whose side effects are bounded below
by L. To execute a closure, a Capability (see
$JIF/sig-src/jif/lang/Capability.java) is required. 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 isAuthorized(authPrf, c,
lb) called with receiver principal p returns true, and null
otherwise.
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
delegates-chains 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.
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 the expression 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 prevent this covert
channel, Jif requires subclasses of
RuntimeException to be checked.
To reduce the additional programming burden of handling runtime
exceptions, this version of Jif has a simple not-null analysis, which
tracks whether local variables and final fields of the
this object are definitely not-null. Thus, in the following
example, the method m(Object, String) cannot throw a
NullPointerException, 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) {
try {
((String)o).length();
// OK, if instanceof succeeds, o is not-null
}
catch (ClassCastException e) {
// still need to catch the ClassCastException
}
}
if (f != null) {
f.length(); // OK, f is final field of this.
}
if (another.f != null) {
try {
f.length();
}
catch (NullPointerException e) {
// still need to catch the NPE, as we cannot reason
// about fields of objects other than this.
}
}
}
}
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;
}
}
The assignment to the field p must occur
before the call to super. In fact, in Java no code may
precede the call to super.
Note that this example has an assignment from n (with label
{q:}) to the field name (with label
{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.
main methodJif provides two possible signatures for the main method of a class. The first is compatible with the signature for Java main methods, and accepts a single argument of an array of String, that is,
public static void main(String[] args) { ... }
The second signature takes two arguments, the first a principal, and the second an array of String:
public static void main(principal p, String[] args) { ... }
The principal p is the principal representing the current user that invoked the main. The signature
may optionally have the authority of the current user:
public static void main(principal p, String[] args) where caller(p)
{
...
}
main.
The Jif compiler provides a mechanism to allow Jif code to be compiled against and linked to existing Java classes. However, appropriate Jif signatures must be supplied for the Java classes. NOTE: the Jif compiler does not verify that the Java code conforms to these provided signatures.
Suppose that you have an existing Java class, called Foo,
i.e. you have a file Foo.java, and a file
Foo.class that was produced by compiling
Foo.java. Furthermore, suppose you want to use the class
Foo in some Jif code you are writing. You can do this by supplying a
Jif signature for the class Foo; at compile time, your Jif code will
be compiled against the signature you provide, but at runtime the
original Foo.class will be loaded. The steps for doing this are as
follows:
Foo.jif write an appropriate Jif signature for the
methods and fields in the class Foo. Take a look at
$JIF/sig-src/java/lang/*.jif for some examples of this.
Note the use of the native flag to avoid the need to provide a
body for the methods. Note also that there is a private static int
field named __JIF_SIG_OF_JAVA_CLASS$20030619; this is a hack to
let the Jif compiler to know that the class provides a Jif
signature for an existing Java class.
Foo.jif to produce the file Foo.class
Foo.class you created in step 2 is on the
signature classpath. Do this either by dropping the class file into
the $JIF/sig-classes directory, or by specifying the directory with
the -sigcp flag to the Jif compiler. (If you use the -sigcp
flag you will probably also need to explicitly add the
$JIF/sig-classes directory to the signature classpath, e.g. use
-sigcp my-sig-classes:$JIF/sig-classes)
Foo.class is on the classpath, but
that the Foo.class you created in step 2 is not. Now, when you
run your Jif compiled code, the original Foo.class will be loaded
by the classloader.
Tracking down and correcting compilation errors in Jif code can be difficult. While there is not as yet a debugger specifically for the Jif language, the Jif compiler has a number of reporting options that will result in additional information being displayed.
The -explain or -e flag of the Jif compiler can be used to view
more information about failed label checking. For example, consider
the program, in which there is a potential implicit information flow
from the high security argument h, whose label is the dynamic label
lbl, to the low security local variable l:
class Implicit {
void m(boolean{*lbl} h, label{} lbl) {
if (lbl <= new label {Alice:}) {
boolean{} l = false;
if (h) {
l = true;
}
}
}
}
$ $JIF/bin/jifc Implicit.jif
Implicit.jif:6: Label of right hand side not less restrictive
than the label for local variable l
l = true;
^
1 error.
More information can be gleaned by using the -explain flag:
$ $JIF/bin/jifc Implicit.jif -explain
Implicit.jif:6: Unsatisfiable constraint:
rhs.nv <= label of var l
{h} <= {lbl}
in environment
[{*lbl} <= {Alice: }]
Label Descriptions
------------------
- rhs.nv = label of successful evaluation of right hand of assignment
- rhs.nv = {h}
- label of var l = {lbl}
More information is revealed by the successful evaluation of the right
hand side of the assignment than is allowed to flow to the local variable
l.
l = true;
^
1 error.
The more detailed error message first shows what the symbolic
unsatisfiable constraint is (rhs.nv <= label of var l),
and then shows the same constraints with the actual labels substituted
for the symbols ({h} <= {lbl}). The label environment in
which the constraint must be satisfied is also shown. Here, the
environment indicates that the value held in the label variable
lbl is bounded above by the label
{Alice:}. Brief descriptions of the labels that appear in
the unsatisfiable constraint are also shown. Here, we see that
rhs.nv represents the label of the information that may
be acquired by knowing the value of the successful
(normal) evaluation of the right hand
side of the assignment; for this assignment, that label is
{h}, the label of the actual argument h.
Sometimes the additional information provided by the -explain option
is not sufficient to determine why a Jif program fails to
compile. There are two additional useful ways to gain more information
about the label checking process: reporting the topics debug and
solver.
Specifying the command line option -report debug=n, where n is a
non-negative integer, will display more information about labels. The
higher the value for n, the more information is displayed. For
example:
$ $JIF/bin/jifc Implicit.jif -report debug=1 -explain
Implicit.jif:6: Unsatisfiable constraint:
rhs.nv <= label of var l
{<arg h {<dynamic lbl>}>} <= {<arg lbl {}>}
in environment
[{<dynamic lbl>} <= {<pr-external Alice>: }]
Label Descriptions
------------------
- rhs.nv = label of successful evaluation of right hand of assignment
- rhs.nv = {<arg h {<dynamic lbl>}>}
- label of var l = {<arg lbl {}>}
More information is revealed by the successful evaluation of the right
hand side of the assignment than is allowed to flow to the local variable
l.
l = true;
^
1 error.
In the environment, we see that the label of the actual argument
for h is displayed as <arg h {<dynamic
lbl>}>. That is, we see that the label is the argument
label for the argument h, and that this arg-label is
bounded above by the label <dynamic lbl>, that is by the dynamic label
lbl.
The arg-label for h would normally be displayed simply
as h, and the dynamic label lbl would normal
be displayed as *lbl. But with the debug
topic reporting at level 1, we see more detail about the labels, which
can be helpful to determine what reasoning the compiler is
performing. Setting the report level higher reveals even more
information.
Thus, reporting the debug topic provides more information about the labels and their meaning, but a less readable display.
Specifying the command line option -report solver=n, for a
nonnegative n, will display more information about the constraint
solver, which attempts to solve the system of constraints generated by
label checking. The higher the value for n, the more information is
displayed.
When the constraint solver is unable to solve a system of constraints, it attempts to find the most appropriate constraint to "blame": this is the constraint that is displayed in the error message. However, sometimes this constraint is not the real culprit, and one or more other constraints are really preventing successful compilation. Enabling reporting for the solver allows the user to determine which constraint(s) are problematic, when the error message does not appear to be helpful.
To interact with the external environment, Jif provides a runtime
interface to allow Jif code to read and write files, and access stdin,
stdout and stderr, and also to obtain a principal representing the current user. The runtime interface is jif.runtime.Runtime.
Although the runtime code is itself is written in Java (see $JIF/rt-src/jif/runtime/Runtime.java), a Jif signature is provided to allow calls to this interface can be checked statically (see $JIF/sig-src/jif/runtime/Runtime.jif).