Verifikation von Java-Programmen mit Datenbank-Anbindung

Typ:	MA / BA
Datum:	2023-04-27
Betreuer:	Mattias Ulbrich
Aushang:

Reale Applikationen sind -- zumal im Zeitalter von Web-Applikationen -- häufig an Datenbanken gekoppelt und operieren mittels Standard-Schnittstellen auf den darin enthaltenen Daten. Häufig wird dafür die Sprache Standard-Query-Language SQL verwendet, mit der die meisten relationalen Datenbanken angesprochen werden können.

Oftmals werden die Anfragen in textueller Form in Programmtext zusammengebaut und dann an die Datenbank geschickt. Dabei ist es sehr einfach, Fehler in diese Zeichenketten einzubauen, die dann Fehler im Programmverhalten oder Programmabstürze induzieren. Im schlimmsten Fall ermöglichen sie es einer Angreiferin, unerlaubt Daten auszulesen oder zu manipulieren.

KeY ist ein am Lehrstuhl entwickeltes Tool zur deduktiven Verifikation von Java-Programmen, die mit formalen Spezifikationen in der Java Modeling Language annotiert sind.

Die Aufgabe dieser Arbeit ist es, formale Methoden, die z. B. in KeY zur Verfügung stehen, auszunutzen, um damit Java-Programme, die bestimmte SQL-Anfragen auf ein bekanntes Datenbankschema anwenden, statisch zu verifizieren.

Dabei ist die Herausforderung, existierende Spezifikations- und Verifikationsmethoden so zu adaptieren, dass damit relevante Sicherheitsaussagen aus einem Datenbankschema abgeleitet und formuliert werden können, um Java-Programme mit Datenbankanbindung auf Korrektheit prüfen zu können.

Ein Beispiel

Das folgende Java-Fragment zeigt das Potenzial für statische Analysen von Java-Code mit Datenbank-Anbindung. In diesem Fragment wird eine Datenbank angefragt, um alle Info-Studierenden mit ihrem Alter abzufragen. Es soll für alle jungen Studierenden eine Ausgabe getätigt werden.

Dieses Programmfragment wird vom Übersetzer akzeptiert, es wird aber zur Laufzeit abstürzen, denn die Anfage set.getInt(0) greift auf das Studienfach als Ganzzahl zu.

Unter Ausnutzung des statisch bekannten Datenbankschemas kann eine statische Analyse des Programmcodes herausfinden, dass hier ein Typfehler vorliegt.

Für dieses einfache Beispiel könnte ein geeignetes Java Typsystem helfen, um die Korrektheit statisch zu zeigen, in schwierigeren Fällen können schwergewichtigere Werkzeuge wie KeY herangezogen werden.

Ihr Profil

Sie sollten solide Java-Kenntnisse besitzen sowie das Modul Formale Systeme erfolgreich abgeschlossen haben. Grundkenntnisse im Bereich Datenbanken, wie z. B. aus dem Modul KomDat, sollten Sie besitzen.

Zusammenarbeit

Diese Arbeit wird angeboten in Zusammenarbeit mit Prof. Dr. Stefanie Scherzinger (Schwerpunk Skalierbare Datenbanksysteme) von der Universität Passau.