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

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.

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

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

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

Read Typing Correspondence Assertions for Communication Protocols

Read Authenticity by Typing for Security Protocols

Try the applet at http://www.cryptyc.org/

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.

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 file:ansi-c-lib.zip

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