Action de recherche coopérative INRIA
Java Card : sémantique, optimisations et sécurité
The INRIA research action Java Card has as its aim to coordinate research
carried out at INRIA concerning formal aspects of Java and Java Card, a
Java dialect for programming smart cards. This includes research on the
formal semantics of these languages, program analysis for program optimization
and methods for verifying safety and security related properties.
Card language (latest version: 2.1) is a subset of Java. Certain data
types such as long integers, floating-point values and characters have
been removed; there are no threads and classes are not loaded dynamically.
The language has been extended with facilities for programming atomic transactions
and for specifying applet isolation and sharing through interfaces (only
in Java Card 2.1). The Java card language is being designed in collaboration
with the Java Card Forum.
A French summary of the project's
Project leader : D.
Post-doctoral researchers employed on the project : Ewen
Denney (Lande) and Shen-Wei
The project has held the following meetings
Rocquencourt, March 1998
Sophia, July 1998
Rocquencourt, January 1999
St. Malo July 1999
Publications related to the project
I. Attali et al.: A Formal Executable Semantics for Java
Proceedings of Formal Underpinnings of Java - An OOPSLA'98 Workshop,
Vancouver, October 1998.
X. Leroy and F. Rouaix: Security properties of typed applets POPL '98.
A. Fau: Analyse et éléments de formalisation de la
sécurité Java, Mémoire de DEA, Juin 1999.
T. Jensen, D. Le Métayer, T. Thorn:
Security and Dynamic Class Loading in Java: A Formalisation
In Proceedings of the 1998 IEEE International Conference on
Computer Languages, pp. 4-15,
T. Jensen, D. Le Métayer, T. Thorn: Verification of control flow based security policies
nº 1210, Appears in the porceedings of 20th IEEE Security
and Privacy Symposium, Oakland, CA, 1999
The project was presented by a poster
at the European Multimedia, Microprocessor Systems and Electronic Commerce
(EMMSEC'98) conference organised by the European Commision.
An article describing
the project appeared in the Inria newsletter InEdit.
newsletter no. 36 on Programming Language technology contains two articles
from participants in the project describing their activities around Java
and Java Card.
- Transparencies from a talk
Java Card : a language for programming smart cards held at the
Danish Technical University.
Programming smart cards in Java
One of the major interests in the Java language is the possibility of downloading
code and executing it in a transparent manner. This practice raises serious
problems regarding the security of information (confidentiality and integrity
in particular). Java addresses these concerns, and others, through a greater
level of safety features in the language (typing, verification of imported
code, simple inheritance, etc.) and a security manager which enforces security
policies. The language itself is considered safe but this assertion is
still a topic of debate, all the more so since there is no formally specified
official definition of the semantics of the language. The need for a formal
definition clearly arises from the contradictory declarations of type-safeness
and the fact that Java integrates a certain number of complex features,
making the formalization of the language (at the very least some of its
critical aspects) essential. Indeed, there are particular characteristics
of Java which have a direct impact on security and for which the informal
definitions are neither comprehensive nor free of ambiguity.
Recently, Sun published the definition of a version of Java, called
Java Card, intended for programming smart cards. Java Card was designed
by removing a certain number of constructions of Java considered to be
useless or too complex for smart cards (there are no "threads", memory
is not recovered automatically, class loading is more restricted than in
Java etc.) and by adding specific facilities to manage transactions with
a card (atomicity of a group of operations, persistent objects, etc.).
The security policy of Java (known as the "sandbox" model) which prohibits
any interaction between the objects of different applets, was modified
and relaxed. Thus, Java Card makes it possible to share an object between
The efficiency aspect did not have priority in the definition of Java.
However, since the resources of a smart card are as limited in terms of
computation as in memory, the performance of code intended to be executed
on a card becomes significant. It is necessary, therefore, to have powerful
analysis and optimization techniques for Java Card.
Axiomatization of static and dynamic semantics of Java Card and
proof of the safety of the type system of the language ("subject reduction
theorem") from this axiomatization. The property of safety is a precondition
to any specification of a security policy. It is also planned to specify
the virtual machine, its semantics, and the translation between Java Card
and byte-code of the virtual machine (a subset of the byte-code of the
Specification of security policies for Java Card. The security policy
defined for Java Card differs from that for Java by allowing a more or
less restricted sharing of objects between the applets loaded on a card.
The objective is to formalize this security policy in order to be able
to study its effect and the requirements it imposes on the components of
a Java Card application. Starting from this formalization it is proposed
to study how to prove the conformance of a program with the security policies.
Optimization of Java Card applications. This concerns adapting and
formalizing traditional methods of optimization to Java Card programs as
well as developing new techniques. The goal is to minimize execution time
and memory consumption, while showing that optimizations do not threaten
the security policies. Transparencies
of R. Guider on the analysis of the form of object structure.
of an environment for the semantic analysis of Java Card programs in Centaur.
This environment should serve as a development tool for Java Card programs.
During the design stage, one will have information on the typing of variables
(e.g. the set of dynamic types that an entity of the program can take)
and on properties relating to applet security (e.g. the set of interactions
with the environment). During execution, the topology of the object
graph can be visualized, together with their attributes, the composition
of subsystems and their interaction generated by the use of applets, communications
with the external world, etc. Transparencies
of C. Courbis on the Java card development environment.