IFC
Lectures
Lectures are every week on Wednesday, 10:00 - 12:00 on Zoom. (We start at 10:00 sharp).
- Lecture 1: November 4, [zoom] [video] [slides] [notes].
Topics: λ-calculus: syntax, evaluation judgment, type system, type-preservation and progress; security lattice for confidentiality and integrity, simple & labeled types and λSFG type system, L-equivalence for labeled and simple types, non-interference theorem. - Lecture 2: November 11, [zoom] [video] [slides] [notes].
Topics: λ-calculus with store and references: syntax, evaluation and type system; implicit flows and program-counter label, λSFG typing rules for references. - Extra Lecture: November 11, [video] [notes]
- Lecture 3: November 18, [zoom] [video] [no slides] [notes].
Topics: λSFG partitioned 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 25, [zoom] [video] [no slides] [notes].
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).
All the video recordings of the lectures are available here.
Q&A Session
The Q&A session runs every week on Friday, 10:00 - 12:00 on Zoom. (We start at 10:00 sharp).
- Q&A 1: November 6, [zoom] [video] [notes].
- Q&A 2: November 13, [zoom] [video] [notes].
- Q&A 3: November 20, [zoom] [video] [notes].
- Q&A 4: November 27, [zoom] [video] [notes].
- Final Q&A: December 1, 14:00 - 16:00, [zoom] [videos] [notes]
All the video recordings of the Q&A sessions are available here.
Besides answering questions about the content of the lectures, during the Q&A sessions we will also solve exercises together.
Participation is strongly recommended.
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).
Assignment List:
- Assignment 1,
Deadline: November 13, 23:59, Solution - Assignment 2,
Deadline: November 24, 23:59, Solution - Assignment 3,
Deadline: December 6, 23:59, Solution
Exam
The oral exam is about 30 minutes long and will take place on December 3 and December 4, on Zoom. 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.
Zoom links for the oral exams:
- Thursday afternoon, December 3: Zoom
- Friday morning, December 4: Zoom
- Friday afternoon, December 4: Zoom
You are welcome to join the final Q&A session on December 1, from 14 to 16 on Zoom to ask questions about all the topics of the course. During this session, we can also simulate an oral examination in preparation for the exam, where I ask exam-like questions and students try to answer and receive immediate feedback.
Rocket Chat
In addition to the Q&A sessions, you can also ask questions on the Rocket Chat channel #ifc (password: non-interference).