Captains' Log: Language Based Security, Fall 2004

August 31

Introduction to course: Banerjee presented Andrei Sabelfeld's slides from the recent Dagstuhl seminar on Language-Based Information-Flow Security.

September 7

Banerjee presented a type system for information-flow analysis for a simple imperative language, along the way proving on the board "read confinement" and "write confinement".
For next time: see if you can prove the Noninterference Theorem yourself!
Background reading: Volpano & Smith's A Type-Based Approach to Program Security.

September 14

Students went through some of the cases in the inductive proof of the Non-interference Theorem. Then Banerjee continued his presentation of a type system for information-flow analysis for a simple imperative language, extending it with a loop construct which calls for more advanced proof techniques.

September 21

Amtoft starts the presentation of Noninterference for concurrent programs and thread systems by Gérard Boudol and Ilaria Castellani: after a motivating example, the type system (from Sect. 2) is presented; then (as a preparation to the proof of non-interference) we show "subject reduction" (Theorem 3.1) and that an "L-guarded" program evolves independently of its high variables (Lemma 3.13).

September 28

Amtoft continues his presentation of the Boudol & Castellani paper, finishing the correctness proof (Sect. 3) for the system from Sect. 2: after motivating various notions of bisimulation, the stage is set for the proof of Sequential Noninterference (Theorem 3.15) and Concurrent Noninterference (Theorem 3.16).

October 5

Amtoft finishes his presentation of the Boudol & Castellani paper, covering Section 4. (See here for the key definitions of that paper.)
Banerjee starts the presentation of his and David Naumann's paper Stack-based Access Control and Secure Information Flow: after a motivation, he covered the first 8 pages of these slides.

October 12

No class (student holiday)

October 19

Banerjee continues the presentation of his and Naumann's paper, covering pages 9--39 of these slides.

October 21 (1pm)

Banerjee finishes the presentation of his and Naumann's paper, by stating the correctness of the information flow analysis, and showing how to integrate the analysis with stack-based access control.

October 26

Edwin Rodriguez presents Information Flow Analysis in Logical Form by Amtoft & Banerjee.

November 2

Class cancelled, since Amtoft and Banerjee are both out of town (unrelated to the election!)

November 4 (1pm)

Edwin Rodriguez finishes his presentation from last week (covering the "frame rule").
Sanghamitra Das starts her presentation of Using Replication and Partitioning to Build Secure Distributed Systems by Lantian Zheng et al.

November 9

Sanghamitra Das finishes her presentation of Using Replication and Partitioning to Build Secure Distributed Systems by Lantian Zheng et al.

November 16

Sanjeev U.N. presents Type-Based Distributed Access Control by Chothia & and Duggan & Vitek.

November 18 (1pm)

Edwin Rodriguez outlines his project proposal.

November 23

Sanghamitra Das outlines her project proposal.
Sanjeev U.N. outlines his project proposal.

November 30

Edwin Rodriguez presents the final report for his project: A Characterization of Secure Information Flow in Location Based Access Control - and Something More

December 3 (11:30am, in the library)

Sanghamitra Das reports on her project.
Sanjeev U.N. reports on his project.