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
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
- 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
Information Flow Security
  • McLean, A general theory of composition for trace sets closed under selective interleaving functions.
Encryption and Languages
Security Protocol Verification