Captains' Log: Language Based Security, Fall 2003

Wed August 20

Introduction to course. Brief Motivation followed by presentation of A Language-Based Approach to Security

Mon August 25

Amtoft: Part I (pages 1--27) of Walker's Presentation of Typed Assembly Language.

Wed August 27

Amtoft proved the auxiliary results (admissibility, canonical form) needed to establish type safety of the "vanilla" system presented last Monday.

Mon September 1

Student/University holiday

Wed September 3

Amtoft finished the proof of type safety for the TAL-0 system in Walker's Presentation of Typed Assembly Language, covered the TAL-1 system featuring polymorphism (pages 28--36), and embarked on the TAL-2 system featuring stacks (pages 38--43).

Mon September 8

Amtoft continued Walker's Presentation of Typed Assembly Language, finishing the TAL-2 system featuring stacks (pages 38--52) and also covering Type-Directed Compilation (pages 54--76).

Wed September 10

Amtoft started on Proof-Carrying Code, covering Necula's Presentation (here in postscript) and also listing the symbolic evaluator from Table 3 in Necula & Lee: Safe, Untrusted Agents using Proof-Carrying Code.

Mon September 15

Amtoft presented more example applications of Proof-Carrying Code, such as those found in Kedar's presentation (given in Walker's course on language-based security) and also the list sum program (adapted from George C. Necula: Proof-carrying code) where we generated the safety theorem using the "weakest precondition" method as well as using the "strongest postcondition" method. By incorporating time resources in the invariants, one can reason about termination; we discussed some of the pitfalls of that approach.
For a reading guide to Proof-Carrying Code (cf. our reading list), see Necula's annotated bibliography (though not up-to-date).

Wed September 17

Banerjee started on Information Flow Analysis, with a presentation based on Andrei Sabelfeld and Andrew C. Myers: Language-based Information-Flow Security.

Mon September 22

Banerjee continued Information Flow Analysis, proving (on the board) the non-interference property for while-loops.

Wed September 24

Banerjee presented a semantics and a type system for a Java-like language, using pages 1--25 of these slides.

Mon September 29

Motivated by the desire to prevent certain information leaks, Banerjee augmented the type system for a Java-like language with security levels, using pages 26--40 of these slides.
Background reading: Volpano & Smith: A Type-Based Approach to Program Security.

Wed October 1

No class (Banerjee in Germany)

Mon October 6

No class (Amtoft & Banerjee in Germany for a Dagstuhl seminar on language based security)

Wed October 8

No class (Amtoft & Banerjee in Germany for a Dagstuhl seminar on language based security)

Mon October 13

Student holiday

Wed October 15

Presentation by Banerjee on Banerjee & Naumann: Stack-based Access Control for Secure Information Flow.

Mon October 20

Gurvan Le Guernic presented the work by Andrew Myers and others on DLM, in particular A Decentralized Model for Information Flow Control and Complete, Safe Information Flow with Decentralized Labels.

Wed October 22

Gurvan continued his presentation.

Mon October 27

Sruthi Bandhakavi presents Bieber et al: Checking Secure Interactions of Smart Card Applets: extended version (a preliminary version is available here)

Wed October 29

Sruthi continued her presentation.

Mon November 3

Presentation by Georg Jung of Darvas & Hähnle & Sands: A Theorem Proving Approach to Analysis of Secure Information Flow.

Wed November 5

Georg Jung continues his presentation (also discussing some inference rules from Beckert: A Dynamic Logic for the Formal Verification of Java Card Programs).

Mon November 10

Presentation by Nithya Raveendran of Xavier Leroy: Bytecode verification on Java smart cards.

Wed November 12

Nithya Raveendran continued her presentation.

Mon November 17

Gurvan outlined his proposed project.

Wed November 19

Georg outlined his proposed project.

Mon November 24

Nithya and Sruthi gave a demo showing their experience with Coq, the tool to be used in both their projects.

Wed November 26

Student holiday

Week from December 1 to December 5

No classes; the students should work on their projects and when needed schedule one-on-one meetings with instructors.

Mon December 8

Student reports in