Blame-Enabled Jif

Blame-Enabled Jif is a modification of the Jif compiler to provide traces of security errors encountered during compilation. At present, label checking errors in security-typed languages are not well understood. Jif and Flowcaml (the two most mature implementations of a security-typed language compiler) currently provide limited facilities for explaining why an individual constraint may fail. However, as information-flow errors may be caused by any runtime code path, a local approach to error explanation often fails to explain the real cause of security errors.

Error Explanations

Even simple errors can be impenetrable in Jif [1]. For example:

int{Alice:} aliceData;

public void modifyData(int{Alice:} newData) {
   aliceData = newData;
}

When the above code is compiled, the most recent version of Jif (3.1.1) gives the following error message:

BlameTest.jif:21: Label of right hand side not less restrictive than the label
    for field aliceData
        aliceData = newData;
        ^-------^

--- ERROR ---
constraint: {#var_newData; #pc3; #var_{this}} <= {Alice: } in environment [{this} <= {caller_pc}]
position: BlameTest.jif:21,1-10
BlameTest.jif:21: constraint generated by
        aliceData = newData;
        ^-------^

environment: [{this} <= {caller_pc}]

failed: {#var_newData; #pc3; #var_{this}} <= {Alice: }
why: {#var_{this}} == {this} in environment [{this} <= {caller_pc}]@BlameTest.jif:1,7-22
BlameTest.jif:1: constraint generated by
public class BlameTest {
       ^-------------^

unsatisfiable: {this} <= {Alice: }
-------------

The error trace from Blame-Enabled Jif indicates:

A constraint failed at the assignment; some variables were forced to be less than {Alice:}.

That constraint failed because the variable #var_{this} was set equal to the this label.

The equation {this} <= {Alice:} was unsatisfiable.

With knowledge of the Jif compiler, we know that {this} in a method is always constrained to be less than the caller_pc of a method. By setting the begin label on modifyData to {Alice:}, we can force this to be less than {Alice:} and so resolve this error.

While resolving this error is a little esoteric, the important feature of Blame-Enabled Jif is that it does not just notify the user that a constraint solving error has occured: it examines the failed constraint, determines which of the variables in the failed constraint contributed to an error, and thus provides a trace of what caused the error.

Our key modifications to the Jif compiler are:

A blame engine for explaining errors in the constraint solver that occur during variable assignment.

Introducing auxiliary variables to provide traces for errors that would otherwise fail statically, i.e. errors that would otherwise have no trace.

While introducing more variables increases the runtime of the Jif constraint solver, this does not greatly impact the performance of the Jif solver, as it usually behaves in a linear-time. We believe that this is an acceptable trade-off.

More details about the theoretical background of the error explanations provided by Blame-Enabled Jif can be found in the technical report describing this work [2]. This work will be presented at SIGSOFT/FSE 2008.

Using Blame-Enabled Jif