JLift

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.

Files

  • JLift 0.0.3 (Java 5 JRE: download.)
  • Recent Changes

  • 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
  • Example Programs

  • Java Card Wallet (download)
  • Java Card Purse (download)
  • Mental Poker (download)
  • JES Server (download)
  • tinySQL (download)
  • Error Traces

  • 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)
  • Usage

    Use bin/jliftc script on source file that you want to analyze. These files should have .jif, .java, or .jl extensions.

    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)
  • Lemon Mincut

    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>

    Warnings

  • 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 program counter.

  • The analysis needs signatures to handle external libraries correctly. siggen should be used for this.

    Note

    All .jif source code retains its original license.

    Dave King