Overview Lecture (powerpoint)
Gary McGraw and Greg Morrisett. Attacking Malicious Code: A Report to the Infosec Research Council. In IEEE Software, Volume 17(5), September/October 2000.
F.B. Schneider, G. Morrisett, and R. Harper. A Language-Based Approach to Security. Informatics: 10 Years Back, 10 Years Ahead (Saarbrucken, Germany, August 2000), Lecture Notes in Computer Science, Volume 2000 (Reinhard Wilhelm, ed.), Springer-Verlag, Heidelberg, 2000, 86-101.
C. Colby, K. Crary, R. Harper, P. Lee, F. Pfenning. Automated Techniques for Provably Safe Mobile Code. Theoretical Computer Science, 2000.
B. Bershad, S. Savage, P. Pardyak, D. Becker, M. Fiuczynski, E.G. Sirer. Protection is a Software Issue. In Proceedings of the Fifth Workshop on Hot Topics in Operating Systems (HotOS-V), Orcas Island, WA. pp. 62-65.
Software-Based Fault Isolation (powerpoint)
Wahbe, R., S. Lucco, T.E. Anderson, S.L. Graham. Efficient Software-Based Fault Isolation. In Proceedings of the 14th ACM Symposium on Operating Systems Principles, pages 203--216, December 1993.
Chris Small. MiSFIT: A Tool for Constructing Safe Extensible C++ Systems. In Proceedings of the Third Usenix Conference on Object-Oriented Technologies, Portland, OR, June 1997.
Stack Inspection (powerpoint)
Wallach, D. and E. Felten. Understanding Java Stack Inspection. In Proceedings of the 1998 IEEE Symposium on Security and Privacy, Oakland, CA, 1998.
A. Gordon and C. Fournet. Stack Inspection: Theory and Variants. In Conference Record of POPL 2002 The 29th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, ACM Press, 2002. An extended version of this paper appears as Technical Report MSR-TR-2001-103, Microsoft Research, December 2001.
Inlined Reference Monitors (powerpoint)
U. Erlingsson and F.B. Schneider. SASI Enforcement of Security Policies: A Retrospective. Proceedings of the New Security Paradigm Workshop (Caledon Hills, Ontario, Canada, September 1999), Association for Computing Machinery, 87--95.
U. Erlingsson and F.B. Schneider. IRM Enforcement of Java Stack Inspection. Proceedings 2000 IEEE Symposium on Security and Privacy (Oakland, California, May 2000), IEEE Computer Society, Los Alamitos, CA, 246--255.
David Evans and Andrew Twynman. Flexible Policy-Directed Code Safety. In 1999 IEEE Symposium on Security and Privacy, Oakland, CA, May 1999.
- Greg Morrisett, David Walker, Karl Crary, and Neal Glew. From System F to Typed Assembly Language. In ACM Transactions on Programming Languages and Systems, 21(3):528-569, May 1999.
- 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. In the 1999 ACM SIGPLAN Workshop on Compiler Support for System Software, pages 25-35, Atlanta, GA, USA, May 1999.
- George Necula. Proof-Carrying Code. In 24th ACM Symposium on Principles of Programming Languages, pages 106-119, Paris France, January 1997.
- George Necula and Peter Lee. Proof-Carrying Code. CMU-CS Technical Report CMU-CS-96-165. November, 1996. (A longer version of the above with more details.)
- George Necula. The Design and Implementation of a Certifying Compiler. In ACM Conference on Programming Language Design and Implementation, June 1998.
- Andrew W. Appel and Amy P. Felty. A Semantic Model of Types and Machine Instructions for Proof-Carrying Code. 27th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL '00), pp. 243-253, January 2000.
- Appel, Andrew W. and David McAllester. An Indexed Model of Recursive Types for Foundational Proof-Carrying Code. Princeton University Computer Science TR-629-00, November 2000.
- Karl Crary, David Walker, and Greg Morrisett. Typed Memory Management in a Calculus of Capabilities. In Twenty-Sixth ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 262-275, San Antonio, TX, USA, January 1999.
- David Walker. A Type System for Expressive Security Properties. In the Twenty-Seventh ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 254-267, Boston, MA, USA, January 2000.
- Grzegorz Czajkowski and Thorsten von Eicken. JRes: A Resource Accounting Interface for Java. Department of Computer Science, Proceedings of 1998 ACM OOPSLA Conference, Vancouver, BC, October 1998.
- [Greg B. will come back to this one later in the semester:] Crary, Karl and Stephanie Weirich. Resource Bound Certification. In the Twenty-Seventh ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 184-198, Boston, MA, USA, January 2000.
- J-Kernel (Walter)
- SPIN (Nate)
- Brian Bershad, Stefan Savage, Przemyslaw Pardyak, Emin Gun Sirer, David Becker, Marc Fiuczynski, Craig Chambers, Susan Eggers. Extensibility, Safety and Performance in the SPIN Operating System, in Proceedings of the 15th ACM Symposium on Operating System Principles (SOSP-15), Copper Mountain, CO. pp. 267--284.
- Przemyslaw Pardyak, Brian Bershad, Dynamic Binding for an Extensible System, in Proceedings of the Second USENIX Symposium on Operating Systems Design and Implementation (OSDI), Seattle, WA, pp. 201-212, October 1996.
- Vino (???)
- Margo Seltzer and Christopher Small, Self-monitoring and Self-adapting Operating Systems (postscript, html), Proceedings of the Sixth Workshop on Hot Topics in Operating Systems
- Margo Seltzer, Yasuhiro Endo, Christopher Small, Keith Smith, Dealing with Disaster: Surviving Misbehaved Kernel Extensions (postscript), Proceedings of the 1996 Symposium on Operating System Design and Implementation (OSDI II).
- Vault (Yanling)
- Robert DeLine and Manuel Fähndrich. Enforcing high-level protocols in low-level software. In Proceedings of the ACM Conference on Programming Language Design and Implementation, June 2001, pages 59-69.