Specification of the JavaCard API in JML

This paper reports on an effort to increase the reliability of JavaCard-based smart cards by means of formal specification and verification of JavaCard source code. As a first step, formal interface specifications, written in the specification language JML, have been developed for all the classes that make up the JavaCard API. These specifications are "lightweight" in the sense that they are incomplete and specify only some aspects of the API, but they already provide a useful addition to the existing informal API specifications. Moreover, the fact that these specification are written in a formal language makes them amenable to tool support, for verification purposes. As an illustration, the JML specifications of the APDU (Application Protocol Data Unit) class in the JavaCard API are discussed in detail. Key words: smart card, JavaCard, formal specification

• Type: Conference
• Year: 2000
• Where: CARDIS
• Authors: Erik Poll, Joachim van den Berg, Bart Jacobs
• Keywords: CARDIS 2000, Formal Specification, Hardware, JavaCard API, Specifications