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 and/or untrusted information from being used improperly.
This document describes Jif 3.3.1, and is the most current documentation for the Jif language and compiler. The current release of 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 can be found in Andrew Myers' thesis, linked to from the Jif web site. However, the language has developed since that time, and some features in this version of Jif are not documented in the thesis.
Jif extends Java by adding
labels that express restrictions on how information may be used.
For example, the following variable declaration declares not only that
the variable x is an int, but also that the
information in x is governed by a security policy:
int {Alice→Bob} x;
In this case, the security policy says that the information in x
is controlled by the principal Alice, and that Alice permits this information
to be seen by the principal Bob.
Using label annotations like this one, the Jif compiler analyses how information flows within programs and determines whether security policies for the confidentiality or integrity of information are enforced by the program. For example, consider the following variable declaration and assignments:
int {Alice→Bob, Chuck} y;
x = y; // OK: policy on x is stronger
y = x; // BAD: policy on y is not as strong as x
The variable y is declared to be an int,
and Alice permits the information in y to be seen by both Bob and Chuck.
The first assignment is secure because it does not make the information in
y visible to any additional principals. The second assignment is
insecure because now Chuck can see the information that was in x,
and the policy on x forbids this (unless Alice or Bob happen
to trust Chuck, as seen later). The Jif compiler makes these determinations
at compile time, 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 program can then be executed with a standard Java virtual machine. Although enforcement is mostly done at compile time, Jif does also allow some enforcement to take place at run time. Therefore, Jif programs in general require the Jif run-time library.
This manual describes the latest version of Jif, Jif 3.3.1. With the introduction of version 3, the language was extended with some important new features. In particular, Jif now supports integrity policies and can use them to check the robustness of downgrading performed by the program. Jif now also provides a richer set of operators for constructing and manipulating security labels, including general meet and join operators. Jif also supports automatic inference of class parameters, including inference of both labels and principals.