Formalizing the safety of Java, the Java virtual machine, and Java card

1 December 2001

journal article
Published by Association for Computing Machinery (ACM) in ACM Computing Surveys

Vol. 33 (4) , 517-558
https://doi.org/10.1145/503112.503115

Abstract

We review the existing literature on Java safety, emphasizing formal approaches, and the impact of Java safety on small footprint devices such as smartcards. The conclusion is that although 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 build trust in Java safety, and thence to achieve ITSEC level 6 or Common Criteria level 7 certification for Java programs.

Keywords

This publication has 66 references indexed in Scilit:

Java consistency
ACM Transactions on Computer Systems, 2000
Initialization problems for Java
Software - Concepts & Tools, 2000
Model checking JAVA programs using JAVA PathFinder
International Journal on Software Tools for Technology Transfer, 2000
A practical method for specification and analysis of exception handling-a Java/JVM case study
IEEE Transactions on Software Engineering, 2000
Secure execution of Java applets using a remote playground
IEEE Transactions on Software Engineering, 2000
Secure Java class loading
IEEE Internet Computing, 1998
Programming languages for mobile code
ACM Computing Surveys, 1997
The model checker SPIN
IEEE Transactions on Software Engineering, 1997
Polymorphic type, region and effect inference
Journal of Functional Programming, 1992
Safe programming
BIT Numerical Mathematics, 1978