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.

2018S, VU, 4.0h, 6.0EC, wird geblockt abgehalten

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 analysis of security and privacy properties in
cryptographic protocols and programming languages.

For instance, students will study and have hands-on experience on F*,
a programming language for verification that has been recently used to
program the first verified TLS 1.3 implementation as well as the
cryptographic libraries embedded in Firefox, 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, Predicate Abstraction)
- Formal Security Analysis of Bytecode (Android, Ethereum Virtual Machine)

Weitere Informationen

ECTS Breakdown:

30h lectures, tutorials, exam

40h self-study

80h projects and exercises

Additional Info:

The study committee will discuss on March 14th the approval of this lecture (with validity already in the current term) as a regular course in the following master programs:

  • Logic and Computation
  • Software Engineering & Internet Computing
  • Technische Informatik
  • Computational Logic

Students will be promtly notified about the decision. 

Vortragende

Mitwirkende

Institut

LVA Termine

TagZeitDatumOrtBeschreibung
08:30 - 10:0016.05.2018 - 08.06.2018Seminarraum FAV EG C (Seminarraum Gödel) Lecture/Tutorial
Mo.08:30 - 10:0011.06.2018Seminarraum FAV EG C (Seminarraum Gödel) Lecture/Tutorial
Di.14:00 - 17:0026.06.2018EI 10 Fritz Paschke HS 192.059 Final Exam
Formal Methods for Security and Privacy - Einzeltermine
TagDatumZeitOrtBeschreibung
Mi.16.05.201808:30 - 10:00Seminarraum FAV EG C (Seminarraum Gödel) Lecture/Tutorial
Do.17.05.201808:30 - 10:00Seminarraum FAV EG C (Seminarraum Gödel) Lecture/Tutorial
Fr.18.05.201808:30 - 10:00Seminarraum FAV EG C (Seminarraum Gödel) Lecture/Tutorial
Mi.23.05.201808:30 - 10:00Seminarraum FAV EG C (Seminarraum Gödel) Lecture/Tutorial
Do.24.05.201808:30 - 10:00Seminarraum FAV EG C (Seminarraum Gödel) Lecture/Tutorial
Fr.25.05.201808:30 - 10:00Seminarraum FAV EG C (Seminarraum Gödel) Lecture/Tutorial
Mo.28.05.201808:30 - 10:00Seminarraum FAV EG C (Seminarraum Gödel) Lecture/Tutorial
Di.29.05.201808:30 - 10:00Seminarraum FAV EG C (Seminarraum Gödel) Lecture/Tutorial
Mi.30.05.201808:30 - 10:00Seminarraum FAV EG C (Seminarraum Gödel) Lecture/Tutorial
Fr.01.06.201808:30 - 10:00Seminarraum FAV EG C (Seminarraum Gödel) Lecture/Tutorial
Mo.04.06.201808:30 - 10:00Seminarraum FAV EG C (Seminarraum Gödel) Lecture/Tutorial
Di.05.06.201808:30 - 10:00Seminarraum FAV EG C (Seminarraum Gödel) Lecture/Tutorial
Mi.06.06.201808:30 - 10:00Seminarraum FAV EG C (Seminarraum Gödel) Lecture/Tutorial
Do.07.06.201808:30 - 10:00Seminarraum FAV EG C (Seminarraum Gödel) Lecture/Tutorial
Fr.08.06.201808:30 - 10:00Seminarraum FAV EG C (Seminarraum Gödel) Lecture/Tutorial
Mo.11.06.201808:30 - 10:00Seminarraum FAV EG C (Seminarraum Gödel) Lecture/Tutorial
Di.26.06.201814:00 - 17:00EI 10 Fritz Paschke HS 192.059 Final Exam
LVA wird geblockt abgehalten

Leistungsnachweis

Projects and final exam.

 

 

Prüfungen

TagZeitDatumOrtPrüfungsmodusAnmeldefristAnmeldungPrüfung
Mi.09:00 - 12:0001.07.2020FAV Hörsaal 1 schriftlich10.05.2020 09:00 - 28.06.2020 12:00in TISSFinal Exam
Mi.09:00 - 13:0023.09.2020FAV Hörsaal 1 schriftlich25.06.2020 10:00 - 22.09.2020 16:00in TISSRetake Final Exam

LVA-Anmeldung

Von Bis Abmeldung bis
01.03.2018 13:00 29.04.2018 13:00 29.04.2018 13:00

Anmeldemodalitäten:

Please send your registration request to christopher.vomastek@tuwien.ac.at. We will notify you about your registration request by April 29. 

Die Anmeldung ist derzeit manuell gesperrt

Curricula

Literatur

Es wird kein Skriptum zur Lehrveranstaltung angeboten.

Vorkenntnisse

Some background in verification and security is ideal, but motivated students without this background are also welcome to the course. However, we would expect some more spirited efforts from you.

Sprache

Englisch