Difference between revisions of "TU Wien:Formal Methods for Security and Privacy VU (Maffei)"
| Line 1: | Line 1: | ||
== Daten == | == Daten == | ||
{{LVA-Daten | {{LVA-Daten | ||
| − | |ects=6 | + | | ects = 6 |
| − | |vortragende=[ | + | | vortragende = [[tiss.person:306636|Matteo Maffei]], [[tiss.person:308337|Clara Schneidewind]] |
| − | |id=192059 | + | | abteilung = Logic and Computation |
| − | |wann=SS | + | | id = 192059 |
| − | |sprache=en | + | | wann = SS |
| − | |zuordnungen= | + | | sprache = en |
| + | | zuordnungen = | ||
{{Zuordnung|E066931|Programming Languages and Verification|wahl=1}} | {{Zuordnung|E066931|Programming Languages and Verification|wahl=1}} | ||
{{Zuordnung|E066937|Advanced Security|wahl=1}} | {{Zuordnung|E066937|Advanced Security|wahl=1}} | ||
Revision as of 12:20, 5 July 2020
Daten
| Lecturers | Matteo Maffei, Clara Schneidewind |
|---|---|
| ECTS | 6 |
| Department | Logic and Computation |
| When | summer semester |
| Language | English |
| Links | tiss:192059 , Mattermost-Channel |
Mattermost: Channel "formal-methods-for-security-and-privacy" • Register • Mattermost-Infos
Inhalt
noch offen, bitte nicht von TISS oder Homepage kopieren, sondern aus Studierendensicht beschreiben.
Ablauf
noch offen
Benötigte/Empfehlenswerte Vorkenntnisse
noch offen
Vortrag
noch offen
Übungen
Sind in Gruppen von 1-3 Personen zu erledigen, 3 Projekte - je mit ProVerif, F* und Z3.
Prüfung, Benotung
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.
- Summer term 2020: Exam at the beginning of July consisted of four parts: Typing for Cryptographic Protocols (30 points, 3 exercises: Does a given process hold secrecy/integrity, give a type derivation if yes or a counter-example if not; find an appropriate type instantiation for a given process; show the incompleteness of the given type system by example of a process that preserves secrecy and integrity but does not type check), Protocol Analysis (20 points, 2 exercises: Does a given protocol satisfy (non-)injective agreement, if not describe an attack and propose a minimal modification to fix it; give an intuitive explanation why two protocols do or do not hold injective agreement or show an attack), Information Flow (20 points, 2 exercises: Prove incompleteness of the given type system for non-interference by counterexample; give a type derivation for a given program or show why it fails), Static Analysis (30 points, 2 exercises: show all intermediate and final configurations of a short program given small-step semantics; for three different abstractions argue whether the given soundness claim holds and give example programs). 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.
Dauer der Zeugnisausstellung
noch offen
Zeitaufwand
noch offen
Unterlagen
noch offen
Tipps
noch offen
Verbesserungsvorschläge / Kritik
noch offen