TU Wien:Formal Methods for Security and Privacy VU (Maffei)
Daten[Bearbeiten | Quelltext bearbeiten]
| Vortragende | Anagha Athavale• Matteo Maffei |
|---|---|
| ECTS | 6,0 |
| Letzte Abhaltung | 2024S |
| Sprache | English |
| Mattermost | formal-methods-for-security-and-privacy • Register • Mattermost-Infos |
| Links | tiss:192059, eLearning |
Inhalt[Bearbeiten | Quelltext bearbeiten]
- Cryptographic Protocols (Needham-Schröder, Proverif, Spi-Calculus, Observational Equivalence)
- Bana-Comon Logic
- Information Flow Control (Side Channels, Implicit/Explicit Flow, Termination Channels, Timing Channels, Probabilistic Channels, Non-Interference)
- Static Analysis (Ethereum Smart Contracts, EVM Bytecode)
Ablauf[Bearbeiten | Quelltext bearbeiten]
Seven lectures are held throughout the semester, all of which have been prerecorded and are uploaded over the course of the semester. After each block there is the possibility to attend a live Q&A session with Prof. Maffei.
For the first three lectures there are three exercise sheets which can be solved for additional practice. The Q&A session is intended for students who have questions regarding these exercise sheets. It is possible to ask different questions as well.
Starting from end of March, the first project (Proverif) is put online. Students usually have two weeks to one month to do each project.
At the end of the semester there is a 3h exam taking place either online via a Zoom session or in person.
Benötigte/Empfehlenswerte Vorkenntnisse[Bearbeiten | Quelltext bearbeiten]
Interest in and a basic understanding of cryptography is a must, IMO. Students who like to do small proofs will have it much easier for certain topics. I suggest having taken TIL and/or EWBS, because it helped me deal with the type-checking part. For the Static Analysis part it makes sense to already have a good understanding of how Ethereum works. Students who know common vulnerabilities (eg. Reentrancy Attacks) of Smart Contracts (as taught in the course Smart Contracts) will have it easier to understand the last project.
Vortrag[Bearbeiten | Quelltext bearbeiten]
noch offen
Übungen[Bearbeiten | Quelltext bearbeiten]
Sind in Gruppen von 1-3 Personen zu erledigen, 3 Projekte - je mit ProVerif, F* und Z3.
Do not underestimate the amount of work required to get the three projects done! I could not find a group to do the projects with and ended up doing them on my own. I do not recommend this approach at all!
Prüfung, Benotung[Bearbeiten | Quelltext bearbeiten]
- Benotung ergibt sich aus den Übungsprojekten sowie einer schriftlichen Prüfung am Schluss ("Final exam").
- Für die Prüfung hat man 2,5 Stunden Zeit, im Juni 2018 bestand die Prüfung aus 4 Teilen (Themengebiete jeweils die großen Themen der Vorlesung also "Cryptographic protocols", "Observational equivalence", "Information flow control" und "Static analysis") wobei kein reines Theoriewissen abgefragt wurde sondern man musste sein Verständniswissen auf Beispiele anwenden und das erklären. Bei 1 oder 2 Aufgaben wurde auch nach Beweisen gefragt.
- SS 2020: Due to COVID-measures the exam was handed out via TUWEL and had to be uploaded within 3 hours, all course materials could be used but communication with other students was strictly prohibited. To ensure that answers were not copied from other people short video calls took place the day after the exam during which a selection of answers had to be explained.
- SS 2021: Same as SS 2020, but no video calls the next day. Instead, all participants had to be connected to a Zoom session for the whole 3 hours. All material could be used, but communication between students was prohibited.
Dauer der Zeugnisausstellung[Bearbeiten | Quelltext bearbeiten]
| Semester | Letzte Leistung | Zeugnis | |
|---|---|---|---|
| SS21 | 2021-07-09 |
Zeitaufwand[Bearbeiten | Quelltext bearbeiten]
Depending on the amount of existing knowledge and your affinity for everything theoretical, I would say the time required ranges from around 100h (students who like theoretical computer science topics and have a good group to do the projects with) to about 175h or more.
If you do the projects on your own, the time required could very well exceed 200h.
Unterlagen[Bearbeiten | Quelltext bearbeiten]
Tipps[Bearbeiten | Quelltext bearbeiten]
- Get a good group
- Start early with the projects
- Solve the optional exercises (you will need it for the exam)
- Ask questions during the Q&A sessions
- Make sure that you are able to type-check a process from sleep, so that there is enough time for all the other exercises during the exam
Highlights / Lob[Bearbeiten | Quelltext bearbeiten]
noch offen
Verbesserungsvorschläge / Kritik[Bearbeiten | Quelltext bearbeiten]
(2022SS) My main critique is in regards to the didactic style of the lecture. It is unfortunately an extremely confusing and incomprehensible regurgitation of Maffei's paper. His lecturing style is also very odd as he will often present a new and unintuitive subject theoretically and when you think he's about to present a practical example he breaks off with a "As an exercise you can do this yourself". This happens a lot. Definitions are usually prefaced with a "... as in Table (n)" where "Table (n)" is not part of the presentation. You are then however also tasked to read the corresponding chapter in the book. The lecture at no point tells you what book that is, as there are zero literature references. Nomenclature is introduced seemingly at will and sometimes not even the source paper cares to explain what it means. Looking at you img(Gamma). What does it mean? Hopefully nothing important! Anyway, the lecture would greatly benefit from doubling the speaking time of the lecturer and not just blasting through the absolute heaps of symbol salad and hoping that people just figure it out.
In 2021SS the last two projects had to be done in a short amount of time at the end of the semester where there are usually other exams. I saw no good reason for this and thus would suggest putting the project descriptions online as soon as possible.
In 2018SS the lecture and exercises lasted well into the holidays, and the exam lasted 3 hours, but the time was insufficient for most, so the exam was extended to 3.5 hours.