Byte code verification for java smart cards based on model checking

Abstract

The paper presents a novel approach to Java byte code verification: The verification process is performed "offline" on a network server, instead of incorporating it in the client. Furthermore, the most critical part of the verification process is based upon a formal model and uses a model checker for checking the verification conditions. The result of the verification process can be securely communicated to the runtime platform with cryptographic means. The major advantages of our approach are twofold: On the one hand, it offers a higher degree of security, since the verification process is based on a formal framework. Secondly, it saves resources on the client's side, since the process of byte code verification can be replaced by a simple check of a digital signature. This paper concentrates on Java smart cards, where resource limitations inhibit fully-fledged byte code verification within the client, but the demand for security is very high. However, our approach can also be applied to other variants of Java.