Language features

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).

Lexical considerations

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.

Labeled types

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 L1L2.

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, ST and L1L2 iff S{L1} ≤ T{L2} (as in [VSI96])

Label inference

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.

Principals and 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.

Implicit flows and program-counter labels

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.

Method declarations

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 class Vector 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.

Default labels

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:

Authority and access control

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.

Authority declarations

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

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 classes

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.

Label and principal parameters

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.

Parameter inference

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.

Interactions with object types

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.

Using parameters at run time

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.

Dynamic labels and principals

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[, pp] foo = new C[, pp]();
        C[{Alice→foo.q}, P] quux = null;

        int{→; *} 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"

Label expressions

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.

Run-time tests of labels and principals

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

User-defined principals

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);
                     findProofUpto{this←*}(Principal p, Object searchState);
                     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 constraints

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;

Constant arrays

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

Other differences from Java

Jif makes several less significant changes to Java that are necessary in order to reason securely about information flow.

Static fields

Static fields of classes are supported in Jif, subject to the following restrictions.

  1. If a static field has an initializing expression, the expression must contain only constant values. Without this restriction, the initializing expression could be used to convey information about when the class is loaded (e.g., by calling a method), which may depend on sensitive information.
  2. The label of a static field cannot mention this (as this is not valid in a static context).
  3. The label of a static field cannot mention any class parameters (as class parameters are specific to an instance of the class).

Runtime exceptions

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) {
        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

Final field initialization

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;
        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.

Unsupported Java features

Jif does not currently support nested classes, initializer blocks, or threads.