Formale Verifikation der Korrektheit sicherheitskritischer Java Anwendungen

Sei es im Internet beim Homebanking, bei Chipkarten wie der Geldkarte oder bei der kommenden Gesundheitskarte - Sicherheit ist einer der entscheidenden Faktoren fur die Akzeptanz und den Erfolg kommunizierender Anwendungen. Hohe Summen werden investiert, um Sicherheitsziele wie Vertraulichkeit oder Authentizitat von Daten bei Entwurf und Implementierung solcher Anwendungen zu garantieren. Dennoch finden sich fast taglich Meldungen uber Sicherheitslucken von Computersystemen in den Medien. Der Einsatz formaler Methoden bietet die derzeit maximal moglichen Garantien fur die Verlasslichkeit von Computersystemen. Bisherige Ansatze zur formalen Behandlung von kommunizierenden Anwendungen erlauben allerdings keine verlassliche Aussage uber die Sicherheit einer tatsachlichen Implementierung, sondern beschranken sich meist auf die Verifikation von Modellen. Diese Arbeit fuhrt - basierend auf Theorien zur formalen Verfeinerung von Systemen - bisherige Verifikationsansatze bis zur Codeebene fort. Hauptergebnis der Arbeit ist eine Spezifikations- und Verifikationsmethodik, die es erlaubt, formale Beweise fur die Sicherheit von Anwendungen auf einem Modell zu fuhren und diese dann formal korrekt auf eine tatsachliche Implementierung des Systems zu ubertragen. Die Methodik wird an zwei Anwendungen fur Mobiltelefone und Chipkarten illustriert.