JLift is a static analysis tool for finding information-flow errors
in Java programs. It is an extension of the Jif compiler to operate on
Java programs. It is similar to CQual/JQual, except that
it also detects implicit flows arising from conditionals and
exceptions. It has been used to successfully catalogue
information-flow errors in a number of server programs.
JLift is in a state of active development. Dave King is the maintainer of JLift.
JLift 0.0.3 (Java 5 JRE: download.)
0.0.3 (June 18, 2008): a number of various changes -- more soundness for type casts, better explanations for runtime exceptions, different declassification constraint scheme.
0.0.2.1 (March 18, 2008): added switch -noimplicit to disable implicit flows
0.0.2 (March 7th, 2008): fixed a number of bugs with information-flow constraint output
Java Card Wallet (download)
Java Card Purse (download)
Mental Poker (download)
JES Server (download)
JES Server (66 errors, catalogued here)
Mental Poker: (8 errors, corresponding to basic cryptographical operations, catalogued here)
TinySQL (29 manual + 62 automatic errors, catalogued here)
Use bin/jliftc script on source file that you want to
analyze. These files should have .jif, .java, or
For some good example programs, the tests/testharness
directory has a number of tests.
Switches that can be helpful:
-report summary=1 (displays progress of summary constraint generation)
-report summary=2 (more detailed description of summary constraint generation)
-report callgraph=1 (outputs callgraph in text)
-report callgraph=2 (outputs callgraph in DOT)
-noex (turn off exception flows)
Automatic Declassification Suggestion Engine: (requires Berkely Solver + minisat+)
-declcons (output constraints for Berkeley IFC Solver). Files will be big.
-declsources (declassify sources; not enabled by default)
-multirhs (output non-definite constraints for encoding)
The Lemon Mincut tool
generates suggestions for placing mediators
(minimum set) using the constraint XML file generated by JLift.
We used the Lemon
graph libraries developed for scientific
computing to calculate the minimum cut of a graph, but implemented
our own dominator computation.
To use the mincut tool, run the JLift tool on the program to
obtain the constaint XML file. Then copy that to the Debug/
directory in the lemon tool, and run
./lemon_mincut -xml <XML file>
Labels should only be placed on fields and method arguments; labels on
local variables are handled according to the black magic of the
original Jif compiler and are automatically raised to the level of the
The analysis needs signatures to handle external libraries
should be used for this.
All .jif source code retains its original license.