The model checking of JavaCard applets will be illustrated with an example; a modification of the purse example from SUN's JavaCard Development Kit (version 2.1.2). This example is a prototypical purse and loyalty smartcard application, which comprises around 1430 lines of JavaCard code.
To understand the example it is helpful to recall the
execution characteristics of JavaCard applets (language version 2.1.1).
An interaction with the card (after installation of an applet,
and its selection) is initiated through calling its process
method. Inter-applet communications, crossing package borders,
are controlled by the JavaCard firewall mechanism and
take place through special interface objects.
The methods of such interface objects
are indicated in Figure 1.
The purse applet keeps a balance that is updated upon requests from the environment. Purse transactions, whether successful or not, are logged to a transaction log. The operations of updating the balance, logging the new transaction and updating the transaction number are made atomic through use of the transaction facility of JavaCard.
Upon completion of a new purse transaction the purse applet
notifies subsidiary loyalty applets via the interface
method grantPoints.
These are applets that should
be notified of the balance update so that they,
for example, can award loyalty points.
A concrete example is a bank smartcard with an embedded
loyalty applet for a car rental company that awards bonus
points for every car rented using the bank card.
In addition to these functionalities there are methods,
accessible through the process method of the applet,
for modifying most of the parameters of the purse applet,
including adding knowledge about new loyalty applets
that should be notified when card transactions occur.
The loyalty applets
of the Development Kit purse application do
not attempt to communicate with other applets.
We have extended the example loyalty applet with
two new functionalities:
(i) A loyalty applet can have agreements with other loyalty
applets to share bonus points; to achieve this we
introduce direct loyalty applet to loyalty applet communication
using the interface method grantLoyaltyPoints.
(ii) loyalty applets can have an agreement with the purse
to transfer, according to same fixed rate, part of the
bonus points back to the purse.
This is achieved through calling the interface
method bonusPointsToPurse of the purse.
The modified purse and loyalties example is a rewarding example to study using our model checking approach as many key applet correctness properties can be phrased as properties of inter-applet communications.
