Information Flow in Java with JIF

While DLM forms the foundation of Jif, it is a technology model in itself. Jif takes the concepts and the language rules form DLM and expands them into a full language extension to Java. This section of the report explains some of the features of the language extension that will be covered in the example.

int{Alice->Bob; Alice<-Frank} x = 0;

declassify(x, {Alice->Bob; Alice<-Frank} to 
	{Alice->Bob, Frank; Alice<-Frank});
	
endorse(x, {Alice->Bob, Frank; Alice<-Frank} to 
	{Alice->Bob, Frank; Alice<-Frank, Bob});

In the first article it was detailed how policies restrict information flow, however, this does not make for a usable programming language. Jif allows the security of information to be downgraded by explicitly specifying a new policy label for an expression. The method declassify(e, L1 to L2) downgrades the security of the read set by replacing label L1 with L2 for expression e. The writer set of L2 must be at least as restrictive as L1. To downgrade the writer set, the programmer must instead use endorse(e, L1 to L2). This time, the writer set is relaxed to the policies of L2,however, the reader set must remain at least as restrictive as L1. This is illustrated in Example 1, “Downgrading Policies” though it is worth noting that Jif 3.1.1 is inconsistent with this notation and instead only uses the expression and the new label in declassification and endorsements. By forcing these downgrades to be performed independently of one another there is never the chance that the programmer can accidentally relax the policy for the wrong reader or writer set.

l = false;
if (h) {
    l = true;
}

So far the report has only discussed explicit assignments information flow, however, there are many ways that information can pass through an application without being explicitly transferred. Example 2, “Implicit Flow manjif” shows a simple program taken from the Jif reference manual [manjif] whereby private information stored in variable h could be propagated to public variable l. To combat this, Jif records the program counter during compilation to check that any reads or assignments are to variables with policies at least as restrictive as those associated with the branch variable, in this case h. If l were public, it would be less restrictive than the branch condition h and the program would not compile.

class Train authority(driver) {

	void start() where authority(driver) {...}
	
	void stop() where caller(driver, emergencyBrake){...}
	
	void {driver<-* meet waitstaff<-*}doTeaService(){...}
}

To explicitly state that an application runs as a particular principal, the class can be marked with the authority of that principle. Principals can also be specified in the method signature to limit the principals that can call a particular method. The caller condition only allows principals listed in parenthesis to execute the method. More flexibly, a policy label can be specified before the method name as a precondition to running the method. These are illustrated in Example 3, “Class Authority”.

While Jif provides a comprehensive way to improve the security of information in Java programs, there are limitations to the solution. Several Java programming features are not supported by the language including nested classes, initialiser blocks and threads [manjif]. Since it is possible to use these features as covert channels for data propagation they cannot be ignored by Jif and due to their complex nature are difficult to provide solutions for.

By their very nature, data policies must be verbose to ensure that they correctly define the restrictions on data, however, from the view of the programmer they require a significant amount of typing and repetition to perform the simplest of tasks.

System.out.println()

Most notably, Jif is not part of the Java programming language and as such, Jif programs must be pre-compiled to Java before they can be compiled and run. This is taken care of in one step by the Jif compiler, however, it means that Jif classes are notably distinct from regular Java classes. Jif can make use of regular Java classes and be inter-operable but it isn't seamless.

import jif.principals.*;

public class Example1
{
    public static void main{}(principal{} p, String[]{} args) {

	// Construct the principals
	final principal Alice = new Alice();
	final principal Bob = new Bob();

	// Set up private data, notice the fields only
	// have owners
	String{Alice:} aliceCarReg = "XYZ";
	String{Bob:} bobCarReg = "ABC";
	
	String{} publicReg = "";
	
	// attempt to set the public field with alice's
	// private car registration
	publicReg = aliceCarReg;
    }
}

String{Alice<-_} aliceCarReg = "XYZ";

String{Alice:} aliceCarReg = "XYZ";
String{Bob:} bobCarReg = "ABC";

String{} publicReg = "";

// attempt to set the public field with alice's
// private car registration
aliceCarReg = declassify(aliceCarReg, {Alice:; Alice<-_});
publicReg = aliceCarReg;