Effiziente Verifikation von Informationssicherheit

Typ:	BA
Datum:
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.

An unserem Lehrstuhl wird daher daran geforscht, 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. Diese Methode wurde bereits in das von unserem Lehrstuhl mitentwickelte KeY-System integriert.

Allerdings besitzen präzise Methoden wie diese den Nachteil, dass sie menschliche Interaktion benötigen oder hohe Komplexität haben. Dadurch ensteht gerade für "offensichtlich" sichere Programme ein deutlich unnötiger Overhead.

In dieser Bachelor-Arbeit sollen die Ideen von automatischen (aber unvollständigen) Methoden wie Typsystemen und formaler Verifikation zusammengebracht werden. Dabei bauen wir auf das KeY-System auf. Es ist regelbasiert und verwendet den aus "Formale Systeme" bekannten Sequenzenkalkül. Daher ist es durch Hinzufügen von Regeln sehr leicht erweiterbar. Die bisherigen Regeln sind jedoch nicht auf die Verifikation von Informationsflüssen optimiert. Die zentrale Aufgabe dieser Arbeit besteht darin, Regeln zu entwickeln, durch die die "offensichtlichen" Fälle effizient und automatisch bewiesen werden können.

Gute Kenntnisse aus der Vorlesung "Formale Systeme" werden vorausgesetzt. Programmierkenntnisse sind nicht notwendig. Die Ausarbeitung in englischer Sprache ist erwünscht.