Description
The description of this lecture can be found on the SIF master webpage.Teachers
Thomas Jensen (TJ) and Simon Castellan (SC)Guest lecture by Benjamin Farinier (BF)
Evaluation
A quiz (exam) on the first part of the course and student presentations (groups of two) of articles from the research literature.Exam SOS from 2017
Planning, lecture notes
| Lecture | Date | Topic | Teacher | Handout |
|---|---|---|---|---|
| 1 |
12/09/2022 | Dataflow analysis | TJ |
Dataflow analysis |
| 2 | 13/09/2022 | Dataflow analysis |
TJ | Bonus: Java byte code verification |
| 3 | 19/09/2022 | Operational semantics | SC | Slides |
| 4 | 20/09/2022 | Operational semantics |
SC |
Slides |
| 26/09/2022 | Lambda-calculus and type systems | SC |
Slides | |
| 5 |
27/09/2022 | Abstract interpretation |
TJ |
Abs Int slides |
| 6 |
03/10/2022 | Information flow analysis | TJ | Static inf flow |
| 7 | 04/10/2022 | Information flow analysis | TJ | Inf flow challenge |
| 8 | 10/10/2022 | |||
| 9 | 11/10/2022 | QUIZ | SC,TJ |
|
| 10 |
17/10/2022 | Symbolic execution | BF |
|
| 11 |
18/10/2022 | Preparation of student presentations | |
|
| 12 |
24/10/2022 | Preparation of student presentations |
|
|
| 13 |
25/10/2022 | Student presentations | SC,TJ | |
| 14 |
31/10/2022 | Fall break |
||
| 15 |
01/11/2022 | Fall break |
||
| 16 |
07/11/2022 |
Student presentations:
- Models of low-level code: A Better x86 Memory Model: x86-TSO (Owens, Sarkar, Sewell)
- Separation logic: Local Reasoning about Programs that Alter Data Structures (O'Hearn, Reynolds, Yang) (Informal description of separation logic)
- Logical Relations for Encryption (Sumii, Pierce)
- On flow-sensitive Security Types (Hunt, Sands)
- System-level non-interference for constant-time cryptography (Barthe et al.)
- Precise static analysis of untrusted driver binaries (Kinder, Veith)