CMSC 838Z Spring 2005

Language-Based Security


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.

Notes, Supplementary Papers
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

Security Foundations
- Saltzer and Schroeder, Protection of Information in Computer Systems
- Denning and Denning, Data Security

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
Hamlen, Morrisett, and Schneider, Computability Classes for Enforcement Mechanisms Lecture notes (Hicks)
- 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)
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)
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)
- Sekar, Venkatakrishnan, Basu, Bhatkar, and DuVarney, Model-Carrying Code: A Practical Approach for Safe Execution of Untrusted Applications
- Appel, Foundational Proof-Carrying Code

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
- 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

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
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

- 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
- 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
- Viega, Bloch,  Kohno, and McGraw, ITS4: A Static Vulnerability Scanner for C and C++ Code
- Wagner and Dean, Intrusion Detection via Static Analysis

Grab Bag
- Bauer, Ligatti and Walker, Composing Security Policies in Polymer
- Gopalakrishna, Spafford and Vitek, Efficient Intrusion Detection using Automaton Inlining

Student Presentations
- (Gary Jackson presents) Bishop and Dilger, Checking for Race Conditions in File Accesses
- (Morgan Kleene presents) Chothia,  Duggan, and Vitek, Type-based Distributed Access Control

- (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

- (Justin McCann presents) Abadi, Secrecy by Typing for Security Protocols
- (Saurabh Srivistava presents) Gordon and Jeffrey, Authenticity by Typing for Security Protocols

- (Jose Troche presents) Zitser, Leek and Lippman, Testing Static Analysis Tools Using Exploitable Buffer Overflows From Open Source Code
- (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

Project Presentations
Tim Fraser

Justin McCann
Saurabh Srivistava
Jose Troche

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