Specification of the Javacard API in JML

Abstract

This paper reports on an effort to increase the reliabilityof JavaCard-basedsmart cards by means of formal specification and verification ofJavaCard source code.As a first step, lightweight formal interfacespecifications,written in the specification language JML, have beendeveloped for all the classes in the JavaCard API (version 2.1).They make many of the implicit assumptionsunderlying the currentimplementation explicit, and thusfacilitate the use of this API andincrease the reliability of the code that is based on it. Furthermore,the formal specifications are amenable to tool support, for verificationpurposes.