Card language is a dialect of Java, designed for programming smart
cards. The core language is a subset of Java. This has been extended
with various libraries (APIs in Java terminology) with specific functionality
for smart cards. It is one of a family of dialects of Java, targetted at
specific application areas. Other such languages are Embedded
Java and Personal
By "Java Card technology" is meant the core language definition, the
APIs, and the virtual machine.
Java Card Language
Java Card is based on Java, so is an object-oriented programming language,
with features such as exceptions, packages, and visibility modifiers.
However, given the memory and processing constraints on current generation
smart cards, it is not possible to use the more `expensive' features of
Java. The most significant is the removal of threads. Also, `big' datatypes
such as floats and double integers are not present. Other features dropped
include garbage collection and dynamic class loading.
Application Programming Interfaces
There are several core APIs furnishing the basics of the Java Card environment
(objects, exceptions, etc.). Some interesting features for smart cards
applets : One of the things that makes smart cards `smart', is the
potential to download code and install independent applications on the
same card. Java Card has a notion of applet (different from Java
applets), with methods for installation, selection and so on. The runtime
environment handles firewalls and limited object sharing.
APDUs : The card and card reader communicate by sending packets of data
known as APDUs.
object-oriented file system : This is a considerable advance over previous
approaches to programming smart cards, which were/are at the assembler
In addition, APIs have been developed with functionality for specific
application areas, such as financial services (EMV) and telecommunications
Java Card Virtual Machine
Applets are downloaded in the form of bytecode which is then execute on
a virtual machine. The JCVM handles a subset of the instructions in Java
bytecode. However, there are specialised instructions for the small datatypes.
The bytecode is organised in a particular optimised format, called a CAP
file. The runtime environment takes care of various security aspects such
as object sharing and transactional processing.
We can describe the Java Card architecture at several levels:
In general, therefore, current research into Java and Java Card is taking
place at several levels.
The core APIs (the `framework')
`Add-on' industry-specific APIs
In our project, "Verification
of Java Card programs", I have looked, so far, at the semantics of
bytecode and the JCVM, and the correctness and formal development of a
Semantics of bytecode
Semantics of Java Card language
Correctness of compilers and optimisers
Semantics of `higher-level' semantic features (object sharing, atomicity)
Axiomatising interesting APIs and modelling the conformance to `vertical'
specifications (eg. EMV, GSM)
Formal development for applets with respect to specific APIs
Some Java Card and Java links