| 18-732 • Secure Software Systems • Spring 2013 | |||||
| Schedule (subject to change) | |||||
| Date | Topic | Inst | Reading | Notes | |
| 1 | 14-Jan | Introduction [pdf] | B,D | CMU Computing Policy CMU Policy on Cheating |
|
| 2 | 16-Jan | System model: Source code to execution [pdf] | B | ||
| 3 | 21-Jan | Attacks: Buffer overflows, format-string vulnerabilities, and other attacks [pdf] | B | [Cowan+03, blexim02, teso01] Optional: [AlephOne, Erlingsson07] |
assignment 1 out |
| 4 | 23-Jan | Basic building blocks: separation, memory protection [pdf] | D | [Saltzer+75] Optional: [Wahbe+94] |
|
| 5 | 28-Jan | Basic building blocks: VMs, Java sandboxing [pdf] | B | [Garfinkel+03, McGraw+99] | |
| 6 | 30-Jan | Isolation and confinement in Android [pdf] | B | ||
| 7 | 4-Feb | Control-flow integrity [pdf] | D | [Abadi+09] | |
| 8 | 6-Feb | Run-time enforcement: enforceable properties [pdf] | B | [Schneider00] | assignment 1 due |
| 9 | 11-Feb | Web attacks [pdf] | B | [Jim+07] | |
| 10 | 13-Feb | exam 1 | assignment 2 out (Feb 15) | ||
| 11 | 18-Feb | Web defenses: Native client, app isolation [pdf] | D | [Ansel+11, Chen+11, Yee+09] | |
| 12 | 20-Feb | Crypto overview [pdf]; software security architectures: Trusted Computing | D | [Parno+10, Sailer+04] | |
| 13 | 25-Feb | Software security architectures: Trusted Computing + policy | D | [McCun+08] Optional: [McCun+10] |
assignment 2 due |
| 14 | 27-Feb | Static analysis: C programs | D | [Bessey+10, Engler+00] | |
| 15 | 4-Mar | Static analysis: web applications | J | [Taly+11] | assignment 3 out |
| 16 | 6-Mar | Static analysis: malware | D | [Chris+05] | |
| 11-Mar | Spring break | ||||
| 13-Mar | |||||
| 17 | 18-Mar | Dynamic analysis | B | [Godef+05, Cadar+06] | |
| 18 | 20-Mar | Software model checking | D | [Chaki+04] | assignment 3 due |
| 19 | 25-Mar | Software model checking | D | [Chaki+08] | |
| 20 | 27-Mar | exam 2 | |||
| 21 | 1-Apr | Software model checking | C | [Clarke+04, Vasudevan+13] | assignment 4 out (3/29) |
| 22 | 3-Apr | Building verifiable systems: seL4, browsers | J | [K+09, JTL12] | |
| 23 | 8-Apr | Language-based security: type systems | B | ||
| 24 | 10-Apr | Language-based security: typed assembly language | B | [M+99] | assignment 4 due |
| 25 | 15-Apr | Language-based security: noninterference | D | [Ryan01, Volpano+96, Denning+77]; | assignment 5 out (4/12) |
| Dynamic taint analysis | Optional: [Enck+10] | ||||
| 26 | 17-Apr | Language-based security: security-typed languages | B | ||
| 27 | 22-Apr | Usability in software security | B | ||
| 28 | 24-Apr | Usable Security: Passwords (Part 1) | B | assignment 5 due | |
| Usable Security: Passwords (Part 2) | D | [Blocki+13] | |||
| 29 | 29-Apr | Wrap-up | |||
| 30 | 1-May | exam 3 | |||
| Lectures taught by: (B) Lujo Bauer, (D) Anupam Datta, (C) Sager Chaki (guest lecturer), (J) Limin Jia (guest lecturer) | |||||
| Readings | |||||
| [Abadi+09] | M. Abadi, M. Budiu, U. Erlingsson, and J. Ligatti. Control-Flow Integrity: Principles, implementations, and applications. ACM TISSEC, 2009. | link | |||
| [AlephOne] | Aleph One. Smashing the stack for fun and profit. Phrack, Vol. 7 Issue 49. | link | |||
| [Ansel+11] | J. Ansel, P. Marchenko, Ú. Erlingsson, E. Taylor, B. Chen, D. L. Schuff, D. Sehr, C.L. Biffle, and B. Yee. Language-independent sandboxing of just-in-time compilation and self-modifying code. SIGPLAN Not. 46, 6 (June 2011), 355-366. 2011. | link | |||
| [Bessey+10] | A. Bessey, K. Block, B. Chelf, A. Chou, B. Fulton, S. Hallem, C. Henri-Gros, A. Kamsky, S. McPeak, and D. Engler. A few billion lines of code later: using static analysis to find bugs in the real world. Commun. ACM 53, 2 (February 2010), 66-75. | link | |||
| [blexim02] | blexim. Basic integer overflows. Phrack, Num. 60, Dec. 2002 (Sections 1-3) | link | |||
| [Blocki+13] | J. Blocki, M. Blum, and A. Datta. "Naturally-Rehearsing Passwords." arXiv preprint arXiv:1302.5122 (2013). | link | |||
| [Cadar+06] | C. Cadar, V. Ganesh, P. M. Pawlowski, D. L. Dill, and D. R. Engler. EXE: Automatically generating inputs of death. In Proc. CCS, 2006. | link | |||
| [Chaki+04] | S. Chaki, E. Clarke, A. Groce, S. Jha, and H. Veith. Modular verification of software components in C. TSE, 2004. | link | |||
| [Chaki+08] | S. Chaki and A. Datta. ASPIER: An automated framework for verifying security protocol implementations. 2008. | link | |||
| [Chen+04] | H. Chen, D. Dean, and D. Wagner. Model checking one million lines of C code. In Proc. NDSS, 2004. | link | |||
| [Chen+11] | E. Chen, J. Bau, C. Reis, A. Barth, and C. Jackson. App isolation: get the security of multiple browsers with just one. In Proc. ACM CCS 2011. | link | |||
| [Chris+05] | M. Christodorescu, S. Jha, S. A. Seshia, D. Song, and R. E. Bryant. Semantics-aware malware detection. In Proc. IEEE Security & Privacy, 2005. | link | |||
| [Clarke+04] | E. Clarke, D. Kroening, and F. Lerda. A tool for checking ANSI-C programs. In Proceedings of the International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Lecture Notes in Computer Science, vol. 2988, Springer, 168--176, 2004. | link | |||
| [Cowan+03] | C. Cowan, P. Wagle, C. Pu, S. Beattie, and J. Walpole. Buffer overflows: Attacks and defenses for the vulnerability of the decade. In Proc. Foundations of Intrusion Tolerant Systems, 2003. | link | |||
| [Denning+77] | D. E. Denning and P. J. Denning.Certification of programs for secure information flow. Commun. ACM 20, 7 (July 1977), 504-513. 1977. | link | |||
| [Enck+10] | W. Enck, P. Gilbert, B. Chun, L. P. Cox, J. Jung, P. McDaniel, and A. N. Sheth. TaintDroid: an information-flow tracking system for realtime privacy monitoring on smartphones. In Proceedings of the 9th USENIX conference on Operating systems design and implementation (OSDI'10). 2010. | link | |||
| [Engler+00] | D. Engler, B. Chelf, A. Chou, and S. Hallem. Checking system rules using system-specific, programmer-written compiler extensions. In Proceedings of the 4th conference on Symposium on Operating System Design & Implementation - Volume 4 (OSDI'00), 2000. | link | |||
| [Erlin07] | Ú. Erlingsson. Low-Level software security: Attacks and defenses. FOSAD 2007: 92-134 | link | |||
| [Ganap+03] | V. Ganapathy, S. Jha, D. Chandler, D. Melski, and D. Vitek. Buffer overrun detection using linear programming and static analysis. In Proc. CCS, 2003. | link | |||
| [Garfi+03] | T. Garfinkel and M. Rosenblum. A virtual machine introspection based architecture for intrusion detection. In Proc. NDSS, 2003. | link | |||
| [Godef+05] | P. Godefroid, N. Klarlund, and K. Sen. DART: Directed automated random testing. In Proc. PLDI, 2005. | link | |||
| [JTL12] | D. Jang, Z. Tatlock, and S. Lerner. Establishing browser security guarantees through formal shim verification. In Proc. USENIX Security, 2012. | link | |||
| [Jim+07] | T. Jim, N. Swamy, and M. Hicks. Defeating script injection attacks with browser-enforced embedded policies. In Proc. WWW, 2007. | link | |||
| [K+09] | G. Klein, K. Elphinstone, G. Heiser, J. Andronick, D. Cock, P. Derrin, D. Elkaduwe, K. Engelhardt, R. Kolanski, M. Norrish, T. Sewell, H. Tuch, and S. Winwood. seL4: formal verification of an OS kernel. In Proc. SOSP, 2009. | link | |||
| [M+99] | G. Morrisett, K. Crary, N. Glew, D. Grossman, R. Samuels, F. Smith, D. Walker, S. Weirich, and S. Zdancewic. TALx86: A realistic typed assembly language. In Workshop on Compiler Support for System Software, 1999. | link | |||
| [McCun+08] | J. M. McCune, B. Parno, A. Perrig, M. K. Reiter, and H. Izaki. Flicker: An execution infrastructure for TCB minimization. In Proc. EuroSys, 2008. | link | |||
| [McCun+10] | J. M. McCune, Y. Li, N. Qu, Z. Zhou, A. Datta, V. Gligor, and A. Perrig. TrustVisor: Efficient TCB reduction and attestation. In Proc. IEEE Security & Privacy, 2010. | link | |||
| [McGra+99] | G. McGraw and E. W. Felten. Securing Java. John Whiley and Sons, 1999. (Chapter 3) | link | |||
| [Parno+10] | B. Parno, J. M. McCune, and A. Perrig. Bootstrapping trust in commodity computers. In Proc. IEEE Security & Privacy, 2010. | link | |||
| [Ryan01] | P. Ryan. Mathematical Models of Computer Security (Section 5). In Foundations of Security Analysis and Design, Lecture Notes in Computer Science Volume 2171, 2001, pp 1-62. | link | |||
| [Sailer+04] | R. Sailer, X. Zhang, T. Jaeger, and L. van Doorn. Design and implementation of a TCG-based integrity measurement infrastructure. In Proc. USENIX Security, 2004. | link | |||
| [Saltz+75] | J. H. Saltzer and M. D. Schroeder. The protection of information in computer systems. Proceedings of the IEEE. Vol. 63, Issue 9, 1975. | link | |||
| [Schne00] | F. Schneider. Enforceable security policies. ACM TISSEC, 2000. | link | |||
| [Taly+11] | A. Taly, Ú. Erlingsson, J. C. Mitchell, M. S. Miller, and J. Nagra. Automated analysis of security-critical JavaScript APIs. In Proc. IEEE Symposium on Security and Privacy, 2011. | link | |||
| [teso01] | team teso. Exploiting format string vulnerabilities. Sept. 2001. (Sections 1-3) | link | |||
| [Wahbe+94] | R. Wahbe, S. Lucco, T. E. Anderson, and S. L. Graham. Efficent software-based fault isolation. In Proc. SOSP, 1994. | link | |||
| [Vasudevan+13] | A. Vasudevan, S. Chaki, L. Jia, J. McCune, J. Newsome, A. Datta. Design, Implementation and Verification of an eXtensible and Modular Hypervisor Framework, in Proceedings of 34th IEEE Symposium on Security and Privacy, May 2013. | link | |||
| [Volpano+96] | D. Volpano, C. Irvine, and G. Smith. A sound type system for secure flow analysis. J. Comput. Secur. 4, 2-3 (January 1996), 167-187, 1996. | link | |||
| [Yee+09] | B. Yee, D.Sehr, G. Dardyk, J. Bradley Chen, R. Muth, T. Ormandy, S. Okasaka, N. Narula, and N. Fullagar. Native Client: a sandbox for portable, untrusted x86 native code. In Proc. IEEE Security & Privacy, 2009. | link | |||