Nach positiver Absolvierung der Lehrveranstaltung sind Studierende in der Lage eine statische Analysetechnik zur Durchsetzung von Sicherheits- und Datenschutzeigenschaften in  kryptographischen Protokollen, Bytecode, und Deep Neural Networks zu entwickeln.

In diesem Kurs werden insbesondere die Grundlagen der statischen Analyse von Sicherheits- und Datenschutzmerkmalen erläutert, wobei ein besonderer Schwerpunkt auf SMT-Lösungen und Typsystemen liegt. Die Studierenden lernen, eine statische Analyse zu formalisieren, ihre Richtigkeit zu belegen und mit modernsten Verifikationswerkzeugen effizient umzusetzen.

Grundlagen  (6 Vorlesungen)

• Static Analysis of Cryptographic Protocols  (ProVerif)
• Language-based Security (Information Flow)
• Static Analysis of Bytecode (Ethereum Smart Contracts)
• Refinement Types (F*)
• Static Analysis of Deep Neural Networks

Fortgeschrittene Themen (Präsentationen von Studierenden):   

• Side Channels 
• Security of Machine Learning Models
• Mobile Security
• Web Security
• Blockchain Security

Der Kurs basiert auf einer Kombination aus

• Vorlesungen über die theoretische Grundlagen mit wöchentlichen Hausaufgaben
• Presentationen von Studierenden zu fortgeschrittene Themen
• Forschungsprojekt

ECTS Breakdown:
---------------------------------------------------

25 Std. Vorlesung, Presentationen

50 Std. Selbststudium und Hausaufgaben

75 Std. Projekt

---------------------------------------------------
150 Stunden (6 ECTS)

Die Bewertung erfolgt anhand von Hausaufgaben, einer Präsentation, der aktiven Teilnahme an Präsentationen, und einem Forschungsprojekt.

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.