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)

    • 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
    Last modified: Wed Jun 18 09:01:34 EDT 2008