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.

2019S, VU, 4.0h, 6.0EC

Merkmale

  • Semesterwochenstunden: 4.0
  • ECTS: 6.0
  • Typ: VU Vorlesung mit Übung

Ziele der Lehrveranstaltung

Writing secure code is a challenging, since one has to make sure that
attackers cannot interfere with the program execution in order to
steal confidential data or to perform unauthorized, security-critical
operations. This task is particularly hard for various reasons:
cryptography is often required to protect messages while
in transit over the network,
programming languages (e.g., JavaScript) often feature a sophisticated and not clearly
defined semantics, and development environments (e.g., mobile OS,
web platforms, and smart contracts) are extremely complex and offer a large attack
surface.

In this course, students will learn the semantic foundations of
computer security. In particular, they will study the state-of-the-art
formal methods for the verification of security and privacy properties.  

These verification techniques are based on type systems and SMT-solving: students will study their foundations and learn how to apply them in various domains of interest, such as cryptographic protocols, source code, bytecode (e.g., Android and Ethereum). 

For instance, students will study and have hands-on experience on ProVerif, a state-of-the-art cryptographic protocol verifier, and F*, a typed programming language successfully used to verify  TLS 1.3 implementations as well as Firefox cryptographic libraries, thereby showing the
practical impact of formal methods for security and privacy in today's
software and systems (see also https://project-everest.github.io).

This is a research-oriented course, so it is particularly (but not
exclusively) indicated to those students who are potentially
interested in doing research at the intersection between logic &
verification and security & privacy, or to learn the state-of-the-art
in security and privacy verification.

Inhalt der Lehrveranstaltung

- Analysis of Cryptographic Protocols via SMT solving (Applied
Pi-Calculus and ProVerif)
- Language-based Security (Non-Interference, Hyperproperties, and Side Channels)
- Secure JavaScript Programming (Semantics and Security Type Systems for
JavaScript)
- Foundations of Security Static Analysis (Taint Analysis, Symbolic
Execution, SMT solving)
- Formal Security Analysis of Bytecode (Android, Ethereum Virtual Machine)

Weitere Informationen

ECTS Breakdown:

40h lectures, tutorials, exam

30h self-study

80h projects and exercises

Vortragende

Institut

LVA Termine

TagZeitDatumOrtBeschreibung
Mi.08:45 - 12:0013.03.2019 - 26.06.2019FAV Hörsaal 1 192.059: Formal Methods for Security and Privacy
Mi.08:45 - 12:0003.04.2019 - 05.06.2019Seminarraum Argentinierstrasse Lecture
Formal Methods for Security and Privacy - Einzeltermine
TagDatumZeitOrtBeschreibung
Mi.13.03.201908:45 - 12:00FAV Hörsaal 1 Lecture (Type Systems for Cryptographic Protocols)
Mi.20.03.201908:45 - 12:00FAV Hörsaal 1 Lecture (ProVerif)
Mi.27.03.201908:45 - 12:00FAV Hörsaal 1 Lecture (Observational Equivalence)
Mi.03.04.201908:45 - 12:00Seminarraum Argentinierstrasse Tutorial (ProVerif)
Mi.08.05.201908:45 - 12:00FAV Hörsaal 1 Lecture (Information Flow)
Mi.15.05.201908:45 - 12:00FAV Hörsaal 1 Tutorial (Z3)
Mi.22.05.201908:45 - 12:00FAV Hörsaal 1 Lecture (Bytecode Analysis)
Mi.29.05.201908:45 - 12:00FAV Hörsaal 1 Tutorial (F*)
Mi.05.06.201908:45 - 12:00Seminarraum Argentinierstrasse Formal Methods for Web Security
Mi.12.06.201908:45 - 12:00FAV Hörsaal 1 Backup
Mi.19.06.201908:45 - 12:00FAV Hörsaal 1 Backup
Mi.26.06.201908:45 - 12:00FAV Hörsaal 1 Exam

Leistungsnachweis

Projects and final exam.

 

 

Prüfungen

TagZeitDatumOrtPrüfungsmodusAnmeldefristAnmeldungPrüfung
Mi.08:30 - 12:3025.09.2019FAV Hörsaal 1 schriftlich27.06.2019 10:00 - 24.09.2019 23:59in TISS192.059 Retake Exam

LVA-Anmeldung

Von Bis Abmeldung bis
11.02.2019 13:00 24.03.2019 13:00 24.03.2019 13:00

Curricula

Literatur

Es wird kein Skriptum zur Lehrveranstaltung angeboten.

Vorkenntnisse

Some background in verification and security is ideal, but motivated students with a good background in either of them are also welcome to the course. 

Sprache

Englisch