Towards Development of Safe and Secure Java Card Applets

This thesis is concerned with different aspects of Java Card application development and use of formal methods in the Java Card world. Java Card is a technology that provides means to program smart (chip) cards with (a subset of) the Java language. The use of formal methods in the Java Card context is highly justified due to the criticality of Java Card applications. First of all, Java Card applications are usually security critical (e.g., authentication, electronic cash), second, they are cost critical (i.e. they are distributed in large amounts making updates quite difficult) and finally, they can also be legally critical (e.g., when the digital signature law is considered). Thus the robustness and correctness of Java Card applications should be enforced by the best means possible, i.e. by the use of formal verification techniques. At the same time Java Card seems to be a good target for formal verification - due tothe relative simplicity of Java Card applications (as compared to full Java), formal verification becomes a feasible and manageable task. In this thesis, we touch upon different levels of Java Card application development and the use of formal methods. We start by defining a UML/OCL supported development process specifically tailored to JavaCard applications, then we go on to define an extension to the logic used in formal verification of Java Card programs to handle so called "rip out" properties (properties that should be maintained in case of an unexpected termination of a Java Card program), which are specific to Java Card. Finally, we end up with a simple tool support for Java Card program compilation and testing inside a CASE tool. The thesis contains three papers focusing on these aspects. The main purpose of this work is to ensure the robustness of Java Card applications by providing a well defined development process and means to formally verify properties specific to Java Card applications to be able to develop Java Card applets which are robust "by design". At the sametime we want to make rigorous Java Card development relatively easy, tool supported (automated wherever possible) and usable by people that do not have years of training in formal methods