CS 101 (Fall 2005)
Special Topics in Computer Science
Language-Based Security

Time: WF 1:00–1:55
Place: Jorgensen 287
Instructor:  Aleksey Nogin
Units: 9 (2+0+7), pass/fail or letter grade
Office Hours:  Wed 6 PM, Moore 04 and by appointment
TA: Nathan Gray
Mailing list: cs101-class@metaprl.org


Paper reading project

Schedule and Lecture Notes

This schedule is preliminary and is subject to change
Oct 5 Introduction to Language-Based Security, Introduction into OCaml, Introduction into Lambda-Calculus.
Slides (PDF, 4 per page), OCaml session transcript
Oct 7 Introduction into Lambda-Calculus, Introduction into OCaml (Continued)
Slides (PDF, 4 per page), Evaluation and typing rules, examples (PDF), OCaml session transcript
Oct 12 Type Preservation for Simply-Typed Lambda-Calculus
Slides (PDF, 4 per page), Substitution Lemma — proof fragment (PDF)
Oct 14, 19, 21 SLam: Lambda-Calculus and Secure Flow Analysis (purely functional fragment)
OCaml session transcript: Oct 14, Oct 19, Slides (PDF, 4 per page),
Paper: Nevin Heintze and Jon G. Riecke. The SLam calculus: programming with secrecy and integrity. In Proceedings of the 25th ACM Symposium on Principles of Programming Languages (POPL), pages 365--377, San Diego, CA, January 19-21, 1998. (Gzipped Postscript)
Oct 26 SLam: Non-Interference; Discussion
Operational Semantics of a Simple Imperative Language
Slides (part 2 of the lecture, PDF, 4 per page)
Oct 28 Secure Flow Analysis of a Simple Imperative Language
Paper: Andrei Sabelfeld, Andrew C. Myers. Language-based information-flow security. IEEE Journal on Selected Areas in Communication, special issue on Formal Methods for Security, 21(1), January 2003, pages 5-19.
Mutable References in Lambda-Calculus
Type checking and operational semantics of references
Nov 2 Secure Flow Analysis of the full SLam language.
Introduction to Stack Inspection.
Nov 4, 9, 16Stack Inspection.
Paper: Cedric Fournet and Andrew D. Gordon. Stack inspection: theory and variants, ACM Symposium on Principles of Programming Languages (POPL), January 2002, pp. 307–318.
Nov 18Proof-Carrying Code.
Paper: George C. Necula, Peter Lee, Safe Kernel Extensions Without Run-Time Checking. In 2nd Symposium on Operating Systems Design and Implementation (OSDI '96), October 28--31, 1996. Seattle, WA
George Necula's PCC Page
Nov 23Typed Assembly Language.
Paper: G.Morrisett, D.Walker, K.Crary, and N.Glew.  From System-F to Typed Assembly Language.  In ACM Symposium on Principles of Programming Languages (POPL), January 1998, San Diego, pp. 85-97.
Nov 25Thanksgiving, no class
Nov 30Review
Dec 2Student presentations

Useful links


Other courses on language-based security

Survey Papers

What is language-based security?

Traditionally, computer security has been enforced at the level of operating systems. However, modern attacks often succeed at circumventing operating-system security mechanisms. A part of the problem is that while operating-system security policies are low-level (such as access control policies, protecting particular files), many attacks are high-level, or application-level (such as email worms that pass by access controls pretending to be executed on behalf of a mailer application). The key to defending against application-level attacks is application-level security. Because applications are typically specified and implemented in programming languages, this area is generally known as language-based security. A direct benefit of language-based security is the ability to naturally express security policies and enforcement mechanisms using the developed techniques of programming languages.

Who should take this class?

If you are interested in some of:

then this class is for you!

You should have previously studied a course in programming languages (and of course basic programming skills are assumed) and basics of computer security. It is an advantage if you have experience with functional languages (such as OCaml) and/or if you have studied courses such as semantics of programming languages and compiler construction.

Some materials in this course are based on Andrei Sabelfeld's course. I would like to thank Andrei for his permission to use them here.

Valid HTML 4.01!  Valid CSS!

Last update: Monday, January 29, 2007