Modellierung von Angriffen für quantitative Sicherheitsanalysen
|
Typ | Masterarbeit |
|---|---|---|
| Aushang | ||
| Betreuer | Wenden Sie sich bei Interesse oder Fragen bitte an: Frederik Reiche (E-Mail: frederik.reiche@kit.edu, Telefon: +49-721-608-45992), Florian Lanzinger |
Hintergrund
Die meisten Methoden für formale Softwareverifikation geben ein binäres Ergebnis aus: Die Software ist entweder korrekt oder nicht. Qualitätsmaße wie Testabdeckung sind selten robust. In einer Zusammenarbeit der Lehrstühle Prof. Beckert und Prof. Reussner entstand deshalb ein Ansatz zur formalen quantitativen Verifikation der Software-Zuverlässigkeit. Zuerst ermittelt das Verifikationswerkzeug KeY alle Eingaben, für die die Korrektheit der Software nicht bewiesen werden kann. Diese kritischen Eingaben werden dann in ein Palladio-Architekturmodell hinzugefügt. Das resultierende Modell wird daraufhin in ein probabilistisches Programm übersetzt, wodurch so Fehlerwahrscheinlichkeiten für das System errechnet werden. Dieser Ansatz ist bisher auf funktionale Korrektheit bzw. Zuverlässigkeit beschränkt. Eine Analyse der Sicherheit, bei der auch Angreifer berücksichtigt werden, ist bisher nicht möglich.
Aufgabe
Ihre Aufgabe ist es, den existierenden Ansatz mit im Hinblick auf Angriffssicherheit zu erweitern. Das beinhaltet unter anderem
- das Entwickeln einer geeigneten Angreifermodellierung als Erweiterung des Palladio Komponentenmodells. Die Modellierung soll es hierbei erlauben, Szenarien als Angriffsbäume (siehe Grafik) zu beschreiben. Hierbei soll das Verhalten des Angreifers sowohl probabilistisch (der Angreifer wählt eine zufällige Handlungsoption) als auch possibilistisch (der Angreifer weiß, welche Handlungsoption die beste Erfolgswahrscheinlichkeit birgt, und verhält sich entsprechend) beschrieben werden können.
- Mit dieser Modellierung soll dann die Analyse erweitert werden. Die Quantifizierung der Sicherheit bezieht sich dann auf die Kosten und Schwere möglicher Angriffe.