CMSC 838Z Spring 2005

Language-Based Security

Schedule

Here is the review form you should use to review each paper (unless marked below as not for review). Please submit your reviews to

. The order that we go through papers, and which others to read, will be based on class interest.

Date	Topic	Papers	Notes, Supplementary Papers
1/31	Motivation and Overview	- Bershad, Savage, Pardyak, Becker, Fiuczynski, and Gun Sirer, Protection is a Software Issue (review highlights) - McGraw and Morrisett, Attacking Malicious Code: A Report to the Infosec Research Council - Morrisett, Harper, Schneider, A Language-Based Approach to Security
2/2	Security Foundations	- Saltzer and Schroeder, Protection of Information in Computer Systems - Denning and Denning, Data Security
2/7	Reference Monitors	- Wahbe, Lucco, Anderson, and Graham, Efficient, Software-based Fault Isolation - Erlingsson and Schneider, SASI Enforcement of Security Policies, A Retrospective	- Discussion Summary (McCann) - Small, MiSFIT: A Tool For Constructing Safe Extensible C++ Systems - Erlingsson and Schneider, IRM enforcement of Java stack inspection
2/9	Reference Monitors	Hamlen, Morrisett, and Schneider, Computability Classes for Enforcement Mechanisms	Lecture notes (Hicks)
2/14	Applications	- Bershad, Savage, Pardyak, Sirer, Fiuczynski, Becker. Eggers, and Chambers, Extensibility, Safety and Performance in the SPIN Operating System (review highlights) - Chen, Ng, Chadra, Aycock, Rajamani, and Lowell, The Rio file cache: surviving operating system crashes (review highlights) - Swift, Bershad, and Levy, Improving the Reliability of Commodity Operating Systems (review highlights)	Lecture notes (Hicks)
2/16,2/21,2/23	Typed Assembly Language	Morrisett, Typed Assembly Language taken from Pierce's Advanced Topics in Types and Programming Languages (do not distribute)	- Discussion 1 summary (Jackson) - Discussion 2 summary (Fraser) - Discussion 3 summary (Wo)
3/2,3/7,3/9	Proof Carrying Code	Necula, Proof-Carrying Code (with solutions to selected exercises) taken from Pierce's Advanced Topics in Types and Programming Languages (do not distribute)	- Discussion 1 summary (Troche) - Discussion 2 summary (Srivastava)
3/14	Proof Carrying Code	- Sekar, Venkatakrishnan, Basu, Bhatkar, and DuVarney, Model-Carrying Code: A Practical Approach for Safe Execution of Untrusted Applications - Appel, Foundational Proof-Carrying Code
3/16	Information Flow Control	Sabelfeld and Myers, Language-Based Information-Flow Security	- Denning, A Lattice Model of Secure Information Flow - Denning and Denning, Certification of Programs for Secure Information Flow - Goguen and Messguer, Security policies and security models - Volpano, Smith, and Irvine, A Sound Type System for Secure Flow Analysis
3/28		- Zdancewic, Zheng, Nystrom, and Myers. Untrusted Hosts and Confidentiality: Secure Program Partitioning - Zheng, Chong, Zdancewic, and Myers. Building Secure Distributed Systems Using Replication and Partitioning
3/30		Vachharajani, Bridges, Chang, Rangan, Ottoni, Blome, Reis, Vachharajani, and August, RIFLE: An Architectural Framework for User-Centric Information-Flow Security	Tse and Zdancewic, Run-time Principals in Information-flow Type Systems
4/4	Static Analysis	- Wagner, Foster, Brewer, and Aiken, A First Step Towards Automated Detection of Buffer Overrun Vulnerabilities - Chen and Wagner, MOPS: an Infrastructure for Examining Security Properties of Software
4/6		- Ashcraft and Engler, Using Programmer-Written Compiler Extensions to Catch Security Holes - Yang, Kremenek, Xie, and Engler, MECA: an Extensible, Expressive System and Language for Statically Checking Security Properties	Metacompilation home page
4/11		- Johnson and Wagner, Finding User/Kernel Pointer Bugs With Type Inference - Zhang, Edwards and Jaeger, Using CQUAL for Static Analysis of Authorization Hook Placement	CQual homepage
4/13		- Viega, Bloch, Kohno, and McGraw, ITS4: A Static Vulnerability Scanner for C and C++ Code - Wagner and Dean, Intrusion Detection via Static Analysis
4/15	Grab Bag	- Bauer, Ligatti and Walker, Composing Security Policies in Polymer - Gopalakrishna, Spafford and Vitek, Efficient Intrusion Detection using Automaton Inlining
4/20	Student Presentations	- (Gary Jackson presents) Bishop and Dilger, Checking for Race Conditions in File Accesses (slides) - (Morgan Kleene presents) Chothia, Duggan, and Vitek, Type-based Distributed Access Control (slides)
4/25		- (Nicholas Tsz Wo presents) Clarke, Emerson, and Sistla, Automatic Verification of Finite-State Concurrent Systems Using Temporal Logic Specifications - (Tim Fraser presents) Myers, Sabelfeld, and Zdancewic, Enforcing Robust Declassification (slides)
5/2		- (Justin McCann presents) Abadi, Secrecy by Typing for Security Protocols - (Saurabh Srivistava presents) Gordon and Jeffrey, Authenticity by Typing for Security Protocols (slides)
5/4		- (Jose Troche presents) Zitser, Leek and Lippman, Testing Static Analysis Tools Using Exploitable Buffer Overflows From Open Source Code (slides) - (Nick Petroni presents) Baratloo, Singh, Tsai, Transparent Run-Time Defense Against Stack Smashing Attacks and Avijit, Gupta, Gupta, TIED, LibsafePlus: Tools for Runtime Buffer Overflow Protection (slides)
5/4	Project Presentations	Tim Fraser
5/9		Justin McCann Saurabh Srivistava Jose Troche
5/11		Morgan Kleene Gary Jackson Nicholas Tsz Wo

Unscheduled Papers

Reference Monitors

Walker, A type system for expressive security policies

Information Flow Security

McLean, A general theory of composition for trace sets closed under selective interleaving functions.

Encryption and Languages

Duggan, Cryptographic types.
Sumii and Pierce, Logical Relations for Encryption.
Gifford, Cryptographic sealing for information secrecy and authentication

Security Protocol Verification

Abadi, Security Protocols and their Properties