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 |