Address
Project Everest
INRIA Sophia-Antipolis
2004, Route des Lucioles
BP 93
06902 Sophia-Antipolis

Software

JACK: Java Applet Correctness Kit

JACK is a toolset for applet validation that has been developed in collaboration between Gemalto and INRIA. Its main design goals are:

a high correctness assurance;
an accessible user interface;
prover independence; and
a high degree of automation.

JACK takes as input Java programs, annotated with JML specifications. It generates appropriate proof obligations, which can be used as input for different theorem provers (automatic or interactive).

For more information, see the JACK webpage.

Auditing Assistant

We developed a secure auditing assistant that generates JML annotations from high-level security properties. The assistant has been successfully applied to industrial case studies. Its implementation has been integrated into JACK.