Copenhagen Programming Language Seminar


Java Program Verification for Smart Cards

Bart Jacobs
Nijmegen University, Netherlands

Thursday, April 3rd, 15:15-16:00
DIKU, Universitetsparken 1, room N037


The latest generation of smart cards i developed for multiple applications. There is a small operating system on-card together with a virtual machine, an API and some cryptographic machinery.

These cards are capable of executing small JavaCard programs, called applets, for instance for banking or communication (GSM). JavaCard is a stripped-down version of Java, designed to run in an environment with limited resources.

Since these cards are especially used for security sensitive application, correctness is an important issue. In this talk it will be argued that such smart cards form an ideal target (and challenge) for formal methods, because:
- the programs that run on these cards are very small, and within the reach of modern verification tools;
- these cards are distributed in large numbers, so that flaws can have a huge impact;
- the smart card industry is driven by certification demands in which formal medthods are important

This talk will focus on the work done at Nijmegen on applet specification, with the spcification language JML, for Java Modeling Language (see http://www.cs.iastate,edu/~leavens/JML.html), and verification with the prooftool PVS (see http://www.pvs.csl.sri.com ). It will show several sample verifications and explain the program logics that are used.

Scientific host: Carsten Butz. Administrative host: Camilla Jensen. All are welcome.
The Copenhagen Programming Language Seminar (COPLAS) is a collaboration between DIKU, IT-C and KVL.
To receive information about COPLAS talks by email, send a message to prog-lang-request@mail.it-c.dk with the word 'subscribe' as subject or in the body.

For more information about COPLAS, see http://www.coplas.org