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 |
|---|---|---|---|
| 1/16 | Introduction | [pdf] | |
| 1/18 | Propositional logic & proofs | [pdf][tex] | |
| 1/23 | Program semantics, safety, & dynamic logic | [pdf][tex] | |
| 1/25 | Proving safety, compositionally | [pdf][tex] | |
| 1/30 | Bounded model checking & symbolic execution | [pdf][tex] | |
| 2/1 | Memory safety & sandboxing | [pdf][tex] | |
| 2/6 | Inlining safety | [pdf][tex] | |
| 2/8 | Lab 0 discussion, Control flow safety | [pdf][tex] | |
| 2/13 | Security automata & dynamic instrumentation | [pdf][tex] | |
| 2/15 | Information flow policies | [pdf][tex] | |
| 2/20 | Information flow types I | [pdf][tex] | |
| 2/22 | Pin tutorial session | ||
| 2/27 | Information flow types II | [pdf][tex] | |
| 3/1 | Midterm review | ||
| 3/6 | Midterm exam | ||
| 3/8 | Guest lecture: Prof. Jean Yang on policy-agnostic programming | ||
| 3/13 | No class, spring break | ||
| 3/15 | No class, spring break | ||
| 3/20 | Relaxing noninterference | [pdf][tex] | |
| 3/22 | Provable privacy | [pdf][tex] | |
| 3/27 | Timing side channels | [pdf][tex] | |
| 3/29 | Memory side channels | [pdf][tex] | |
| 4/3 | Web application security I | [pdf][tex] | |
| 4/5 | Guest lecture: Prof. Bryan Parno on end-to-end security and full-system verification | ||
| 4/10 | Web application security II | [pdf][tex] | |
| 4/12 | Penetration testing, Lab 3 tutorial | [pdf][tex] | |
| 4/17 | Distributed authorization | [pdf][tex] | |
| 4/19 | No class (happy Carnival!) | ||
| 4/24 | Bootstrapping Trust | [pdf][tex] | |
| 4/26 | Trusted Computing | [pdf][tex] | |
| 5/1 | Final review | ||
| 5/3 | Final exam |