A and L denote lectures to be delivered by Anupam and Lujo, respectively. MM = Michelle Mazurek
|
Date |
Topic |
|
Notes |
|
Mon Aug 23 |
Introduction; overview of software security problems [A+L] [PDF] |
|
|
|
Wed Aug 25 |
Buffer overflows, format-string vulnerabilities, and other attacks [A] [PDF] |
· Cowan et al., Buffer Overflows: Attacks and Defenses for the Vulnerability of the Decade, Foundations of Intrusion Tolerant Systems 2003. · blexim, Basic Integer Overflows (Sections 1-3) · team teso, Exploiting Format String Vulnerabilities (Sections 1-3) · Optional: Aleph One, Smashing The Stack For Fun And Profit · Optional: Úlfar Erlingsson, Low-Level Software Security: Attacks and Defenses. FOSAD 2007: 92-134 |
|
|
Mon Aug 30 |
Web attacks and defenses [L] [PDF] |
· Jim, Swamy, and Hicks, Defeating script injection attacks with browser-enforced embedded policies, WWW 2007. |
|
|
Wed Sep 1 |
Software security architectures (separation, memory protection) [L] [PDF] |
· Saltzer and Schroeder, The Protection of Information in Computer Systems. 1975. · Optional: Wahbe et al., Efficent Software-based Fault Isolation. SOSP, 1994. |
Assignment 1 handed out. (Discussion notes) |
|
Mon Sep 6 |
No class—university holiday |
· |
|
|
Wed Sep 8 |
Software security architectures (VMs, Java sandboxing) [L] [PDF] |
· McGraw and Felten, Securing Java, chp. 3. John Whiley and Sons, 1999. · Garfinkel and Rosenblum, A Virtual Machine Introspection Based Architecture for Intrusion Detection, NDSS 2003. |
|
|
Mon Sep 13 |
Overview of cryptography; Software security architectures (Trusted Computing) [Jonathan McCune] [PDF] |
· Parno, McCune, and Perrig, Bootstrapping Trust in Commodity Computers, IEEE Security & Privacy 2010. · Sailer et al., Design and Implementation of a TCG-based Integrity Measurement Architecture, USENIX Security 2004. |
Assignment 1B handed out. (Discussion notes) |
|
Wed Sep 15 |
Software security architectures (Trusted Computing) [A] [PDF] |
· McCune et al., Flicker: An Execution Infrastructure for TCB Minimization, EuroSys 2008. · Optional: McCune et al., TrustVisor: Efficient TCB Reduction and Attestation, IEEE Security & Privacy 2010. |
|
|
Mon Sep 20 |
Software model checking [A] [PDF] |
· Chaki et al., Modular Verification of Software Components in C, TSE 2004. |
Assignment 1 due |
|
Wed Sep 22 |
Software model checking for security [A] [PDF] |
· Chaki and Datta, ASPIER: An Automated Framework for Verifying Security Protocol Implementations, Tech. Report 2008. · Chen et al., Model Checking One Million Lines of C Code, NDSS 2004. |
|
|
Mon Sep 27 |
In-class test |
|
|
|
Wed Sep 29 |
Static analysis for detecting buffer overflows [A][PDF] |
· Ganapathy et al., Buffer Overrun Detection using Linear Programming and Static Analysis, CCS 2003. |
|
|
Mon Oct 4 |
Static analysis for software security (metacompilation) [MM] [PDF] |
· Engler et el., Checking System Rules Using System-Specific, Programmer-Written Compiler Extensions, OSDI 2000. |
Assignment 2 handed out. Instructions. VM. Tarball. Murphi3.1_gcc4.2 Murphi3.1_gcc4.3 |
|
Wed Oct 6 |
Usability in software security [Lorrie Cranor][PDF] |
· Egelman et al., You've been warned: an empirical study of the effectiveness of web browser phishing warnings, CHI 2008. · Cranor, A framework for reasoning about the human in the loop, Conference on Usability, Psychology, and Security, 2008. |
|
|
Mon Oct 11 |
Dynamic analysis (DART, CUTE, EXE) [L] [PDF] |
· Godefroid, Klarlund, and Sen, DART: Directed Automated Random Testing, PLDI 2005. · Cadar, Ganesh, Pawlowski, Dill, and Engler, EXE: automatically generating inputs of death, CCS 2006. |
|
|
Wed Oct 13 |
Software analysis of a microkernel [Limin Jia] [PDF] |
· Klein et al., seL4: Formal verification of an OS kernel, SOSP 2009. |
Assignment 2B handed out. Discussion notes. |
|
Mon Oct 18 |
Software analysis for malware detection [A] [PDF] |
· Christodorescu et al., Semantics-Aware Malware Detection, IEEE S & P, May 2005. |
|
|
Wed Oct 20 |
Language-based approaches to security (type systems) [Deepak Garg] [PDF] |
· Cardelli, Type Systems (Sections 1-3), in CRC Handbook of Comp. Sci. and Eng. · Jim et al., Cyclone: A safe dialect of C, USENIX 2002. |
Assignment 2 due Fri Oct 22 |
|
Mon Oct 25 |
Language-based approaches to security (non-interference) [A] [PDF] |
· Denning and Denning, Certification of programs for secure information flow, CACM 1977. · Volpano et al., A Sound Type System for Secure Flow Analysis, JCS 1996. |
|
|
Wed Oct 27 |
In-class test |
|
|
|
Mon Nov 1 |
Language-based approaches to security (JIF) [L] [PDF] |
· Sabelfeld and Myers, Language-based information flow security, IEEE Journal on Selected Areas in Communications, 2003. · Askarov and Sabelfeld, Security-typed languages for implementation of cryptographic protocols: A case study, ESORICS 2005. · Hicks et al., Understanding practical application development in security-typed languages, ACSAC 2006. ·
Optional: Chong et al., SIF: Enforcing
confidentiality and integrity in Web applications, USENIX Security 2007. |
|
|
Wed Nov 3 |
Language-based approaches to security (Proof-Carrying
Code) [L] [PDF] |
· Necula and Lee, Safe kernel extensions without run-time checking, OSDI 1996. |
|
|
Mon Nov 8 |
Language-based approaches to security (Typed Assembly Language) [L] [PDF] |
· Morrissett et al., TALx86: A Realistic Typed Assembly Language, Workshop on Compiler Support for System Software 1999. |
|
|
Wed Nov 10 |
Run-time enforcement (understanding the power of
enforcement mechanisms) [L] [PDF] |
· Schneider, Enforceable security policies, TISSEC 2000. |
Assignment 3, part 1 instructions and tarball. |
|
Mon Nov 15 |
Run-time enforcement (implementing enforcement mechanisms) [L] [PDF] |
· Erlingsson and Schneider, SASI enforcement of security policies, NSPW 1999. · Optional: Bauer, Ligatti, and Walker, Composing security policies with Polymer, PLDI 2005. |
|
|
Wed Nov 17 |
Run-time enforcement (CFI) [A] [PDF] |
· Abadi et al., Control-Flow Integrity: Principles, Implementations, and Applications, TISSEC 2009. |
Homework 3 VM, Instructions and Part 3 files. |
|
Mon Nov 22 |
Review: midterm 2, Jif, language-based security and
run-time enforcement [A+L] [Jif
Notes] |
|
|
|
Wed Nov 24 |
No class—university holiday |
|
|
|
Mon Nov 29 |
Wrap-up [A+L] [PDF] |
|
Assignment 3 due |
|
Wed Dec 1 |
In-class test |
|
|