Java bytecode verification on Java cards

A Java program is usually translated into an intermediate language, known as Java Virtual Machine Language (JVML), which is then executed by a Java Virtual Machine (JVM). Before its execution a JVML program is verified to prevent a wide range of run-time errors. Nowadays, Java applets are available for various kinds of portable devices, including modern Java smart cards. However, Java cards cannot execute the classical verification algorithms, due to their very small amount of working memory.We present a new algorithm to verify a subset of the Java bytecode language, suitable to be executed in low-memory environments, such as Java smart cards. The method is based on abstract interpretation of the language operational semantics. We define an abstract small-step semantics of the language, able to keep information regarding the modifications of data during Java constructs execution. We state the equivalence between our verification algorithm and the "standard" one. Moreover, we discuss the low memory requirements of the algorithm.