Applications to JavaCard

JavaCard^TM is a simplified version of Java, especially designed for use on smart cards (with a processor running a virtual machine). These cards will be used for all kinds of transactions and for access to services and networks. JavaCard is an ideal target for the application of formal methods because:

• The language is relatively simple; for example, it does not include threads, floating point numbers, or multi-dimensional arrays.
• The JavaCard API is relatively small, currently consisting of about 45 classes.
• JavaCard programs (called applets) for use on smart cards are small, due to the restrictions imposed by the processor on these cards.
• JavaCard programs will be used in great numbers in often critical applications.

• formal interface specifications of the JavaCard API, written in the specification language JML.
  A first release of these API specifications is available on-line.
  There are several papers about these specifications: [PollBJ:CARDIS00] [PollBJ:CN01] [MeijerPoll:eSmart01].


• verifying that the current JavaCard API classes satisfy these interface specifications.
  See [BergJP:CJW2000] for first attempts in this direction.
• annotating and verifying individual JavaCard applets, based on the formal interface specifications of the JavaCard API.
  A case study used for this is a Purse applet from Gemplus. The first results of annotating and verifying a part of this case study with the LOOP tool and PVS are reported in [BreunesseBJ02].

• CardSpec: JavaCard Specification and Verification with JML. This involves a three-year postdoc position funded by NWO, the national science foundation in The Netherlands. The position is held by Engelbert Hubbers.
• VerifiCard: Tool-assisted Specification and Verification of JavaCard Programs. This is a European IST project for which the LOOP group is coordinator. [JacobsEtAl:NVTI01]. Employed on this project are Martijn Oostijk and Cees-Bart Breunesse.

For more information, contact Erik Poll.