Formalizing the safety of Java, the Java virtual machine, and Java card
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, to build a coherent set of machine-readable formal models of the whole of Java and its implementation.
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.