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 |