JRIF: Reactive Information Flow Control for Java

Overview

JRIF extends Java to support RIF labels, by modifying the Jif compiler and run time. RIF labels express changes in values' confidentiality and integrity that are instigated by applied operations. For example, a RIF label that tags a vote can express that (i) initially the vote can be read only by the principal that cast this vote, (ii) but the result of the majority (which is derived based on this and other votes) can be read by all principals.

A RIF label consists of two RIF automata; a c-automaton that specifies the confidentiality policy, and an i-automaton that specifies the integrity policy for a value. States of either kind of RIF automaton are mapped to sets of principals, and transitions are mapped to operations. For a c-automaton, these sets contain principals that are allowed to read values. For an i-automaton, these sets contain principals that should be trusted in order for values to be trusted. A visual representation of a c-automaton appropriate for the vote of the example above is shown below, where M identifies the majority operation, \not M identifies all other operations, pi is the principal that cast this vote, P is the set of all principals, \ast identifies all operations, and the grey state represents the initial state.

JRIF allows programmers to tag variables with RIF labels, and generally use RIF labels anywhere that ordinary types are used, specifying confidentiality and integrity restrictions on the corresponding information. RIF labels may be known statically, or they may be created dynamically. In the latter case, RIF labels can be treated as first-order values. For a more complete description of how labels can be used in a Java program, please study Jif's documentation (the syntax of Jif labels, and Jif's features for downgrading and authority are irrelevant for JRIF).

If a JRIF program is type correct, then all RIF labels used in that program are satisfied. In particular, if the value of a variable tagged with RIF label L is derived from the value of another variable tagged with L', by applying some operations, then L should be more restrictive than L' after taking transitions that correspond to these operations. L1 is more restrictive than L2, when L1 allows less principals to read and requires more principals to be trusted, comparing to L2, for all possible derived values.

Syntax

RIF automaton: It is written as a linear representation of an automaton, by listing identified states and transitions. For example, the syntax for the c-automaton of the above figure is:

rif[q1*:{pi},q2:{_},M:q1->q2].

We use {_} to represent the set of all principals, and {} to represent the empty set.

RIF label: It is a pair of a c-automaton (starting with rif) and an i-automaton (starting with rifi). For example:

{rif[q1*:{pi},q2:P,M:q1->q2];rifi[q1*:{pi},q2:{},M:q1->q2]}.

The least restrictive RIF label, which is sometimes written as {}, allows all principals to read and requires no principal to be trusted:

{rif[q1*:{_}];rifi[q1*:{}]}.

Absence of the c-automaton from a RIF label, by default implies that no confidentiality restrictions are imposed. Similarly for the i-automaton.

Annotated expression: Expressions in a program are regarded to be operations; the values of variables in an expression are the inputs, and the value of that expression is the output. Expressions are assumed to be annotated with reclassifiers, which identify these operations. Reclassifiers are used to trigger transitions on RIF automata. Expression E annotated with reclassifier f is written as

 reclassify(E,f).

Expressions that are not explicitly annotated, are assumed to be annotated with a default "empty" reclassifier, which has no effect on RIF automata. Currently, we assume that programmers use reclassifiers ranging from f0 to f9. Discharging this assumption requires a slight modification of the algorithm that decides the restrictiveness relation between two RIF labels, which we leave for future work.

Transitions on RIF labels: New RIF labels can be computed by applying transitions to existing ones. For example, a programmer may write tr(tr(L,f1),f2), meaning the RIF label derived from L, by applying reclassifiers f1 and f2. Notice that L may or may not be statically known.

Examples

1. Reclassifying assigned expression: Reclassifier f1 is applied to x+y. This method is type correct, because (i) the c-automaton of res is more restrictive than the c-automata of x and y after taking the f1 transition, (ii) the c-automaton of the declared exception is more restrictive than the c-automaton of res, and (iii) the c-automaton of res if more restrictive than the c-automaton of the pc (program counter) at the call site of this method. In general, the specified RIF label of the pc at the call site of a method is written between the name and the arguments of that method. In this case, this RIF label is {}.

public static void  main {} (String[] args) throws (Exception{rif[q1*:{Alice}]}) {

    int {rif[q1*:{Alice}]} res; 
    int {rif[q1*:{Alice,Bob},q2:{Alice},f1:q1->q2]} x;
    int {rif[q1*:{Alice},q2:{Alice,Bob},f1:q1->q2]} y; 
    
    res = reclassify(x+y,f1);
    
    throw new Exception("Result: "+res);
    
}

2. Reclassifying guard expression: Reclassifier f1 is applied to x==y. This snippet is type correct, because the c-automaton of res is more restrictive than the c-automata of x and y after taking the f1 transition.

int {rif[q1*:{Alice}]} res; 
int {rif[q1*:{Alice,Bob},q2:{Alice},f1:q1->q2,f2:q2->q1]} x;
int {rif[q1*:{Alice,Bob},q2:{Alice,Bob},f1:q1->q2]} y;

if (reclassify(x==y,f1)){
	res = 1;
}

3. Consecutive reclassifications: The final value of res depends on consecutively applying reclassifiers f3, f1, f2 to x. Here, both c-automata and i-automata are explicitly specified.

int {rif[q1*:{},q2:{Alice},q3:{Alice,Bob},f1:q1->q2,f2:q2->q3];
     rifi[q1*:{Alice,Bob},q2:{Alice},f1:q1->q2]} res; 
int {rif[q1*:{},q2:{Alice},q3:{Bob,Alice},f1:q1->q2,f2:q2->q3];
     rifi[q1*:{Alice,Bob},q2:{Alice},f1:q1->q2]} x;
int {rif[q1*:{Alice},f2:q1->q2,q2:{Bob, Alice}];
     rifi[q1*:{Alice}]} y;

x = reclassify(res,f3);
y = reclassify(x+4,f1);
res = reclassify(y,f2);

4. Method call: Method work calls method help inside an annotated expression. This snippet is type correct, because (i) the c-automaton of the return type of help is more restrictive than the c-automaton of y, (ii) the c-automaton of res is more restrictive than the c-automata of help(x) after taking the f1 transition, and (iii) the c-automaton of y is more restrictive than the c-automaton of x.

public work {} (int {rif[q1*:{Alice,Bob}]} x) {

    int {rif[q1*:{Alice}]} res; 

    res = reclassify(help(x),f1);
}


int{rif[q1*:{Alice,Bob},q2:{Alice},f1:q1->q2]} help (int {rif[q1*:{Alice,Bob}]} y) {

    return y%2 + y%3 + y%4;
}

5. Parametric RIF labels in where-constraint: Class foo is defined parametrically to labels L1, L2, and L3. These parameters are instantiated once a foo object is constructed. Whenever the constructor foo is called (e.g. obj = new foo[{rif...;rifi...},{rif...;rifi...},{rif...;rifi...}](7,9); ), the instantiations of the parameters L1,L2,L3 should satisfy the where-constraint. Specifically, L1 should be more restrictive than L2 and L3, after they have taken the f1 transition. If this condition holds, then the constructor is type correct, because the RIF label of res is more restrictive than the RIF labels of x and y, after they have taken the f1 transition.

public class foo[label L1, label L2, label L3] {

   int{L1} res;
   int{L2} x;
   int{L3} y;

   public foo(int{L2} a, int{L3} b) where tr(L2,f1)<=L1, tr(L3,f1)<=L1 {
       x = a;
       y = b;
       res = reclassify(x+y,f1);
   }

}

6. Dynamic RIF labels in dynamic check: Method work creates two dynamic RIF labels, and then it passes these labels as arguments to method help. Method help executes the assignment only if the dynamic check succeeds.

int{*l2} help {rif[q0*:{_}];rifi[q1*:{}]} 
(label{rif[q0*:{_}];rifi[q1*:{}]} l1, label{rif[q0*:{_}];rifi[q1*:{}]} l2, int{*l1} x){

    int{*l2} y=-1;

    if ( new label tr(l1,f1) <= l2)  y = reclassify(x % 4,f1);
    return y;
}

public void work{rif[q0*:{_}];rifi[q1*:{}]}() {

    final label{rif[q0*:{_}];rifi[q1*:{}]} l1 = new label {rif[q1*:{Alice},q2:{_},f1:q1->q2];
                                                           rifi[q1*:{Alice},q2:{},f1:q1->q2]};
    final label{rif[q0*:{_}];rifi[q1*:{}]} l2 = new label {rif[q1*:{_}]; rifi[q1*:{}]};
    int{*l1} x = new Random();
    int{*l2} res;
   
    res = help(l1,l2,x);

}

Applications

Battleship: Implementation of the Battleship game in JRIF. The implementation involved adapting Jif's Battleship implementation into JRIF. The source code can be found here.

For comparison, the Battleship implementation in Jif can be found here.

Shared Calendar: This application allows users to create and share events in their calendars. The implementation involves all kinds of reclassifications for both confidentiality and integrity, leading to richer RIF automata (more than 3 states). The source code can be found here.

Software

The JRIF compiler can be found here. This package contains source code for the compiler, the above applications, and additional test cases. It also contains a detailed account of the changes introduced in Jif to implement JRIF. An earlier release (October 2015) of JRIF can be found here.

Publication

JRIF: Reactive Information Flow Control for Java
Technical Report, October 2015