JRIF: Reactive Information Flow Control for Java
Elisavet Kozyri, Owen Arden, Andrew C. Myers, Fred B. Schneider

Foundations of Security, Protocols, and Equational Reasoning
April 2019


A reactive information flow (RIF) automaton for a value v specifies (i) restrictions on uses for v and (ii) the RIF automaton for any value that might be derived from v. RIF automata thus specify how transforming a value alters restrictions for the result. As labels, RIF automata are both expressive and intuitive vehicles for describing allowed information flows. JRIF is a dialect of Java that uses RIF automata for specifying information flow control policies. The implementation of JRIF involved replacing the information flow type system of the Jif language by a RIF-based type system. JRIF demonstrates (i) the practicality and utility of RIF automata, and (ii) the ease with which an existing information flow control system can be modified to support the expressive power of RIF automata.