Reading List: Language Based Security, Fall 2003

Below is a superset of the papers covered in class.

General

Fred B. Schneider, Greg Morrisett, and Robert Harper: A Language-based Approach to Security.

Typed Assembly Language

Greg Morrisett, David Walker, Karl Crary, and Neal Glew: From System F to Typed Assembly Language.

Greg Morrisett, Karl Crary, Neal Glew, and David Walker: Stack-Based Typed Assembly Language.

Neal Glew and Greg Morrisett: Type-Safe Linking and Modular Assembly Language.

Dan Grossman and Greg Morrisett: Scalable Certification for Typed Assembly Language.

Greg Morrisett, Karl Crary, Neal Glew, Dan Grossman, Richard Samuels, Frederick Smith, David Walker, Stephanie Weirich, and Steve Zdancewic: TALx86: A Realistic Typed Assembly Language.

Karl Crary and Stephanie Weirich: Resource Bound Certification.

Karl Crary, David Walker, and Greg Morrisett: Typed Memory Management in a Calculus of Capabilities.

Proof Carrying Code

Peter Lee and George Necula: Research on Proof-Carrying Code for Mobile Code Security.

George Necula and Peter Lee: Safe Kernel Extensions Without Run-Time Checking.

George C. Necula: Proof-carrying code.

George C. Necula and Peter Lee: Safe, Untrusted Agents using Proof-Carrying Code.

George Necula and Peter Lee: The Design and Implementation of a Certifying Compiler.

David Walker: A Type System for Expressive Security Properties.

Andrew W. Appel and Amy P. Felty: A Semantic Model of Types and Machine Instructions for Proof-Carrying Code.

George C. Necula and S.P. Rahul: Oracle-Based Checking of Untrusted Software.

Information Flow

Andrei Sabelfeld and Andrew C. Myers: Language-based Information-Flow Security.

Anindya Banerjee and David A. Naumann: Stack-based Access Control for Secure Information Flow.

Dennis Volpano and Geoffrey Smith: A Type-Based Approach to Program Security.

Dennis Volpano, Geoffrey Smith, and Cynthia Irvine: A Sound Type System for Secure Flow Analysis.

Andrew C. Myers and Barbara Liskov: A Decentralized Model for Information Flow Control.

Andrew C. Myers and Barbara Liskov: Complete, Safe Information Flow with Decentralized Labels.

Andrew C. Myers: Mostly-Static Decentralized Information Flow Control.

Steve Zdancewic and Andrew C. Myers: Robust Declassification.

Lantian Zheng, Stephen Chong, Andrew C. Myers, and Steve Zdancewic: Using Replication and Partitioning to Build Secure Distributed Systems.

Steve Zdancewic and Andrew C. Myers: Observational Determinism for Concurrent Program Security.

Anindya Banerjee and David A. Naumann: Secure Information Flow and Pointer Confinement in a Java-like Language.

Andrei Sabelfeld and David Sands: Probabilistic Noninterference for Multi-threaded Programs.

Ádám Darvas, Reiner Hähnle, and David Sands: A Theorem Proving Approach to Analysis of Secure Information Flow.

Stack Inspection

Dan S. Wallach, Andrew Appel, and Ed Felten: SAFKASI: A Security Mechanism for Language-based Systems.

Franois Pottier, Christian Skalka, and Scott Smith: A Systematic Approach to Static Access Control.

Cedric Fournet and Andrew Gordon: Stack Inspection: Theory and Variants.

Anindya Banerjee and David A. Naumann: Using Access Control for Secure Information Flow in a Java-like Language.

Tomoyuki Higuchi and Atsushi Ohori: A Static Type System for JVM Access Control.

Tomoyuki Higuchi and Atsushi Ohori: Java Bytecode as a Typed Term Calculus.

Bytecode Verification

P. Bieber and J. Cazin and P. Girard and J-L. Lanet and V. Wiels and G. Zanon: Checking Secure Interactions of Smart Card Applets: extended version (preliminary version).

R. Stata and M. Abadi: A type system for Java bytecode subroutines.

Xavier Leroy: Java bytecode verification: algorithms and formalizations.

Xavier Leroy: Bytecode verification on Java smart cards.

Torben Amtoft
Anindya Banerjee