SE547: Foundations of Computer Security (Spring 2006)
James Riely

Important Links


Course online

Mailing list


Code examples

More Links
Software, Books and Other Resources
Lecture Materials
Notes HW
1. Security Automata [03/31]

Skim these notes by Andrew Meyers.

Skim section I.A of The Protection of Information in Computer Systems by Saltzer and Schroeder.

Read Enforceable Security Policies by Fred Schneider.

Read Enforcing Non-safety Security Policies with Program Monitors by Jay Ligatti, Lujo Bauer and David Walker.

Read Composing Security Policies in Polymer by Lujo Bauer, Jay Ligatti and David Walker.

available available not available
2. Information Flow [04/06]

Read A Sound Type System for Secure Flow Analysis

Read A New Type System for Secure Information Flow

Read Non-interference for concurrent programs and thread systems

Skim JFlow: Practical Mostly-Static Information Flow Control

Skim A Decentralized Model for Information Flow Control

available available not available
3. Pi and Spi [04/13]

Read sections I and II of Notes on nominal calculi for security and mobility

Alternatively, read A Calculus for cryptographic protocols: the spi calculus

available available not available
4. Cryptyc [04/20]

Read Typing Correspondence Assertions for Communication Protocols

Read Authenticity by Typing for Security Protocols

Try the applet at

available available not available
5. BDDs [04/27]

Read H. R. Andersen. An Introduction to Binary Decision Diagrams. Lecture Notes, Technical Univresity of Denmark, 1998.

Read R. E. Bryant. Graph-Based Algorithms for Boolean Function Manipulation In IEEE Trans. Computers C-35(8) pp. 677-691, 1986.

available available not available
6. CBMC [05/04]

Read E. Clarke and D. Kroening. ANSI-C Bounded Model Checker User Manual. Technical Report, Carnegie Mellon University, 2003.

Read E. Clarke, D. Kroening and K. Yorav. Behavioral Consistency of C and Verilog Programs Using Bounded Model Checking In Proc. Design and Automation Conf. pp. 368-371, 2003.

Download CBMC. You may also need

available available not available
7. PCC [05/11]

Read P. Lee and G. Necula. Research on Proof-Carrying Code for Mobile-Code Security. In Proc. DARPA Workshop on Foundations for Secure Mobile Code, 1997.

Read G. Necula and P. Lee. Safe Kernel Extensions Without Run-Time Checking In Proc. Symp. Operating Systems Design and Implementation. pp. 229-243, 1996.

Check out George Necula's Touchstone and Proof-Carrying Code Demo

Notes from Peter Lee: file:lec1.pdf file:lec2.pdf file:lec3.pdf file:lec1.ppt file:lec2.ppt file:lec3.ppt

not available not available not available
8. Presentations [05/18]
available available not available
9. Presentations [05/25]
available available not available
10. Presentations [06/01]
available available not available
11. Presentations [06/08]
available available not available
Contact Hours
Class Hours: Thu 5:45pm-9:00pm in Lewis 1214 [Section 901]
Office Hours: Wed 4:30-5:30pm in CDM 846
Thu 4:30-5:30pm in CDM 846

The stylesheets used to create this website are based on Corin Pitcher's XSLT stylesheets for lecture slides.