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.
Torben Amtoft
Anindya Banerjee