| Veranstalter: | Malte Mues (malte.mues@tu-dortmund.de) Prof. Dr. Falk Howar (falk.howar@tu-dortmund.de) |
|---|---|
| Typ: | Fachprojekt |
| Modulnummer: | INF-BSc-276 |
| Termine: | Die Informationen sind im Moodle-Raum verfügbar |
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.
Die Anmeldung erfolgt über das zentrale Anmeldesystem für Fachprojekte der Fakultät.
Die Termine werden zentral im Moodle koordiniert. Angemeldet Teilnehmer wurden dem Moodle-Raum hinzugefügt.
Aktive Teilnahme an den Übungen, Einreichung eines Projektexposees und die Projektabschlusspräsentation.