Sprungmarken

Servicenavigation

Hauptnavigation

Sie sind hier:

Hauptinhalt

Fachprojekt: Formale Methoden in der IT-Sicherheit

Veranstalter: Malte Mues ()
Prof. Dr. Falk Howar ()
Typ: Fachprojekt
Modulnummer: TBA
Termine: TBA

Beschreibung

Formale Methoden zur Führung von Beweisen über die Korrektheit von Software werden seit mehreren Jahrzehnten in der Forschung untersucht. In den letzten Jahren finden diese jedoch auch verstärkt Einzug in Werkzeuge, die produktiv zur Qualitätssicherung von Software eingesetzt werden.

Als besonders effektiv haben sich auf symbolische Ausführung gestützte Tools für Crash-Testing erwiesen. Des Weiteren werden Bounded Model Checker erfolgreich in der Praxis genutzt, um Software auf Sicherheitslücken zu untersuchen.

Im Rahmen des Fachprojektes werden wir uns im ersten Schritt mit auf formalen Methoden basierenden Werkzeugen zur Detektion von IT-Sicherheitslücken beschäftigen. Dazu betrachten wir IT-Sicherheitslücken-Muster und versuchen, diese an Capture-The-Flag-VMs selber auszunutzen. Anschließend nutzen wir das gewonnene Wissen über die Funktionsweise von Sicherheitslücken, um zu erarbeiten, wie concolische Ausführung und Bounded Model Checking zur automatischen Detektion von Schwachstellen eingesetzt werden können. Dies kombinieren wir mit kurzen Ausflügen in die Welt der dynamischen und statischen Taint-Analyse.

Sollten Ihnen die Themen noch nichts sagen, ist dies nicht schlimm. In wöchentlichen Vorlesungen von 90 Minuten stellen wir die Theorie zunächst vor, in den begleitenden Übungen erproben Sie diese dann selbstständig am Beispiel.

In der zweiten Hälfte des Fachprojektes wollen wir die Theorie lebendig werden lassen. Sie wählen in der zweiten Hälfte eines der vorgestellten Werkzeuge und Analyseverfahren aus, mit dem Sie sich in Zweiergruppen intensiver auseinandersetzten wollen. Dieses Werkzeug erproben sie an einem abgesteckten Stück echter Software und präsentieren zum Abschluss die Ergebnisse.

Bei Fragen zur Veranstaltung steht Malte Mues gerne als Ansprechpartner zur Verfügung.

Voraussetzungen

  • Grundlegende Programmierkenntnisse in Java und C
  • Interesse an Formalen Methoden und IT-Sicherheit
  • Erfolgreiche Prüfung in DAP1

Themen

  • IT-Sicherheitsschwachstellen
  • Symbolische Ausführung
  • Taint-Analyse
  • Bounded Model Checking
  • SMT-Solving

Anmeldung

Die Anmeldung erfolgt über das zentrale Anmeldesystem für Fachprojekte der Fakultät.

Termine

TBA

Leistung

Wird zusammen mit dem Eintrag im Modulhandbuch bekannt geben.

In jedem Fall ist die abschließende Präsentation Teil der Prüfungsleistung.



Nebeninhalt

Kontakt

Malte Mues, M.Sc.
Tel.: 0231 755-7544
Falk Howar, Prof. Dr.
Tel.: 0231 755-7945