Byte Code Verification for Java Smart Cards Based on Model Checking

摘要

The paper presents a novel approach to Java byte code verification: The verification process is performed "offline" on a network server, isntead of incorporating it in the clien. 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.