Verification of Java card programs [Elektronische Ressource] / von Kurt Stenzel

Veri cation of Java Card ProgramsDissertationzur Erlangung des Doktorgrades Dr. rer. nat.der Fakult at fur Angewandte Informatikder Universit at Augsburgim Jahr 2005 vonKurt Stenzel2Amtierender Dekan: Prof. Dr. Wolfgang ReifGutachter: Prof. Dr. Wolfgang ReifProf. Dr. Bernhard BauerTag der Prufung: 30. Mai 2005Prufer: Prof. Dr. Bernhard BauerProf. Dr. M ollerProf. Dr. Wolfgang ReifProf. Dr. Theo Ungerer3SummarySmart cards are used in security critical applications where money or private data isinvolved. Examples are the German Geldkarte or new passports with biometrical data.Design or programming errors can have severe consequences. Formal methods are thebest means to avoid errors. Java Card is a restricted version of Java to program smartcards. This work presents a logical calculus to formally prove the correctness andsecurity of Java Card programs. The is implemented in the KIV system, andready for use. First, an operational big-step semantics for sequential Java is presentedbased on algebraic speci cations. All Java language constructs are modeled. Then,a sequent calculus for dynamic logic for Java Card is developed, and the correctnessof the calculus is formally proved. The calculus is designed to support libraries, thereuse of proofs, and program modi cations. This entails two di eren t notions of typesoundness, the standard one, and a weaker version.