Diese Dissertation befasst sich mit dem Bereich der sprachbasierten Informationsflussanalyse und erweitert den aktuellen Kenntnisstand insbesondere in den Gebieten der Erkennung und Ausnutzung unsicheren Informationsflusses in Programmen.

Zum Erreichen dieses Ziels werden im Rahmen dieser Arbeit Verfahren entwickelt, die es ermöglichen, unsicheren Informationsfluss in Programmen zu erkennen und dessen Folgen fundiert einzuschätzen. Die entwickelten Verfahren zeichnen sich durch einen hohen Automatisierungsgrad sowie eine hohe Präzision aus.

Im ersten Teil der Dissertation wird ein Verfahren entwickelt, das es erlaubt unsicheren Informationsfluss zu entdecken und aufzuzeigen. Das entwickelte Verfahren kombiniert symbolische Ausführung mit Selbstkomposition (self-composition) von Programmen mit dem Ziel logische Formeln, sog. Unsicherheitsformeln, abzuleiten. Die Modelle dieser Formeln beschreiben initiale Zustandspaare, mit deren Hilfe unsicherer Informationsfluss demonstriert werden kann. Dazu werden Unit-Tests (Leak Demonstrators) erzeugt, die das Programm jeweils in einem der initialen Zustände ausführen und fehlschlagen, wenn ein unsicherer Informationsfluss entdeckt wird. Das entwickelte Verfahren unterstützt unbegrenzte Schleifenausführungen und rekursive Methodenaufrufe mit Hilfe von Programmspezifikationen wie Schleifeninvarianten und Methodenverträgen. Diese Vorgehensweise erlaubt auf der einen Seite eine hohe Präzision (d.h., keine False Positives) und auf der anderen Seite aber auch Abstraktion (und damit eine Zunahme von False Positives) bei höherem Automatisierungsgrad. Der Ansatz unterstützt die Informationsflusspolitiken Noninterference, Delimited Information Release und Information Erasure.

Der zweite Teil der Dissertation baut auf dem oben beschrieben Verfahren auf. Es erlaubt jedoch nicht nur die Demonstration des Vorhandenseins von unsicherem Informationsfluss, sondern ermöglicht es dessen Auswirkungen einzuschätzen. Dazu bettet es das bisherige Verfahren in eine hybride Analyse ein, die einen adaptiven Angriff auf das Programm unter Ausnutzung der entdeckten Unsicherheitsstellen realisiert. Das entwickelte Verfahren führt dazu eine Reihe von Experimenten durch und reichert systematisch das Wissen über das im Programm enthaltene Geheimnis an. Ein Experiment besteht aus einer konkreten Programmausführung mit optimal gewählten Eingabewerten basierend auf einer angenommenen A-priori-Verteilung der Werte des Geheimnisses und des durch die vorherigen Experiment angesammelten Wissens über das aktuell vorliegende Geheimnis. Optimal bedeutet, dass die Programmausführung einen maximalen Wissenszuwachs bedingt. Das entwickelte Verfahren grenzt sich von bisher existierenden Ansätzen dadurch ab, dass es den Informationsfluss als explizite Funktion in Abhängigkeit von öffentlichen Eingabewerten (low inputs), basierend auf Ergebnissen aus der symbolischen Programmausführung und parametrischer Modellzählung präsentiert. In Abhängigkeit von der gewählten Sicherheitsmetrik werden allgemeine nicht-lineare Optimierer und Max-SMT-Problemlöser verwendet, um optimale Eingabewerte zur Geheimnisextraktion zu bestimmen.

Die beiden Ansätze wurden implementiert und sind als Programmanalysewerkzeug KEG, basierend auf dem deduktiven Verifikationssystem KeY, verfügbar. KEG ermöglicht (zu einem hohen Grad) die Analyse sequentieller Java-Programme und erzeugt JUnit Testfälle, um unsicheren Informationsfluss zu demonstrieren. Für die Geheimnisextraktion erzeugt KEG zum Durchspielen eines Angriffs kleine Java Programme und führt diese aus.

Im Rahmen dieser Arbeit wurden die Verfahren mit Hilfe von Microbenchmarks und zweier Fallstudien evaluiert. Die Arbeit beschreibt die Planung sowie Durchführung der Evaluationen und diskutiert deren Ergebnisse.

Die Durchführung der Microbenchmarks zeigte, dass KEG alle unsicheren Informationsflüsse erkennen konnte und entsprechende Demonstratoren erzeugte, sofern die notwendigen Spezifikation korrekt und ausreichend vollständig waren. Es konnte auch nachgewiesen werden, dass KEG bei der Geheimnisextraktion wesentlich effizienter ist als ein Angreifer, der mit zufällig gewählten Experimenten arbeitet.

KEG bewies in den beiden Fallstudien, dass die Verfahren auch zur Analyse realistischerer Programme eingesetzt werden können. Die erste Fallstudie betrachtet eine vereinfachte Version einer realen e-Voting Software mit unbegrenzten Schleifenausführungensowie, Objekt- und Arraydatentypen. Neben der allgemeinen Anwendbarkeit von KEG konnte insbesondere demonstriert werden, dass sich KEG gut mit einem Spezifikationserzeugungswerkzeug kombinieren lässt, um eine vollautomatische Analyse des Programms zu erreichen.

Die zweite Fallstudie betrachtet einem der Literatur entnommenen Algorithmus zum Überprüfen der Integrität von PINs. KEG bewies hier, dass es unter Annahme einer ausreichend guten A-priori-Verteilung der Geheimniswerte einem Angreifer erlaubt, die geheimen PINs effizienter zu extrahieren.