Welcome FAQ Download Papers Links

What is Kacheck/J?

Kacheck/J is an encapsulation checker for Java. It infers which types are confined according to the definition given in Encapsulating Objects with Confined Types. Objects of confined type do not escape their enclosing package.

Kacheck/J was developed using the XTC framework.

News

Kacheck/J v5.0 released
This version adds support for analyzing Java 5.0 bytecode. It also adds a new option to verify @confined annotations that are possible in Java 5.0. It is also possible to add @confined annotations automatically to class files using the new dump option (useful if other tools, static analyses or the VM can benefit from such annotations). The code itself was cleaned up significantly and now requires Java 5.0 to compile.
Kacheck/J v3.1 released
This version is based entirely on the XTC branch and features performance improvements and most importantly, cleaner code.
This version uses Jamit v3.0.
Kacheck/J v3.0 released
This version integrates the new Jamit 2 with dead code elimination and contains various improvements with respect to precision of the analysis.

Usage

If called only with the path to the classes of the application, Kacheck/J will print the names of classes that are annoated to be @Confined but that are in violation of the rules for confinement. Kacheck/J will also list all of the classes that are confined but not annotated as such.
The option -dump=DIR can be used to output rewritten class files that contain the @Confined annotation for confined classes (classes that are not changed will not be written to DIR).
The option -verbose can be used to obtain statistics about the number of @Confined clases. The option -listall will cause Kacheck/J to print the names of all confined classes (whether they are annotated as such or not).
You should copy the code of @Confined into your source project if you want to use @Confined annotations. While Kacheck/J is released under the GPL, the @Confined annotation class is in the public domain (in other words, you can integrate it into any application under any license).

Contact

Kacheck/J was written by Christian Grothoff and Jan Vitek.


Christian Grothoff