Interacting with Java

The `main` method

Jif provides two possible signatures for the main method of a class. The first is compatible with the signature for Java main methods, and accepts a single argument of an array of String, that is,

public static void main(String[] args) { ... }

The second signature takes two arguments, the first a principal, and the second an array of String:

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

The principal p is the principal representing the current user that invoked the main. The signature may optionally have the authority of the current user:

public static void main(principal p, String[] args) where caller(p)
{
    ...
}

A class may have at most one static method named main. Classes with label or principal parameters cannot have a main method, as there is no way to specify appropriate instantiations for the parameters when invoking the main method.

Interacting with Java classes

The Jif compiler provides a mechanism to allow Jif code to be compiled against and linked to existing Java classes. However, appropriate Jif signatures must be supplied for the Java classes. NOTE: the Jif compiler does not verify that the Java code conforms to these provided signatures.

Suppose that you have an existing Java class, called Foo, i.e. you have a file Foo.java, and a file Foo.class that was produced by compiling Foo.java. Furthermore, suppose you want to use the class Foo in some Jif code you are writing. You can do this by supplying a Jif signature for the class Foo; at compile time, your Jif code will be compiled against the signature you provide, but at runtime the original Foo.class will be loaded. The steps for doing this are as follows:

In a file Foo.jif write an appropriate Jif signature for the methods and fields in the class Foo. Take a look at $JIF/sig-src/java/lang/*.jif for some examples of this.
Note the use of the native flag to avoid the need to provide a body for the methods. Note also that there is a private static int field named __JIF_SIG_OF_JAVA_CLASS$20030619; this is a hack to let the Jif compiler to know that the class provides a Jif signature for an existing Java class.
Compile Foo.jif to produce the file Foo.class
Make sure that the Foo.class you created in step 2 is on the signature classpath. Do this either by dropping the class file into the $JIF/sig-classes directory, or by specifying the directory with the -addsigcp flag to the Jif compiler.
Compile your Jif code that uses the class Foo. The Jif compiler will use the signature you created in step 1 when compiling your Jif code.
To run your Jif compiled code, make sure that the original Foo.class is on the classpath, but that the Foo.class you created in step 2 is not. Thus, when running your Jif compiled code, the original Foo.class will be loaded by the classloader.

More explicitly, here is a suggested directory structure.

jif-src/
   Bar.jif // Jif code that uses the Java class Foo

java-src/
   Foo.java // Java source code
   Quux.java // More Java source code, not used by any Jif code

sig-src/
   Foo.jif // Jif signature for the Java source code

Now compile the Java code. (You'll need to create the directory java-classes first.)

$ javac -d java-classes -sourcepath java-src java-src/*.java

Now compile the Jif signatures of the Java code. (Create the directory sig-classes first.)

$ $JIF/bin/jifc -d sig-classes -sourcepath sig-src \
      sig-src/Foo.jif

Now compile the Jif code. (Create the directory jif-classes first.)

$ $JIF/bin/jifc -d jif-classes -sourcepath jif-src \ 
      -addsigcp sig-classes \ 
      -classpath "java-classes:$CLASSPATH" jif-src/Bar.jif

Note that the signature class is added to the signature classpath using -addsigcp sig-classes, and the Java classes are put on the classpath using -classpath "java-classes:$CLASSPATH".

To run code, make sure that the classpath contains both java-classes and jif-classes, but that it does not contain sig-classes:

$ $JIF/bin/jif -classpath "java-classes:jif-classes:$CLASSPATH" Bar

Two other indicator fields can also be used in the Jif signature file of a Java class:

__JIF_SAFE_CONSTRUCTORS$20050907
Adding a private static int field named __JIF_SAFE_CONSTRUCTORS$20050907 to a Jif signature file is an assertion that during the execution of the constructors of the Java class there is no possible way to access a final field of a subclass of the class (for example, by invoking an overridden method that accesses final fields, or by leaking a reference to the object being created to some class that may attempt to access a final field of the class). Accessing final fields before they are initialized may be leveraged to leak information; the Jif typing rules prevent any access to final fields before they are accessed.

The assertion that the Java constructors are "safe" means the Jif compiler can impose fewer restrictions in the constructor bodies of Jif subclasses of the Java class.
__JIF_PARAMS_RUNTIME_REPRESENTED$20051007
Adding a private static int field named ___JIF_PARAMS_RUNTIME_REPRESENTED$20051007 to a Jif signature file is an assertion that the Java class conforms to the Jif conventions for runtime representation of label and principal parameters. Suppose that we have some Java class C and the Jif signature for the class states that the class has n parameters: class C[Q₁ q₁, ..., Q_n q_n], where each Q_i is either label or principal, and q_i is the name of the ith parameter.
Then the Java class C must conform to the following conventions:
1. If C is not an interface, then a method public static boolean jif$Instanceof(Q₁ a1, ..., Q_n an, Object o) must be present in the class, where each Q_i is either jif.lang.Label or jif.lang.Principal as appropriate.
  The method must return true if and only if the object o is an instance of C[a1, ..., an], that is, the class C instantiated with the parameters a1, ..., an.
  The method may not throw any exceptions.
2. If C is not an interface, then a method public static C jif$cast$classname(Q₁ a1, ..., Q_n an, Object o) must be present in the class, where each Q_i is either jif.lang.Label or jif.lang.Principal as appropriate, and classname is the full classname of the Java class C, with periods (".") replaced by underscores ("_") (e.g., for the class C in the package foo.bar, classname would be foo_bar_C).
  The method must return o if and only if the object o is an instance of C[a1, ..., an], that is, the class C instantiated with the parameters a1, ..., an.
  Otherwise, the method must throw a ClassCastException.
3. For each static method m(...) declared in the Jif signature, the Java class must provide a static method m(Q₁ a1, ..., Q_n an, ...).
  Jif code that calls the static method m on class C[a1, ..., an] will be translated into the Java method call C.m(a1, ..., an, ...).
4. For each constructor C(...) declared in the Jif signature, the Java class must provide a constructor C(Q₁ a1, ..., Q_n an, ...).
  Jif code that constructs new C objects via a new expression (new C[a1, ..., an](...) will be translated into the Java code new C(a1, ..., an, ...).
  Note that if Jif classes are able to subclass the class C, then the Jif typing rules require that the Jif signature for C includes a default constructor (that is, a constructor with no arguments), and thus the Java code for the class C must provide a constructor C(Q₁ a1, ..., Q_n an)
5. If C is an interface, then a class named C_JIF_IMPL in the same package, with the same visibility must be provided. This class must contain two static methods: public static boolean jif$Instanceof(Q₁ a1, ..., Q_n an, Object o) and public static C jif$cast$classname(Q₁ a1, ..., Q_n an, Object o). These two methods provide implementations for instanceof tests and class casts, as described above in items 1 and 2.

Debugging Jif programs

Tracking down and correcting compilation errors in Jif code can be difficult. While there is not as yet a debugger specifically for the Jif language, the Jif compiler has a number of reporting options that will result in additional information being displayed.

Constraint explanations

The -explain or -e flag of the Jif compiler can be used to view more information about failed label checking. For example, consider the program, in which there is a potential implicit information flow from the high security argument h, whose label is the dynamic label lbl, to the low security local variable l:

class Implicit {
    void m(boolean{*lbl} h, label{} lbl) {
        if (lbl <= new label {Alice:}) {
            boolean{} l = false;
            if (h) {
                l = true;
            }
        }
    }
}

Trying to compile this program produces the following output:

$ $JIF/bin/jifc Implicit.jif
Implicit.jif:6: Label of right hand side not less restrictive than the label
    for local variable l
                l = true;
                ^

1 error.

More information can be gleaned by using the -explain flag:

$ $JIF/bin/jifc Implicit.jif -explain
Implicit.jif:6: Unsatisfiable constraint:    
     rhs.nv <= label of var l    
        {h; caller_pc; lbl} <= {caller_pc; _: _; _!: _}    
     in environment    
     [{this} <= {caller_pc}, {*lbl} <= {Alice: }]    
        
     Label Descriptions    
     ------------------    
     - rhs.nv = label of successful evaluation of right hand of assignment    
     - rhs.nv = {h; caller_pc; lbl}    
     - label of var l = {caller_pc; _: _; _!: _}    
     - h = polymorphic label of formal argument h of method m (bounded above
    by {*lbl})    
     - caller_pc = The pc at the call site of this method (bounded above by
    {*: })    
     - lbl = polymorphic label of formal argument lbl of method m (bounded
    above by {})    
     - this = label of the special variable "this"    
     - *lbl = dynamic label represented by the final access path lbl    
        
     More information is revealed by the successful evaluation of the right
    hand side of the assignment than is allowed to flow to the local variable
    l.
                l = true;
                ^

1 error.

The more detailed error message first shows what the symbolic unsatisfiable constraint is (rhs.nv <= label of var l), and then shows the same constraints with the actual labels substituted for the symbols ({h; caller_pc; lbl} <= {caller_pc; _: _; _!: _}). The label environment in which the constraint must be satisfied is also shown. Here, the environment indicates that the value held in the label variable lbl is bounded above by the label {Alice:}, and that the label of the receiver object ({this}) is bounded above by the label {caller_pc}. Brief descriptions of the labels that appear in the unsatisfiable constraint are also shown. Here, we see that rhs.nv represents the label of the information that may be acquired by knowing the value of the successful (normal) evaluation of the right hand side of the assignment; for this assignment, that label is {h; caller_pc; lbl}, where {h} and {lbl} are the labels of the formal arguments h and lbl, and {caller_pc} represents the pc of the call site, which is bounded above the method's begin-label, which in this case is the most restrictive label, {*: }.

Detailed reporting

Sometimes the additional information provided by the -explain option is not sufficient to determine why a Jif program fails to compile. There are two additional useful ways to gain more information about the label checking process: reporting the topics debug and solver. Specifying the command line option -report debug=n, where n is a non-negative integer, will display more information about labels. The higher the value for n, the more information is displayed. For example:

$ $JIF/bin/jifc Implicit.jif -report debug=1 -explain
Implicit.jif:6: Unsatisfiable constraint:    
     rhs.nv <= label of var l    
        {<arg h {<dynamic lbl>}>; <arg caller_pc {*: ; _!: _}>; <arg lbl {_: _;
    _!: _}>} <= {<arg caller_pc {*: ; _!: _}>; _: _; _!: _}    
     in environment    
     [{<this (of Implicit)>} <= {<arg caller_pc {*: ; _!: _}>}, {<dynamic
    lbl>} <= {<pr-external Alice>: ; _!: _}]    
        
     Label Descriptions    
     ------------------    
     - rhs.nv = label of successful evaluation of right hand of assignment    
     - rhs.nv = {<arg h {<dynamic lbl>}>; <arg caller_pc {*: ; _!: _}>; <arg
    lbl {_: _; _!: _}>}    
     - label of var l = {<arg caller_pc {*: ; _!: _}>; _: _; _!: _}    
     - <arg h {<dynamic lbl>}> = polymorphic label of formal argument h of
    method m (bounded above by {<dynamic lbl>})    
     - <arg caller_pc {*: ; _!: _}> = The pc at the call site of this method
    (bounded above by {*: ; _!: _})    
     - <arg lbl {_: _; _!: _}> = polymorphic label of formal argument lbl of
    method m (bounded above by {_: _; _!: _})    
     - <this (of Implicit)> = label of the special variable "this"    
     - <dynamic lbl> = dynamic label represented by the final access path lbl    
        
     More information is revealed by the successful evaluation of the right
    hand side of the assignment than is allowed to flow to the local variable
    l.
                l = true;
                ^

1 error.

In the environment, we see that the label of the actual argument for h is displayed as <arg h {<dynamic lbl>}>. That is, we see that the label is the argument label for the argument h, and that this arg-label is bounded above by the label <dynamic lbl>, that is by the dynamic label lbl.

The arg-label for h would normally be displayed simply as h, and the dynamic label lbl would normal be displayed as *lbl. But with the debug topic reporting at level 1, we see more detail about the labels, which can be helpful to determine what reasoning the compiler is performing. Setting the report level higher reveals even more information.

Thus, reporting the debug topic provides more information about the labels and their meaning, but a less readable display.

Specifying the command line option -report solver=n, for a nonnegative n, will display more information about the constraint solver, which attempts to solve the system of constraints generated by label checking. The higher the value for n, the more information is displayed.

When the constraint solver is unable to solve a system of constraints, it attempts to find the most appropriate constraint to "blame": this is the constraint that is displayed in the error message. However, sometimes this constraint is not the real culprit, and one or more other constraints are really preventing successful compilation. Enabling reporting for the solver allows the user to determine which constraint(s) are problematic, when the error message does not appear to be helpful.

Jif runtime interface

To interact with the external environment, Jif provides a runtime interface to allow Jif code to read and write files, and access stdin, stdout and stderr, and also to obtain a principal representing the current user. The runtime interface is jif.runtime.Runtime.

Although the runtime code is itself is written in Java (see $JIF/rt-src/jif/runtime/Runtime.java), a Jif signature is provided to allow calls to this interface can be checked statically (see $JIF/sig-src/jif/runtime/Runtime.jif).