Schedule

(Open to change at any time)

bulletWeek 1: Introduction & principles of systems security
bulletMonday September 13th
bulletIntroduction (Course & Project Notes)
bulletWednesday September 15th
bulletLecture notes (Security Intro)
bulletRead The Protection of Information in Computer Systems. Saltzer and Schroeder, Section I,A.  Do these principles still apply today?  Which do which don't?  Are there missing principles we need to be aware of?  Are there more specific principles that apply to systems written in modern programming languages such as Java?  Are there modern systems where we need to take additional precautions?  Consider additional properties? (Use your experience from PlanetLab?) 
bulletRead Exterminate all operating system abstractions. Dawson R. Engler and M. Frans Kaashoek.  What is the difference between what the ExoKernel means by "secure" and what an ordinary operating system means by "secure"?  What security principles does the ExoKernel abide by or not abide by?  Are these choices good or bad?  Is the ExoKernel more reliable than other operating systems?  Think of your own controversial question to ask the class.  Come up with an interesting position to defend in class.  Be ready to discuss. 
 
bulletWeek 2: Security properties
bulletMonday September 20th:  Review of programming languages concepts
bulletsyntax
bulletoperational semantics
bullettype systems
bulletRead  Benjamin Pierce, Types and Programming Languages.  chapters 1-9.
bulletWednesday September 22nd:
bulletSafety and liveness: from set theory to Buchi automata
bulletRead Recognizing Safety and Liveness.  Bowen Alpern and Fred Schneider
bulletRead Enforceable Security Policies.  Fred Schneider. 
bulletWeek 3: Program monitoring languages
bulletMonday September 27th:  Security monitors continued.
bulletWednesday September 29th:  Implementing security monitors
bulletRead Flexible Policy-Directed Code Safety.  David Evans and Andrew Twyman.
bulletOR IRM Enforcement of Java Stack Inspection.  Úlfar Erlingsson and Fred Schneider.
bulletWeek 4: Program monitors as execution transformers
bulletMonday October 4th: Edit automata.
bulletRead Edit Automata: Enforcement Mechanisms for Run-time Security Policies.  Jarred Ligatti, Lujo Bauer, and David Walker
bulletLecture Notes (Security Monitors)
bulletWednesday October 6th:  Language-theoretic semantics for program monitors
bulletRead A theory of aspects.  David Walker, Steve Zdancewic and Jay Ligatti.
bulletWeek 5: Java security
bulletMonday October 11th:  Lecture Cancelled
bulletWednesday October 13th:  Java security:  Permissions, stack inspection, class loaders and all that jazz
bullet

Lecture Notes (Java Security)

bullet

Read Stack Inspection: Theory and Variants.  Cédric Fournet and Andrew Gordon

bulletWeek 6: Formalizing Stack Inspection
bulletMonday October 18th:  Equational reasoning about stack inspection
bulletLecture Notes (Java Security2)
bulletRead Stack Inspection: Theory and Variants.  Cédric Fournet and Andrew Gordon
bulletWednesday October 20th:  A Type System for reasoning about stack inspection.
bulletLecture Notes (Java Security3)

 

bulletFALL BREAK

 

bulletWeek 7: Static access control via types
bulletMonday November 1st:  Type Qualifiers Intro
bulletLecture Notes (CQual)
bulletWednesday November 3rd:  Security via Type Qualifiers
bulletContinue Monday's lecture
bulletRead Chapter 3, Type Qualifiers: Lightweight Specifications to Improve Software Quality
Jeffrey S. Foster. Ph.D. thesis, University of California, Berkeley, December 2002.
bulletRead Detecting Format-String Vulnerabilities with Type Qualifiers
Umesh Shankar, Kunal Talwar, Jeffrey S. Foster, and David Wagner. In 10th USENIX Security Symposium, August 2001.
bulletFriday November 5th (10:30 AM; CS 401 Make-up Lecture):  Flow-sensitive type analysis.
bulletRead Enforcing High-level Protocols in Low-level Software.  Rob DeLine and Manuel Fahndrich.  PLDI 2001.
bulletWeek 8: Secrecy, integrity and information flow control
bulletMonday November 8th:  Information flow basics
bulletWednesday November 10th: Information flow type systems
bulletRead Information Flow for ML.  Francois Pottier and Vincent Simonet. TOPLAS 2004.
bulletWeek 9: Information flow overflow & analysis of cryptographic protocols
bulletMonday November 15:  Non-interference proofs
bulletRead Information Flow for ML.  Francois Pottier and Vincent Simonet. TOPLAS 2004.
bulletWednesday November 17:  Cryptographic protocols
bulletCryptic:  Analyzing cryptographic protocols via type checking
bulletRead Authenticity by typing for security protocols.  Andrew Gordon and Alan Jeffrey.
bulletWeek 10: Cryptographic protocols continued; Logic and Access control
bulletMonday November 22:  Cryptic continued.
bulletRead Authenticity by typing for security protocols.  Andrew Gordon and Alan Jeffrey.
bulletWednesday November 24:  Binder (Sudhakar Govindavajhala presents)
bulletRead Binder: a logic-based security language.  John DeTreville.
bulletWeek 11: Logic and Access Control
bulletMonday November 29: Says and Speaksfor Logics
bullet A Calculus for Access Control in Distributed Systems.  Abadi et al.
bullet Understanding Java Stack Inspection.  Wallach and Felten.
bullet A General and Flexible Access Control System for the Web.  Bauer et al.
bulletWednesday December 1:  Model Checking for security
bulletHao Chen and David Wagner. MOPS: an Infrastructure for Examining Security Properties of Software. ACM Conference on Computer and Communications Security (CCS), 2002
bulletWeek 12: Project presentations
bulletMonday December 6:  William & Harlan
bulletWednesday December 8:  Mike & Aquinas