18-732 Spring 2015 Schedule
(Subject to change)
date topic inst. reading notes
13 Jan Introduction   CMU Computing Policy
CMU Policy on Cheating
15 Jan System model: Source code to execution      
20 Jan Attacks: Buffer overflows, format-string vulnerabilities, and other attacks   [Cowan+03, blexim02, teso01]
Optional: [AlephOne, Erlingsson07]
assignment 1 out
22 Jan Basic building blocks: separation, memory protection   [Saltzer+75]
Optional: [Wahbe+94]
27 Jan Basic building blocks: VMs, Java sandboxing LBSV [MR99] Optional: [GM03]  
29 Jan Isolation and confinement in Android      
3 Feb Control-flow integrity   [Abadi+09]  
5 Feb Run-time enforcement: enforceable properties YM [Schneider00] assignment 1 due
10 Feb exam 1      
12 Feb Web attacks LBSV Optional: [Jim+07] assignment 2 out
17 Feb Web defenses: Native client, app isolation   [Chen+11] Optional: [Ansel+11, Yee+09]  
19 Feb Crypto overview; software security architectures: Trusted Computing   [Parno+10, Sailer+04]  
24 Feb Software security architectures: Trusted Computing   [McCun+08]
Optional: [McCun+10]
assignment 2 due
26 Feb Static analysis: metacompilation   [Bessey+10, Engler+00]  
3 Mar Dynamic analysis   [Godef+05, Cadar+06]  
5 Mar Software model checking   [Clarke+04] Optional: [Vasud+13] assignment 3 out
10 Mar spring break      
12 Mar spring break      
17 Mar Software model checking BU    
19 Mar Programmer-assisted verification: SPARK WR   assignment 3 due
24 Mar exam 2      
26 Mar Building verifiable systems: seL4, hypervisors LJ [K+09, Vasud+13] assignment 4 out
31 Mar Language-based security: type systems      
2 Apr Language-based security: noninterference   [Ryan01, Volpano+96, Denning+77]  
7 Apr Noninterference (cont'd); Dynamic taint analysis   Optional: [Enck+10] assignment 4 due
9 Apr Security and usability (part 1)      
14 Apr Security and usability (part 2)     assignment 5 out
16 Apr no class; spring carnival weekend      
21 Apr Language-based security: security-typed languages WR    
23 Apr Language-based security: typed assembly language   [MCG+99]  
28 Apr wrap up + review     assignment 5 due
30 Apr exam 3      
Unless otherwise marked, lectures will be delivered by Lujo Bauer and will be taught from Pittsburgh.
LBSV = Lujo @ SV campus; LJ = Limin Jia; YM = Yannis Mallios; WR = Willard Rafnsson; RR = Rob Reeder; BU = Blase Ur
[ABEL09] M. Abadi, M. Budiu, U. Erlingsson, and J. Ligatti. Control-Flow Integrity: Principles, implementations, and applications. ACM TISSEC, 2009.
[AlephOne] Aleph One. Smashing the stack for fun and profit. Phrack, Vol. 7 Issue 49.
[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.
[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-7
[blexim02] blexim. Basic integer overflows. Phrack, Num. 60, Dec. 2002 (Sections 1-3)
[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.
[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.
[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, 2004
[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.
[Denning+77] D. E. Denning and P. J. Denning. Certification of programs for secure information flow. Commun. ACM, 20, 7, 504-513. 1977.
[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 des
[Engler+00] D. Engler, B. Chelf, A. Chou, and S. Hallem. Checking system rules using system-specific, programmer-written compiler extensions. In Proc. OSDI, 2000
[Erling07] . Erlingsson. Low-Level software security: Attacks and defenses. FOSAD 2007: 92-134
[GR03] T. Garfinkel and M. Rosenblum. A virtual machine introspection based architecture for intrusion detection. In Proc. NDSS, 2003.
[Godef+05] P. Godefroid, N. Klarlund, and K. Sen. DART: Directed automated random testing. In Proc. PLDI, 2005.
[Jim+07] T. Jim, N. Swamy, and M. Hicks. Defeating script injection attacks with browser-enforced embedded policies. In Proc. WWW, 2007.
[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.
[MCG+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 assembly language. In Workshop on Compiler Support for System Software, 1999.
[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
[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.
[MF99] G. McGraw and E. W. Felten. Securing Java. John Whiley and Sons, 1999. (Chapter 3)
[Parno+10] B. Parno, J. M. McCune, and A. Perrig. Bootstrapping trust in commodity computers. In Proc. IEEE Security & Privacy, 2010
[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.
[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
[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.
[Schneider00] F. Schneider. Enforceable security policies. ACM TISSEC, 2000.
[teso01] team teso. Exploiting format string vulnerabilities. Sept. 2001. (Sections 1-3)
[Vasud+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 Proc IEEE Symposium on Security and Privacy, 2013.
[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.
[Wahbe+94] R. Wahbe, S. Lucco, T. E. Anderson, and S. L. Graham. Efficent software-based fault isolation. In Proc. SOSP, 1994.
[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.