Formalising the safety of Java, the Java Virtual Machine and Java Card

Paper announcement:

P. H. Hartel and L. Moreau
Formalizing the Safety of Java, the Java Virtual Machine and Java Card
ACM Computing Surveys, to appear, 2001.

We review the existing literature on Java safety, emphasizing
formal approaches, and the impact of Java safety on small
footprint devices such as smart cards. The conclusion is that while a
of good work has been done, a more concerted effort is needed to build
a coherent set of machine readable formal models of the whole of Java
and its implementation. This is a formidable task but we believe it is
essential to building trust in Java safety, and thence to achieve
ITSEC level 6 or Common Criteria level 7 certification for Java

\category{C.3}{Computer Systems Organisation}

  {Special-purpose and application-based systems}[Smart cards]
\category{D.2.4}{Software}{Software/Program Verification}
\category{D.3.1}{Software}{Formal Definitions and Theory}[Semantics]



Professor Pieter Hartel
Distributed and Embedded Systems Group
Department of Computer Science
University of Twente
PO Box 217, 7500 AE Enschede, The Netherlands
Telephone: +31 (53) 489 2411
Fax: +31 (53) 489 4590
Email: pieter@cs.utwente.nl