| 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 |
| 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, 16 | Stack 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 18 | Proof-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 23 | Typed 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 25 | Thanksgiving, no class |
| Nov 30 | Review |
| Dec 2 | Student presentations |
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.
If you are interested in some of:
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.
Last update: Monday, January 29, 2007