Description

The description of this lecture can be found on the SIF master webpage.

Teachers

Thomas Jensen (TJ) and Simon Castellan (SC)

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
 14/09/2021 Operational semantics (While)
SC IntroSOS  OpSem1
2 15/09/2021 Operational semantics (References)
SC OpSem2
3 21/09/2021 Lambda-calculus and type systems
SC Types
4 22/09/2021 Information flow analysis
TJ
 Static IF
5
 28/09/2021 Data Flow analysis
TJ Data Flow
6 29/09/2021 Exercise session
TJ Exercises
7
 05/10/2021  Interval analysis and abstract interpretation

Abs Int
8
 06/10/2021 Alias analysis
TJ Alias
9
 12/10/2021 QUIZ
TJ
10
 13/10/2021 Side channel analysis
TJ
 Constant Time
11
 19/10/2021 (preparation of presentations)


12
 20/10/2021 (preparation of presentations)


13
 26/10/2021 (preparation of presentations)


14
 27/10/2021 Question session (by demand)

SC/TJ
15
 02/11/2021 Fall break


16
 03/11/2021 Fall break


17
 09/11/21
 (preparation of presentations)


18
 10/11/21
 Student presentations
SC,TJ


Student presentation projects:

1. Models of low-level concurrent code: https://www.cl.cam.ac.uk/~pes20/weakmemory/x86tso-paper.tphols.pdf
2. Separation logic: Reasoning on imperative programs: https://www0.cs.ucl.ac.uk/staff/p.ohearn/papers/localreasoning.pdf
  Informal description: https://dl.acm.org/doi/pdf/10.1145/3211968
3. The  mechanical  evaluation  of  expressions (1966 !!)   https://www.cs.cmu.edu/~crary/819-f09/Landin64.pdf
4. Flow-sensitive information flow analysis. 
5. The Java byte code verifier.
6. Taint analysis (dynamic information flow analysis)
7. Static analysis of binary code.
8. System-level constant-time analysis