Jakarta: a toolset for reasoning about JavaCard

Gilles Barthe

Projet Lemme -- INRIA Sophia-Antipolis

Abstract:
JavaCard is a dialect of Java that enables Java technology to run on new generation smart cards and other devices with limited memory. As JavaCard is increasingly popular and is in pass of becoming a standard for smartcards (20,000,000 cards sold in 2000 vs. an estimated 100,000,000 cards that will be sold in 2001), there has been a strong interest, both from academics and industrials, to reason formally about the JavaCard platform.

This talk reports on preliminary results with Jakarta, a toolset for reasoning about the JavaCard platform. The main ingredients of the toolset are:

the Jakarta Specification Language (JSL), a front-end for producing highly readable executable specifications;
the Jakarta Transformation Kit (JTK), a program to manipulate and transform JSL specifications;
the Jakarta Prover Interface (JPI), a compiler that translates JSL specifications into proof assistants;
the Jakarta Automation Kit (JAK), a toolset to support reasoning about executable specifications within proof assistants.

We also report on using Jakarta to specify and reason about the JavaCard platform, and on the benefits of this approach over using a proof assistant directly, as done in our previous work.

Back to schedule.

Marieke Huisman

Last modified: Thu Mar 1 2001