Nach positiver Absolvierung der Lehrveranstaltung sind Studierende in der Lage eine statische Analysetechnik zur Durchsetzung von Sicherheits- und Datenschutzeigenschaften in kryptographischen Protokollen und Bytecode zu entwickeln.In diesem Kurs werden insbesondere die Grundlagen der statischen Analyse von Sicherheits- und Datenschutzmerkmalen erläutert, wobei ein besonderer Schwerpunkt auf Typsystemen und SMT-Lösungen liegt. Die Studierenden lernen, eine statische Analyse zu formalisieren, ihre Richtigkeit zu belegen und mit modernsten Verifikationswerkzeugen effizient umzusetzen.
Der Kurs basiert auf einer Kombination aus theoretischer Vorlesung und praktischen Erfahrungen mit modernsten Verifizierungswerkzeugen (ProVerif, Z3, F*).
ECTS Breakdown:---------------------------------------------------
30 Std. Vorlesung, Tutorial, Klausur
40 Std. Selbststudium
80 Std. Projekte und Übungen
---------------------------------------------------150 Stunden (6 ECTS)
Die Bewertung erfolgt anhand von Projekten und einer schriftlichen Prüfung.
Ein gewisser Hintergrund in Bezug auf Verifikation und Sicherheit ist ideal, aber auch motivierte Studenten mit einem guten Hintergrund in beiden Bereichen sind im Kurs willkommen.
