Verification of Java Card Programs

Smart cards are used in security critical applications where money or private data is involved. Examples are the German Geldkarte or new passports with biometrical data. Design or programming errors can have severe consequences. Formal methods are the best means to avoid errors. Java Card is a restricted version of Java to program smart cards. This work presents a logical calculus to formally prove the correctness and security of Java Card programs. The calculus is implemented in the KIV system, and ready for use. First, an operational big-step semantics for sequential Java is presented based on algebraic specifications. All Java language constructs are modeled. Then, a sequent calculus for dynamic logic for Java Card is developed, and the correctness of the calculus is formally proved. The calculus is designed to support libraries, the reuse of proofs, and program modifications. This entails two different notions of type soundness, the standard one, and a weaker version. Furthermore, the calculus is not restricted to Java Card, but can be used for arbitrary sequential Java program. The work ends with some intricate examples. All properties and theorems are formally proved with the KIV system. The resulting verification system is able to cope with real-life e-commerce applications.Smart Cards werden in sicherheitskritischen Anwendungen benutzt, bei denen Geld oder private Daten involviert sind. Beispiele sind die Geldkarte oder neue Reisepässe mit biometrischen Daten. Entwurfs- oder Programmierfehler können schwerwiegende Konsequenzen haben. Formale Methoden bieten die beste Garantie um Fehler zu vermeiden. Java Card ist eine eingeschränkte Version von Java zur Programmierung von Smart Cards. Diese Arbeit präsentiert einen logischen Kalkül, um formal die Korrektheit und Sicherheit von Java Card Programmen zu beweisen. Der Kalkül ist im KIV System implementiert und einsatzbereit. Als erstes wird eine operationale (big-step) Semantik für sequentielles Java basierend auf algebraischen Spezifikationen präsentiert. Alle Java Sprachkonstrukte sind modelliert. Dann wird ein Sequenzenkalkül für eine dynamische Logik für Java Card entwickelt, und die Korrektheit des Kalküls formal bewiesen. Der Kalkül wurde speziell entworfen um Bibliotheken, die Wiederverwendung von Beweisen und Programmänderungen zu unterstützen. Dies bedingt zwei verschiedene Definitionen von Typsicherheit, die übliche und eine schwächere Version. Darüberhinaus ist der Kalkül nicht auf Java Card beschränkt, sondern kann für beliebige sequentielle Java Programme verwendet werden. Die Arbeit endet mit einigen komplizierten Beispielen. Alle Eigenschaften und Theoreme wurden formal mit dem KIV System bewiesen. Das entstandene Verifikationssystem ist in der Lage, reale E-Commerce Anwendungen zu behandeln