192.059 Formal Methods for Security and Privacy
Diese Lehrveranstaltung ist in allen zugeordneten Curricula Teil der STEOP.
Diese Lehrveranstaltung ist in mindestens einem zugeordneten Curriculum Teil der STEOP.

2021S, VU, 4.0h, 6.0EC
TUWEL

Merkmale

  • Semesterwochenstunden: 4.0
  • ECTS: 6.0
  • Typ: VU Vorlesung mit Übung
  • Format der Abhaltung: Distance Learning

Lernergebnisse

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.

Inhalt der Lehrveranstaltung

  • Analyse kryptographischer Protokolle über Typsysteme und SMT - Lösung (Applied Pi-Calculus und ProVerif)
  • Sprachbasierte Sicherheit (Nichteinmischung, Hypereigenschaften und Seitenkanäle)
  • Grundlagen der statischen Analyse (Taint Analysis, Symbolic Ausführung, SMT-Lösung
  • Statische Analyse von Bytecode (Ethereum Smart Contracts)
  • Sichere Programmierung in F *

 

Methoden

Der Kurs basiert auf einer Kombination aus theoretischer Vorlesung und praktischen Erfahrungen mit modernsten Verifizierungswerkzeugen (ProVerif, Z3, F*).

Prüfungsmodus

Prüfungsimmanent

Weitere Informationen

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

30 Std. Vorlesung, Tutorial, Klausur

40 Std. Selbststudium

80 Std. Projekte und Übungen

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

 

Vortragende Personen

Institut

LVA Termine

TagZeitDatumOrtBeschreibung
Di.14:00 - 15:0002.03.2021 https://tuwien.zoom.us/j/97506040156Presentation of all security courses at TU Wien (not specific to 192.059)
Do.10:00 - 11:0004.03.2021 (LIVE)Introduction
Do.10:00 - 12:0025.03.2021 (LIVE)Q/A on Type Systems for Cryptographic Protocols
Do.10:00 - 12:0015.04.2021 (LIVE)Q/A on ProVerif
Do.10:00 - 12:0029.04.2021 (LIVE)Q/A on Information Flow Analysis
Do.10:00 - 12:0006.05.2021 (LIVE)Q/A on F*
Do.10:00 - 12:0020.05.2021 (LIVE)Q/A on Low-Level Code Analysis

Leistungsnachweis

Die Bewertung erfolgt anhand von Projekten und einer schriftlichen Prüfung.

Prüfungen

TagZeitDatumOrtPrüfungsmodusAnmeldefristAnmeldungPrüfung
Do.10:00 - 13:0023.09.2021 Zoomschriftlich19.07.2021 12:00 - 22.09.2021 23:00in TISSRetake Exam

LVA-Anmeldung

Von Bis Abmeldung bis
15.02.2021 13:00 28.03.2021 14:00 28.03.2021 14:00

Curricula

Literatur

Es wird kein Skriptum zur Lehrveranstaltung angeboten.

Vorkenntnisse

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.

Sprache

Englisch