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