Below, the list of topics to covert in the course. For each subject, there is a link to the corresponding slides.
Introduction
Access Control and Information-Flow Control
Organization of the course
Introduction to Haskell
The IO Monad
IO
Why Haskell? Why Monads?
Running example
The security monad MAC
The join operator
join
Classifying dangerous flows
Covert channels
Concurrency
Internal timing covert channel
Cache attacks
Attacks via lazy evaluation
Formal guarantees
Proof technique
Core calculus
Erasure function
Proving commutability
Two-steps erasure
Progress-insensitive non-interference
Scheduler
Progress-sensitive non-interference
Summary of the course