Information-Flow Security Group
Participants: Brigitte Pientka, Ahmer Ahmedani,
Ye Henry Tian, Clark Verbrugge, Sam Sanjabi.
Readings/Presentations by Week:
- May 6th: Sabelfeld & Myers, "Language-Based Information-Flow
Security". [PDF]
- May 12th:
- May 20th:
- Ahmer -- Robert O'Callahan, "A Simple, Comprehensive Type System
for Java Bytecode Subroutines". [PDF]
- May 27th:
- Sam -- Morrisett et al. "Stack-Based Typed Assembly Language".
[PDF]
I. Background Papers
Numbered references refer to the following paper:
- Andrei Sabelfeld and Andrew C. Myers, "Language-Based Information-Flow
Security".[PDF]
Other background:
- Danny Dolev and Andrew C. Yao, "On the Security of Public Key
Protocols", IEEE Transactions on Information Theory, Vol. IT-29, No. 2,
March 1983, pp. 198-208.
- Nevin Heintze and Jon G. Riecke, "The SLam Calculus: Programming
with Secrecy and Integrity". [PS]
- Spi-Calculus
- Martin Abadi and Andrew D. Gordon, "A Calculus for Cryptographic
Protocols: The Spi-Calculus". [CONCUR
(PS)] [SRC
Report (PS)]
- Martin Abadi and Andrew D. Gordon, "Reasoning about Cryptographic
Protocols in the Spi Calculus". [PS]
- Abstract Interpretation
- Patrick Cousot & Radhia Cousot, "Abstract interpretation:
a unified lattice model for static analysis of programs by construction
or approximation of fixpoints." [PDF]
- J.H. Saltzer, D.P. Reed, and D.D. Clark, "End-to-end arguments
in system design". [1]
II. Typed Assembly Language
- Robert O'Callahan, "A Simple, Comprehensive Type System for Java
Bytecode Subroutines". [PDF][Ajax
Web Site (PhD)]
- Raymie Stata and Martin Abadi, "A Type System for Java Bytecode
Subroutines". [SRC Report
(PS)]
- Morrisett et al.:
- "From System F to Typed Assembly Language". [28]
- "Stack-Based Typed Assembly Language". [PDF]
- J. Agat, "Type Based Techniques for Covert Channel Eliminiation
and Register Allocation". (PhD Thesis) [119]
III. Advanced Type Systems
- M.A. Sheldon and D.K. Gifford, "Static Dependent Types for First
Class Modules". [122]
- H. Xi and F. Pfenning, "Depend Types in Practical Programming".
[123]
IV. Improved Security Policies
- Volpano & Smith [3,63,67,70,87] but especially
- [3] D. Volpano, G. Smith, and C. Irvine, "A Sound Type System
for Secure Flow Analysis". [citeseer][Slides
(PDF)] ... probably continues in [63] & [87]
- [67] D. Volpano and G. Smith, "Eliminating Covert Flows with
Minimum Typings".
- [70] D. Volpano and G. Smith, "Verifying Secrets and Relative
Secrecy".
- Abstract Interpretation and Security
- [136] M. Zanotti, "Security Typings by Abstract Interpretation".
- Also Jerome Feret has done some work in this area ...
- David Walker Reference (which I've already lost...)
V. Java, ML & Information Flow
- Atsushi Igarashi, Benjamin Pierce, and Philip Wadler,"Featherweight
Java: A Core Calculus for Java and GJ". [Tech Report
(PS)] [OOPSLA (PS)][Slides
by Robert Harper (PDF)]
- Andrew C. Myers, "JFlow: Practical Mostly-Static Information
Flow". [POPL
(PS)][Slides
(PDF)]
- Other Java-like stuff (Jif etc.): [13,44,94]
- ML: [14,77]
- Banatre et al. have done some work on compile-time detection
of information flow in...
- Sequential programs [57]
- Parallel & Distributed Systems [56,58]
VI. Stack Inspection