Bart Jacobs, Joe Kiniry and Erik Poll, University of Nijmegen
Using JML and ESC/Java2 for JavaCard Applet Verification
Abstract: JML is a formal specification language for Java that we have been
using in Nijmegen to specify and verify JavaCard programs over
the past few years.
ESC/Java2 is the Open Source evolution of the Extended Static Checker
for Java, originally developed by the SRC group at Compaq. ESC/Java2
has been developed by Cok and Kiniry, was initially made available in
September of 2003, and has now seen over half a dozen releases.
ESC/Java2 supports the full Java 1.4 language, accepts annotations
consistent with the current version of JML (4.X), improves the general
usability of the tool by packaging it in an easy-to-use form, and
increases the amount of JML specification that is statically checked.
ESC/Java2 incorporates several new features that make it capable of
reasoning about much more complex applications. In particular, we can
now attempt to statically verify JavaCard applets that use the
JML-annotated JavaCard API. We will discuss some of these new
features in this talk and report on our progress with statically
checking JavaCard applets.
Peter Müller, ETH Zurich
A Type System for Checking Applet Isolation in Java Card
Abstract: A Java Card applet is, in general, not allowed to access fields and methods
of other applets on the same smart card. This applet isolation property is
enforced by dynamic checks in the Java Card Virtual Machine. This paper
describes a refined type system for Java Card that enables mostly static
checking of applet isolation. With this type system, most firewall
violations are detected at compile time.
Robby, Edwin Rodriguez, Matthew B. Dwyer and John Hatcliff, Kansas State University
Checking JML Specifications Using Model Checking
Abstract: The Java Modeling Language (JML), a general purpose behavioral
specification language for Java, has been used to specify properties of
JavaCard applications in the context of the LOOP and JACK projects.
Both of these tools use theorem prover technologies that provide
a high-degree of behavioral coverage, but are limited in the degree
of automation, difficulty of use and, hence, scalability.
Other technologies make a different cost-coverage tradeoff, for
example, the runtime checking tool jmlc that is included in
the JML distribution.
We present a different approach using the Bogor software model
checking framework. We discuss how strong JML specifications of, for
example, heap allocated objects in concurrent programs and JML models
can be supported in an explicit-state and extensible model checker such
as Bogor. We then discuss the advantages of model checking relative to
other validation techniques.
Reiner Haehnle, Chalmers University of Technology
Verification of Safety Properties in the Presence of Transactions
Abstract: The Java Card Transaction mechanism can ensure that a sequence of
statements either is executed to completion or is not executed at all.
Transactions make verification of Java Card programs considerably more
difficult, because they cannot be formalised in a logic based on pre- and
postconditions. The KeY system includes an interactive theorem prover for
Java Card source code that models the full Java Card standard including
transactions. We show with a number of examples the practical difficulties
encountered during verification of safety and security relevant properties
and to which extent they have been addressed in the KeY system. We draw
some conclusions for the design and functionality of calculi and theorem
provers.