TU Wien:Formal Methods for Security and Privacy VU (Maffei)
Daten[edit]
| Lecturers | Simon Jeanteur• Matteo Maffei |
|---|---|
| ECTS | 6 |
| Alias | Formal Methods for Security and Privacy (en) |
| Department | Logic and Computation |
| When | summer semester |
| Last iteration | 2022SS |
| Language | English |
| Mattermost | formal-methods-for-security-and-privacy • Register • Mattermost-Infos |
| Links | tiss:192059 |
Inhalt[edit]
- 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[edit]
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[edit]
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[edit]
noch offen
Übungen[edit]
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[edit]
- 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[edit]
| Semester | Letzte Leistung | Zeugnis | |
|---|---|---|---|
| SS21 | 2021-07-09 |
Zeitaufwand[edit]
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[edit]
Tipps[edit]
- 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
Verbesserungsvorschläge / Kritik[edit]
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.