Lecture notes will be posted shortly prior to each class meeting.

Note: to compile lecture notes, you will need to download the latex packages and place the .sty files in the same directory as the lecture source.

date topic notes comments
9/1 Introduction [pdf]
9/3 Propositional logic & proofs [pdf][tex]
9/8 Soundness [pdf][tex]
9/10 Program semantics [pdf][tex]
9/15 Safety & dynamic logic [pdf][tex]
9/17 Compositional safety proofs [pdf][tex]
9/22 More compositional safety [pdf][tex]
9/24 Memory Safety & Sandboxing [pdf][tex]
9/29 Memory Safety Continued [pdf][tex]
10/1 Software Fault Isolation [pdf][tex]
10/6 Security Automata [pdf][tex]
10/8 Wrap-up Security Automata, Midterm Review
10/13 Midterm Exam
10/15 Guest Lecture: Prof. Bryan Parno on Provably-Secure Systems
10/20 Information Flow Policies [pdf][tex]
10/22 Information Flow Types [pdf][tex]
10/27 Information Flow Types II [pdf][tex]
10/29 Soundness of Information Flow Enforcement [pdf][tex]
11/3 Relaxing Noninterference [pdf][tex]
11/5 Side Channels I [pdf][tex]
11/10 Side Channels II [pdf][tex]
11/12 Provable Privacy [pdf][tex]
11/17 Provable Privacy [pdf][tex]
11/19 Authorization, logically [pdf][tex]
11/24 No class, extended office hours
11/26 No class (happy thanksgiving!)
12/1 Bootstrapping Trust [pdf][tex]
12/3 PKI Continued, Trusted Computing [pdf][tex]
12/8 Trusted Computing Continued
12/10 Web Security
12/15 Final exam Note: date subject to change