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.

**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

**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

{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

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

**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); }

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

Technical Report, October 2015