Please be advised: Due to maintenance at the TU locking system iintegration some errors in this area may occur.. Please accept our apologies for any inconvenience.

192.059 Formal Methods for Security and Privacy
This course is in all assigned curricula part of the STEOP.
This course is in at least 1 assigned curriculum part of the STEOP.

2021S, VU, 4.0h, 6.0EC
TUWEL

Properties

  • Semester hours: 4.0
  • Credits: 6.0
  • Type: VU Lecture and Exercise
  • Format: Distance Learning

Learning outcomes

After successful completion of the course, students are able to develop a static analysis technique for enforcing security and privacy properties in a variety of domains, such as cryptographic protocols, programming languages, and bytecode.

In particular, this course explains the foundations of the static analysis of security and privacy properties, with a particular focus on type systems and SMT solving. Students will learn how to formalize a static analysis, how to prove its soundness, and how to implement it in an efficient way using state-of-the-art verification tools.  

Subject of course

  • Analysis of Cryptographic Protocols via type systems and SMT solving (Applied Pi-Calculus and ProVerif)
  • Language-based Security (Non-Interference, Hyperproperties, and Side Channels)
  • Foundations of Security Static Analysis (Taint Analysis, Symbolic Execution, SMT solving)
  • Static Analysis of Bytecode (Ethereum Smart Contracts)
  • Secure programming in F* 

Teaching methods

The course is based on a combination of lectures and two projects, which provide theoretical foundations as well as hands-on experience with state-of-the-art security verification tools (ProVerif, Z3, F*).

The lectures and tutorials are released in the form of videos and slides on a weekly basis, and they are accompanied by online Q/A (question/answer) sessions. All the lectures, tutorials, and Q/A sessions are recorded and made available online.

Mode of examination

Immanent

Additional information

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

30h lectures, tutorials, exam

40h self-study

80h projects and exercises

---------------------------------------------------
150 hours (6 ECTS)

 

 

Lecturers

Institute

Course dates

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

Examination modalities

Students will be evaluated based on a written exam and projects. 

Course registration

Begin End Deregistration end
15.02.2021 13:00 28.03.2021 14:00 28.03.2021 14:00

Curricula

Literature

No lecture notes are available.

Previous knowledge

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. 

Language

English