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

To: <types@cis.upenn.edu>
Subject: Formalising the safety of Java, the Java Virtual Machine and Java Card
From: "Pieter Hartel" <pieter@cs.utwente.nl>
Date: Thu, 15 Nov 2001 14:33:29 +0100
Reply-To: "Pieter Hartel" <pieter@cs.utwente.nl>

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.



\begin{abstract}
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
lot
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
programs.
\end{abstract}

\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]


http://www.ub.utwente.nl/webdocs/ctit/1/00000050.pdf

--pieter

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
http://www.cs.utwente.nl/~pieter/