Verifying Java Card Programs

One of the fundamental assumptions of the KeY project at its beginning was that it should support verification of an actual programming language and handle realistic programs. Back then, complete handling of arbitrary Java programs was still considered an unreachable goal in source code based interactive verification. For that reason a simpler, yet actually existing and officially developed, Java technology was chosen as our verification target, namely Java Card—a considerably stripped down version of Java for programming smart cards [Chen, 2000]. The additional motivation for choosing this particular technology were the corresponding application areas that are subject to strict security requirements. Nowadays, smart cards are widely used in the financial sector (bank cards), telecommunications (SIM cards), identity (electronic passports and identity cards), and transportation (electronic tickets). Many of the products are indeed developed on the Java Card platform, in particular, the Dutch biometric passport is based on the Java Card technology. The security requirements of such applications and, sadly, still often occurring security problems in this area 1 highly justify the use formal verification.