Formal Methods in the Software Life Cycle: Languages, methods, and tools

[ main | background | applications | schedule | deliverables ]

Below some information and pointers about the languages, methods, and tools that you will use in the Java Card OOTI course. This should help you get started writing and analyzing your first smart card applets and host applications.

Implementation

Smart Card

Smart cards communicate with the outside world by receiving commands and answering them. The protocol is described in the ISO7816-4 standard.

Java Card is a "dialect" of Java for programming such smart cards. A brief introduction to Java Card is available at JavaWorld. Lots more information is available from Sun's Java Card site. In particular, you can download the Java Card Development Kit there. The kit includes the Java Card API which contains classes you can use in your applet. Applets are compiled using a normal Java compiler and transformed to CAP files using a converter included in the kit. The protocol to download CAP files onto a smart card is described in the Global Platform standard.

We will be using IBM JCOP smart cards which support Java Card 2.1.1. Applets can be loaded onto the card using the JCOP toolset software that comes with the cards.

Terminal

The terminal (or host application) is also written in Java. Obviously, you will need to install a recent version of the Java 2 SDK. Two extra APIs are needed: one to communicate with the reader and one to do cryptographic computations.

For communicating with the smart card reader the OpenCard Framework (OCF) will be used. OCF is a Java-based middleware API for programming smart card host applications.

Since the host application will need to do some cryptographic computations, you also need to install a cryptographic provider compatible with Sun's JCE. (The standard Java library does provide an API for cryptography, but the underlying engine lacks some of the important cryptographic primitives due to export restrictions.) The Bouncy Castle provider is recommended.

The smart card reader used in this course, the Towitoko ChipDrive micro, connects to a USB port. You will need to download drivers for your operating system from the Towitoko web site. The JCOP tools talk to the Chipdrive via PC/SC. The Chipdrive is supported by OCF through the PC/SC bridge. This can be specified in the opencard.properties file.

API Documentation and Jars

Jar files should be copied to the jre\lib\ext folder of the Java 2 SDK in use. The dll files should be copied to \Windows or Windows\System32.

Analysis

JML, which stands for Java Modeling Language, is a specification language tailored to Java. JML can be used to specify the detailed design of Java (Card) programs, and to record design decisions that have been taken, by annotating programs with for instance class invariants, preconditions, and postconditions, in the Design-By-Contract style.

We will be using two tools that support JML:

• The runtime assertion checker:

  JML assertions in a Java program can be compiled into runtime tests that are performed when the program is executing. This will signal any violations of of invariants, preconditions, and postconditions that occur at runtime.

  The runtime assertion checker can be downloaded from the JML sourceforge page. Runtime assertion checking actually involves two separate tools, a special compiler jmlc that produces special bytecode which include runtime checks (which replaces javac), and a program jmlrac to execute this bytecode (which replaces java).

• Extended static checking with ESC/Java:

  ESC/Java is a tool that automatically checks JML-annotated Java(Card) code, and warns about potential NullPointerExceptions and ArrayIndexOutOfBoundsExceptions ESC/Java will be used for the verification of the Java Card smart card applets.

  To use ESC/Java to check your Java Card source code, you will need JML specifications of the Java Card API.

  Documentation about ESC/Java (old?):

  • ESC/Java User's Manual
  • ESC/Java Quick reference guide
  • FAQ

Some pointers to literature about JML and JML-related tools:

• A webpage about an industrial tool using JML: the Java Applet Correctness Kit
• A paper about the runtime assertion checker for JML:

  A Runtime Assertion Checker for the Java Modeling Language (JML).
  Yoonsik Cheon and Gary T. Leavens. In Hamid R. Arabnia and Youngsong Mun (eds.), International Conference on Software Engineering Research and Practice (SERP '02), Las Vegas, Nevada, pages 322-328. CSREA Press, June 2002.

• An overview paper of the ESC/Java tool:

  C. Flanagan, K.R.M. Leino, M. Lillibridge, G. Nelson, J.B. Saxe, R. Stata. Extended static checking for Java.
  In the proceedings of Conference on Programming Language Design and Implementation (PLDI'2002), pages 234- 245, ACM, 2002. © ACM

• A white paper about JML tools:

  An overview of JML tools and applications. Lilian Burdy, Yoonsik Cheon, David Cok, Michael Ernst, Joe Kiniry, Gary T. Leavens, K. Rustan M. Leino, and Erik Poll. To appear at FMICS'03.

• A description of a case study using ESC/Java:

  Formal specification of Gemplus' electronic purse case study
  Nestor Cataño and Marieke Huisman. In the proceedings of Formal Methods Europe (FME 2002), Number 2391 of LNCS, pages 272-289. Springer-Verlag, 2002. © Springer-Verlag

• For people familiar with unit testing, a paper on combining JML with unit testing:

  A Simple and Practical Approach to Unit Testing: The JML and JUnit Way.
  Yoonsik Cheon and Gary T. Leavens. In Boris Magnusson (ed.), ECOOP 2002 -- Object-Oriented Programming, 16th European Conference, Malaga, Spain, June 2002, Proceedings. Volume 2374 of Lecture Notes in Computer Science, Springer-Verlag, 2002, pages 231-255. © Springer-Verlag

Lots more can be found via the JML webpage.

Example applications

Some small example smart card applications are available:

Chipknip terminal

A simple OCF terminal to get the current balance of your Chipknip card. (Chipknip is the Dutch national E-Purse.) Have a look at the Java file: ChipknipTerminal.java. This example demonstrates OCF terminal programming.

Table applet and terminal

This simple applet implements a multiplication table which supports two commands: one for initializing the table (can only be called once), and one for getting entries from an initialized table. The terminal can be used to first initialize and then use the applet. Have a look at the Java files: TableApplet.java and TableTerminal.java. Note that the terminal expects the applet to have been installed with AID 39010203040501. This example demonstrates Java Card and OCF programming. The applet is specified in JML.

Calculator applet and terminal

This simple applet implements a calculator which operates on signed shorts. Overflow is silent. The terminal sends a command for every key on the keypad a user presses, the applet responds by sending the number to put on the display (i.e. the terminal has no state at all). Have a look at the Java files: CalcApplet.java and CalcTerminal.java. Note that the terminal expects the applet to have been installed with AID 3B2963616C6301. This example demonstrates Java Card and OCF programming.

RSA crypto example

This simple example shows how to do RSA keypair generation, encryption and decryption in Java. Have a look at the Java files: RSAKeyGen.java, RSAEncrypt.java and RSADecrypt.java. (Update: Changed algorithm to use PKCS1 padding).

RSA crypto applet and terminal

The applet encrypts or decrypts blocks of data (length at most 128 bytes) using RSA keys which are generated off-card and uploaded to the card. Have a look at the Java files: CryptoApplet.java and CryptoTerminal.java. The key file-format expected by the terminal application is the same as in the crypto example above. Note that the terminal expects the applet to have been installed with AID 01020304050601. This applet demonstrates Java Card cryptography.