18-732 — Secure Software Systems

Schedule (subject to change)

A, L, and J denote lectures to be delivered by Anupam, Lujo, and Jon, respectively.

Date	Topic	Reading	Notes
Mon Aug 25	No class—CS immigration course
Wed Aug 27	No class—CS immigration course
Mon Sep 1	No class—university holiday
Wed Sep 3	No class—CS immigration course
Mon Sep 8 (A+L)	Introduction; overview of software security problems [PDF]	CMU Computing Policy CMU Policy on Cheating
Wed Sep 10 (A)	Overview of Cryptography [PDF] Software security architectures (Trusted Computing) [PDF] [PPT]	Grawrock, The Intel Safer Computing Initiative (chapter 8). Intel Press, 2006. Sailer et al., Design and Implementation of a TCG-based Integrity Measurement Architecture, USENIX Security 2004.	Grawrock book to be handed out in class
Mon Sep 15 (J)	Software security architectures (Trusted Computing) [PDF] [PPT]	Grawrock, The Intel Safer Computing Initiative (chapter 11). Intel Press, 2006. McCune et al., Flicker: An Execution Infrastructure for TCB Minimization, EuroSys 2008. Optional: Trusted Computing Group. TCG Architecture Overview. Optional: Berger et al., vTPM: Virtualizing the Trusted Platform Module, USENIX Security 2006.	Optional readings recommended for project
Wed Sep 17 (L)	Software security architectures (separation, memory protection) [PDF]	Saltzer and Schroeder. The Protection of Information in Computer Systems. 1975. Optional: Wahbe et al. Efficent Software-based Fault Isolation. SOSP, 1994.	Project 1 handed out [PDF]
Mon Sep 22 (L)	Software security architectures (VMs, Java sandboxing) [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.
Wed Sep 24 (A)	Buffer overflows, format-string vulnerabilities, and other attacks [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
Mon Sep 29 (A)	Static analysis for detecting buffer overflows [PDF]	Ganapathy et al., Buffer Overrun Detection using Linear Programming and Static Analysis, CCS 2003.
Wed Oct 1 (L)	Dynamic analysis (DART, CUTE, EXE) [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.	Project 1, parts 2-3 [PDF]
Mon Oct 6 (A)	Software model checking [PDF]	Chaki et al., Modular Verification of Software Components in C, TSE 2004.
Wed Oct 8 (J)	Static analysis for software security (metacompilation) [PDF]	Engler et el., Checking System Rules Using System-Specific, Programmer-Written Compiler Extensions, OSDI 2000.
Mon Oct 13	Midterm exam
Wed Oct 15 (*)	Software model checking for security [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.	Guest Lecturer: Sagar Chaki Project 2 handed out [PDF]
Mon Oct 20 (A)	Language-based approaches to security (non-interference) [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 22 (L)	Language-based approaches to security (Typed Assembly Language) [PDF]	Morrissett et al., TALx86: A Realistic Typed Assembly Language, Workshop on Compiler Support for System Software 1999.
Mon Oct 27 (*)	Usability in software security [PDF, PPTX]	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.	Guest lecturer: Lorrie Cranor
Wed Oct 29 (L)	Language-based approaches to security (Proof-Carrying Code) [PDF]	Necula and Lee. Safe kernel extensions without run-time checking, OSDI 1996.
Mon Nov 3 (*)	Language-based approaches to security (AURA) [PDF]	Vaughan et al. Evidence-based audit, CSF 2008.	Guest lecturer: Limin Jia
Wed Nov 5 (*)	Language-based approaches to security (JIF) [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.	Guest lecturer: Boniface Hicks Project 3 handed out
Mon Nov 10 (A)	Malware detection [PDF]	Christodorescu et al., Semantics-Aware Malware Detection, IEEE S & P, May 2005.
Wed Nov 12 (L)	Run-time enforcement (understanding the power of enforcement mechanisms) [PDF]	Schneider, Enforceable security policies, TISSEC 2000.
Mon Nov 17 (L)	Run-time enforcement (implementing enforcement mechanisms) [PDF]	Erlingsson and Schneider, SASI enforcement of security policies, NSPW 1999. Bauer, Ligatti, and Walker, Composing security policies with Polymer, PLDI 2005.
Wed Nov 19 (L)	Web attacks and defenses [PDF]	Jim, Swamy, and Hicks, Defeating script injection attacks with browser-enforced embedded policies, WWW 2007.
Mon Nov 24 (A)	Run-time enforcement (CFI) [PDF]	Abadi et al., Control-Flow Integrity: Principles, Implementations, and Applications, TISSEC (To appear).
Wed Nov 26	No class—university holiday
Mon Dec 1	Wrap-up [PDF]
Wed Dec 3	Final exam