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
8/27 Introduction [pdf]
8/29 Propositional logic & proofs [pdf][tex]
9/3 Program semantics, safety, & dynamic logic [pdf][tex]
9/5 Proving safety, compositionally [pdf][tex]
9/10 Safety proofs, continued [pdf][tex]
9/12 Automated safety checkers, proof practice [pdf][tex]
9/17 Memory Safety & Sandboxing [pdf][tex]
9/19 Software fault isolation [pdf][tex]
9/24 Control flow safety [pdf][tex]
9/26 Security automata & dynamic instrumentation [pdf][tex]
10/1 Midterm exam
10/3 Information flow policies [pdf][tex]
10/8 Information flow types I [pdf][tex]
10/10 Information flow types II [pdf][tex]
10/15 Relaxing noninterference [pdf][tex]
10/17 Guest lecture: Arthur Azevedo de Amorim, Dynamic Information Flow Control [slides]
10/22 Provable privacy I [pdf][tex]
10/24 Provable privacy II [pdf][tex]
10/29 Timing side channels [pdf][tex]
10/31 Memory side channels [pdf][tex]
11/5 Web security: application model & same-origin policy [pdf][tex]
11/7 Web security: attacks & defenses [pdf][tex]
11/12 Authorization, logically [pdf][tex]
11/14 Bootstrapping Trust [pdf][tex]
11/19 Trusted computing [pdf][tex]
11/21 Trusted computing, continued [pdf][tex]
11/26 No class (Thanksgiving break)
11/28 No class (happy Thanksgiving!)
12/3 No lecture Extended office hours, instructors will be available to assist with Lab 3 and Homework 6
12/5 Final review
12/9 Final exam