Verlässlichkeitsgarantie für kritische Rechnersystem

Ein Informatiker der Uni Augsburg hat einen Code entwickelt, der das bislang mögliche Niveau von Verlässlichkeitsgarantien kritischer Computersysteme entscheidend anheben soll. Dafür erhielt er nun den Kulturpreis Bayern der E.ON Bayern AG. Sicherheitskritische Java-Anwendungen

Softwareprodukte weisen immer wieder Fehler auf, welche die Datensicherheit in Frage stellen und das Vertrauen in die Korrektheit kritischer Anwendungen beeinträchtigen. Der Einsatz formaler Methoden bietet die derzeit maximal möglichen Garantien für die Verlässlichkeit von Computersystemen. Bisherige Ansätze zur formalen Behandlung von kommunizierenden Anwendungen erlauben allerdings keine verlässliche Aussage über die Sicherheit einer tatsächlichen Implementierung. Sie beschränken sich meist auf die Verifikation von Modellen.

Hier setzt die Doktorarbeit "Formale Verifikation der Korrektheit sicherheitskritischer Java-Anwendungen" des Informatikers Dr. Holger Grandy an. Basierend auf Theorien zur formalen Verfeinerung von Systemen führt sie bisherige Verifikationsansätze bis zur Codeebene fort. Sie liefert als Hauptergebnis eine Spezifikations- und Verifikationsmethodik. Diese erlaubt es, formale Beweise für die Sicherheit von Anwendungen auf einem Modell zu führen und diese dann formal korrekt auf eine tatsächliche System-Implementierung zu übertragen. In seiner Studie illustriert Grandy diese Methodik an zwei Anwendungen für Mobiltelefone und Chipkarten.

Den Fortschritt würdigte die Jury des E.ON Kulturpreises Bayern als exzellente wissenschaftliche Spitzenleistung. Grandy erhielt als einer von zehn Preisträgern in der Kategorie „Universitäten“ den mit 4.000 Euro dotierten Preis. (dsc)