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.

The Java 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.

Publicity , Research themes, A French summary of the project's activities.

Participants

Project leader : D. Le Métayer

Post-doctoral researchers employed on the project : Ewen Denney (Lande) and Shen-Wei Yu (Oasis)

Meetings

The project has held the following meetings

Publications related to the project

Publicity

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 several applets.

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.
 

Research themes