IFC

Lectures

Lectures are every week on Wednesday, 10:00 - 12:00 on Zoom and Miro. Class will usually include two 15 mins break. (We start at 10:15).
(https://cispa-de.zoom.us/j/95941144969?pwd=QkI0RWUxY1JJZzZIUlZPMmJSOWpRQT09)
(https://miro.com/app/board/o9J_lxjDkD0=/)

Lecture 1: October 27,
Topics: λ-calculus: syntax, evaluation judgment, type system, type-preservation and progress; security lattice for confidentiality and integrity, simple & labeled types and λ^SFGtype system, L-equivalence for labeled and simple types, non-interference theorem.
Lecture 2: November 3,
Topics: λ-calculus with store and references: syntax, evaluation and type system; implicit flows and program-counter label, λ^SFG typing rules for references.
Lecture 3: November 10,
Topics: λ^SFGpartitioned store, label-annotated syntax, L-equivalence for references, labeled stores and store maps; properties of L-equivalence (reflexivity, symmetricity, transitivity, store square lemma) proof technique for termination-insensitive non-interference: store containment and L-equivalence preservation lemmas.
Lecture 4: November 24,
Topics: Coarse grained IFC, labeled values and MAC security monad, λ^SCG syntax (thunks return, bind, label, unlabel), evaluation (pure, forcing, thunk semantics), type system (no write-down & no read-up rules). Nested computations (toLabeled). Flexible manipulation of labeled values (fmap)., Possibly: Dynamic information flow control

Q&A Session

The Q&A session runs every week on Friday, 10:00 - 12:00 on Zoom and Miro.
(https://cispa-de.zoom.us/j/95941144969?pwd=QkI0RWUxY1JJZzZIUlZPMmJSOWpRQT09)
(https://miro.com/app/board/o9J_lxjDkD0=/)
We will answer questions that pop up on Askbot (see the menu of the course page), even those that appear in anonymous form.
Participation is strongly recommended: DO ask your questions on Askbot: no questions (up until the Q&A session) means no Q&A.

Q&A 1: October 29, https://dl.cispa.de/s/nHGn5ma7dA2WPxK
Q&A 2: November 5, https://dl.cispa.de/s/3TEwDB4XDFPXNGs
Q&A 4: November 26,

Class Material and Recordings

We will use the lecture notes available in the material section.

Recordings for lectures and Q&A can be found here: https://dl.cispa.de/apps/files/?dir=/2021-WS-formal-methods-in-security/IFC&fileid=8376463
For those who do not have access to dl.cispa, here are the individual classes links:

Additional reading material can be found below:

Intro to ifc (overview of class 0, section 1)
Lambda calulus background notes (section 1. disregard lemmas and proofs). Another high-level description of lambda calculus
Static IFC for class 1, 2, 3 (Sections 3.1 and 3.1, they use substitutions instead of \theta but it's the same intuition)
Static IFC #2 for class 1, 2, 3 (Section 3, another slightly different formalisation -- using contextual semantics -- but of the same ideas)
Coarse-grained static IFC for class 4 (Section 3)
Dynamic IFC for class 4 (Section 2)

Assignments

Assignment must be solved, written and submitted individually. You are allowed to discuss the problems with other classmates, but you must not share any solution in written form. Write the answers in English; be clear, precise, and formal. It is recommended to write the answers in LaTeX. Handwritten answers are also acceptable as long as they are legible. Submit your solution in PDF format on CMS (not by email).

Assignments will appear in the course material.

Assignment 1 Deadline (November 5th)
Assignment 2 Deadline (November 19th)
Assignment 3 Deadline (December 3rd)

Solutions will appear in the course materials ~1week after deadline.

Exam

The oral exam is about 30 minutes long and will take place on Thursday December 9th & Friday December 10th.
Locaiton: on Zoom (link in announcements). Book a slot by filling this Doodle.
During the exam, you will have to activate your camera and microphone, identify yourself with a student ID, and be prepared to share your screen if asked to do so. If you have a tablet, you can use that to write your answers to the questions by sharing the screen with me. Otherwise, you can write on a piece of paper and simply show it to the camera. (If you do so, make sure to uncheck the "Mirror my Video" box in Zoom > Preferences > Background & Filters", before the exam starts, please). Since university regulations require to keep a record of oral examinations, the exam will be recorded. The recording will be stored in a private archive until the end of the course and will be deleted afterwards. If you do not want to be recorded, get in touch with the instructor, please.

The exam covers the content of the 4 lectures on IFC (see syllabus above). During the exam, you will answer questions about evaluation and typing rules, theorem definitions and proofs, as well as solve small problems similar to those in the exercise sheets. Your grade will be determined based on three criteria: correctness of the answers, clarity of the explanations, and degree of independence in answering the questions.

Formal Methods in Security

IFC