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