Jif Change Log

2008-04-15 Jif 3.2.0

Refactoring for cleaner support of extensions, including Jifclipse.
Minor bug fixes and style changes.
Allow reader policies o→⊥ and writer policies o←⊥ to be dropped from labels. (Principal ⊥ is the bottom principal, and thus o→⊥ and o←⊥ do not restrict the the sets of readers and writers.)

Based on Polyglot 2.3.0
Checked endorse construct
- A useful form of the endorse statement for the common case of validating an untrusted value. See the Jif manual for more details.
Constant arrays
- Arrays can be declared constant, meaning their contents will not change after initialization. This allows more permissive label checking. See the Jif manual for more details.
Dataflow analysis for array bounds
- Analysis is able to determine if some array access and new array expressions will not throw runtime exceptions.
Numerous bug fixes

See the Jif manual for a full explanation.
Label checking rules to enforce robustness against all attackers can be turned on using the -robust command line option.

UTF-8 encoded source files accepted
A reader policy p:q can also be written p->q or p→q (the arrow is Unicode character 8594)
A writer policy p!:q can also be written p<-q or p←q (the arrow is Unicode character 8592)
Downgrades now explicitly mention the from and to labels e.g., declassify(h, {Alice:} to {Alice:Bob})

A new binary operator equiv added. For principals, p equiv q is equivalent to p actsfor q and q actsfor p. For labels, L1 equiv L2 is equivalent to L1 <= L2 and L2 <= L1.
Principal and label comparisons can be used as arbitrary boolean expressions. e.g., boolean b = (p actsfor q); if a principal or label test occurs as a conjunct of an if-statement, then the label environment used to label check the consequent will include this fact.

Jif manual significantly expanded, including section on the label checking rules in Jif.
Jif library code now has HashMap and HashSet implementations.
Numerous bug fixes.

Numerous bug fixes.
Label less-than-or-equal constraints for methods.
Map implementation in jif.util library.
Simple runtime class analysis removes the need to statically handle some spurious ClassCastExceptions.
jif.lang.IDComparable interface now with additional method equals(label lbl, IDComparable[lbl] o).

Based on the Polyglot 1.2.0 architecture.
Improved error messages.
New command line option to the Jif compiler: -explain (or -e) makes the compiler provide more information about why label checking failed.
The signature for the public static void main method for Jif programs can now optionally include a dynamic principal, who is the current user. See the file examples/README in the distribution for more information.
Misc bug fixes, including:
- The label this cannot be used in a static context.
- Incorrect labels missing colons (e.g., {Alice}) are detected.
- Parameterized classes cannot be subclasses of java.lang.Throwable.
- Final local variables require an initializer.
- Implementation of acts for corrected.