Verifiziert sicherer Informationsfluss mit Events

Typ:	BA
Datum:	05.08.2013
Betreuer:	Daniel Grahl
Aushang:

Die Vertraulichkeit von Informationen ist gerade in sensiblen Bereichen (z. B. Kapitalverkehr, Infrastruktur, etc.) von großer Bedeutung. In der Praxis wurde jedoch immer wieder über gravierende Informationslecks berichtet, über die vertrauliche Informationen (z. B. Kontodaten, Passwörter, Ansatzpunkte für andere Angriffe) nach außen gelangen.

Ziel der Forschungsarbeit an unserem Lehrstuhl ist daher, mit Mitteln der formalen Verifikation zu zeigen, dass ein gegebenes Stück Software keine (oder nur in spezifizierten Maßen) Informationen veröffentlicht. Die Analyse findet sprachbasiert statt, d.h. Java-Quellcode wird statisch untersucht. Dynamische Methoden (z. B. Testen) sind stets unzureichend, da sie nicht alle möglichen Ausführungen betrachten können. Und während bisherige statische Methoden oft Falschmeldungen (false positives) produzieren, d.h. unvollständig sind, arbeiten wir mit einer semantisch präzisen Analyse. So ist etwa ein Programm sicher, dass zwar geheime Daten in einen Zwischenspeicher schreibt, diesen aber löscht bevor die Daten über öffentliche Kanäle ausgegeben werden.

Ein großer Nachteil dieser Verfahrens ist, dass es nicht automatisiert abläuft (oderzumindest mit hohen Kosten verbunden ist). Das liegt daran, dass die Frage, ob ein Programm eine gewisse Eigenschaft erfüllt (z. B. Terminierung oder eben Informationsfluss), im Allgemeinen unentscheidbar ist. Ein Ansatz, die Situation zu verbessern, ist, ein abstrakteres und damit (hoffentlich) einfacheres Problem zu betrachten. In der eventbasierten Analyse sollen daher nicht mehr die konkreten Änderungen von Zustand und Kontrollfluss betrachtet werden, sondern abstrakte Events, z. B. Lese-, Schreib- oder Aufruf-Events.

In Rahmen dieser Bachelorarbeit soll eine Erweiterung der bekannten Spezifikationssprache Java Modeling Language (JML) um Elemente, die auf expliziten Events basieren, erarbeitet werden. Damit Java-Programme dann gegen solche Spezifikationen mit dem KeY-Beweiser verifiziert werden können, ist es notwendig, dass Events auch in die KeY unterliegende dynamische Logik zu integrieren. Die Arbeit soll mit einer entsprechenden Implementierung abschließen.

Gute Kenntnisse in der Programmierung mit Java und aus der Vorlesung "Formale Systeme" werden vorausgesetzt. Die Ausarbeitung in englischer Sprache ist erwünscht.