On the road to Bandol

Every time that a Java Card specification comes out, I like to think that it is a good specification, and in particular that it provides complete information for developers. We have tried hard, but the completeness remains hard to reach. Not that the spec is bad, which is not true. The Java Card Forum has been busy over years trying to define a good spec, Sun has done a very good job at making our ramblings into well-written specifications, and we also have been pretty good at proofreading all this.

The most interesting part of a specification ‘s evolution is not necessarily the entirely new features that get added at each significant release. Of course, we have to evolve with time, and Java Card is no exception. Some other features, in the meantime, seem to have a life of their own: they don’t really change, but it seems that their description needs to be clarified at each release.

In Java Card, we have a few of these. No surprise, they are the features that are specific to our platform: application isolation and sharing, atomicity and transactions, among others.

Some researchers have taken the task of formalizing Java Card, and they often stumble upon these things. A few years ago, while building a formal model of the firewall, some of my colleagues identified a security issue with some API methods that severely weakened the firewall. More recently, Wojciech Mostowski and some colleagues from Radboug University Nijmegen have worked on transactions, and their findings, that I heard about at this year’s e-Smart conference, are as follows:

• There is a bug in the Java Card 2.2 specification, which states that the outcome of a non-atomic operation in unpredictable when it is performed in a transaction that is aborted. This leads the reader to believe that the behavior of these operations is predictable outside of transactions, and I don’t think that this is the intent of the spec.
• They also point to the fact that the behavior obtained when mixing atomic and non-atomic operations and atomic operations in a transaction that gets aborted is in fact quite predictable, although one needs to think about it first.
• They also found that the result of an interrupted non-atomic operation is indeed unpredictable, and may even lead to random values.
• Finally, they have been able to build a usable formal model that takes into consideration all these unpredictable behaviors, which is great.

In practice, this means that the non-atomic methods in Java Card are very hard to use, and should be used very carefully (it must be acceptable to replace any of these operations with a random write, and this is quite uncommon). It also means that the implementations are rather good.

Finally, it also shows that even after 5 or 6 releases, some items in a specification remain very hard to describe accurately. This paper was a finalist for the Java Card Forum prize, and it definitely deserved it, because it actually served the JCF.