18-732 — Spring 2017 — Schedule & Readings


Check back regularly for updates to the schedule.


unit date topic instr. reading notes
Introduction
1/17/17 Introduction LB
Attacks
1/19/17 System model: Source code to execution MW
1/24/17 Attacks: buffer overflows, format string, ... LB [Cowan+03] [Blexim+02] [teso01] Optional: [Petsios15] Optional: [Bittau14] Optional: [AlephOne] Optional: [Erlingsson07]
Architecture
1/26/17 Basic building blocks: separation, memory protection LB [Saltzer+75] Optional: [Wahbe+94] Tentative: HW1 out
1/31/17 Basic building blocks: Java sandboxing, VMs LB [MF99] Optional: [GR+03]
2/2/17 Isolation and confinement in Android LB Optional: [JAF+13]
Run-time
2/7/17 Control-flow integrity MW [Abadi+09]
2/9/17 CFI continued + Run-time enforcement: enforceable properties MW + LB [Schneider00] Tentative: HW1 due
2/14/17 Run-time enforcement: enforceable properties LB
2/16/17 Exam 1
Attacks
2/21/17 Web attacks LB Optional: [Jim+07] Tentative: HW2 out
2/23/17 Web defenses: native client, app isolation LB [Chen+11] [Yee+09] Optional: [Ansel+11]
Architecture
2/28/17 Trusted computing BP [Parno+10] [Sailer+04] [McCun+08] Optional: [McCun+10]
Analysis
3/2/17 Static analysis LB [Bessey+10]
3/7/17 Symbolic execution [Engler+00] [Godef+05] [Cadar+06] Tentative: HW2 due
3/9/17 Software model checking LB [Clarke+04] Optional: [Vasud+13] Tentative: HW3 out
3/14/17 spring break
3/16/17 spring break
3/21/17 Fuzzing MW
3/23/17 Pre-exam review LB
3/28/17 Exam 2
Languages
3/30/17 Programmer assisted verification LB HW3 due
4/4/17 Type systems MF
4/6/17 Type systems (cont'd) + non-interference LJ [Ryan01] [Volpano+96] [Denning+77] Tentative HW4 out
4/11/17 Non-interference (cont'd) LB
4/13/17 Non-interference (cont'd) LB Tentative: HW4 due
4/14/17 Dynamic taint tracking LB
4/18/17 Typed assembly language LB [MCG+99] Tentative: HW5 out
4/20/17 No class, Spring carnival LB
4/25/17 Usable security LB
4/27/17 Secure software systems in practice: a Googler's perspective II Tentative: HW5 due
5/2/17 Wrap up and review LB
5/4/17 Exam 3
Instructors: LB = Lujo Bauer; MW = Maverick Woo; BP = Bryan Parno; II = Iulia Ion; MF = Matt Fredrikson; LJ = Limin Jia

[Cowan+03]Buffer overflows: attacks and defenses for the vulnerability of the decade.
Cowan Crispin, Wagle Perry, Pu Calton, Beattie Steve, and Walpole Jonathan.
In DISCEX '00, volume 2 of DISCEX '00, pages 119–129, 2000. IEEE.
[Blexim+02]Basic integer overflows.
blexim.
Phrack, 2002. Sections 1-3
[teso01]Exploiting format string vulnerabilities.
teso.
Phrack, September 2001.
[Petsios15]Dynaguard: armoring canary-based protections against brute-force attacks.
Theofilos Petsios, Vasileios P. Kemerlis, Michalis Polychronakis, and Angelos D. Keromytis.
In Proceedings of the 31st Annual Computer Security Applications Conference, pages 351–360, 2015. ACM.
[Bittau14]Hacking blind.
Andrea Bittau, Adam Belay, Ali Mashtizadeh, David Mazières, and Dan Boneh.
In Proceedings of the 2014 IEEE Symposium on Security and Privacy, pages 227–242, 2014. IEEE Computer Society.
[AlephOne]Smashing the stack for fun and profit.
Aleph One.
1996.
[Erlingsson07]Low-level software security: attacks and defenses.
Úlfar Erlingsson.
In Foundations of Security Analysis and Design IV, volume 4677 of Lecture Notes in Computer Science, pages 92-134, 2007. Springer Berlin Heidelberg.
[Saltzer+75]The protection of information in computer systems.
J.H. Saltzer and M.D. Schroeder.
Proceedings of the IEEE, 63(9):1278-1308, 1975.
[Wahbe+94]Efficient software-based fault isolation.
Wahbe Robert, Lucco Steven, Anderson Thomas E., and Graham Susan L..
In Proceedings of the Fourteenth ACM Symposium on Operating Systems Principles, pages 203–216, 1993. ACM.
[MF99]Securing Java.
G. McGraw and E. W. Felten.
Chapter 3
1999. John Whiley and Sons.
[GR+03]A virtual machine introspection based architecture for intrusion detection..
Garfinkel Tal, Rosenblum Mendel and others.
In NDSS, pages 191–206, 2003.
[JAF+13]Run-time enforcement of information-flow properties on Android (extended abstract).
Limin Jia, Jassim Aljuraidan, Elli Fragkaki, Lujo Bauer, Michael Stroucken, Kazuhide Fukushima, Shinsaku Kiyomoto, and Yutaka Miyake.
In Computer Security—ESORICS 2013: 18th European Symposium on Research in Computer Security, pages 775–792, September 2013. Springer. (Full version appears as technical report CMU-CyLab-12-015.) © Springer-Verlag  DOI:10.1007/978-3-642-40203-6_43
[Abadi+09]Control-flow integrity principles, implementations, and applications.
Martín Abadi, Mihai Budiu, Úlfar Erlingsson, and Jay Ligatti.
ACM Trans. Inf. Syst. Secur., 13(1):4:1–4:40, November 2009. ACM.
[Schneider00]Enforceable security policies.
Fred B. Schneider.
ACM Trans. Inf. Syst. Secur., 3(1):30–50, February 2000. ACM.
[Jim+07]Defeating script injection attacks with browser-enforced embedded policies.
Trevor Jim, Nikhil Swamy and Michael Hicks.
In Proceedings of the 16th International Conference on World Wide Web, pages 601–610, 2007. ACM.
[Chen+11]App isolation: get the security of multiple browsers with just one.
Eric Yawei Chen, Jason Bau, Charles Reis, Adam Barth, and Collin Jackson.
In Proceedings of the 18th ACM conference on Computer and communications security, pages 227–238, 2011.
[Yee+09]Native client: a sandbox for portable, untrusted x86 native code.
Yee Bennet, Sehr David, Dardyk Gregory, Chen J Bradley, Muth Robert, Ormandy Tavis, Okasaka Shiki, Narula Neha, and Fullagar Nicholas.
In Security and Privacy, 2009 30th IEEE Symposium on, pages 79–93, 2009.
[Ansel+11]Language-independent sandboxing of just-in-time compilation and self-modifying code.
Jason Ansel, Petr Marchenko, Úlfar Erlingsson, Elijah Taylor, Brad Chen, Derek L. Schuff, David Sehr, Cliff L. Biffle, and Bennet Yee.
SIGPLAN Not., 46(6):355–366, June 2011. ACM.
[Parno+10]Bootstrapping trust in commodity computers.
B. Parno, J.M. McCune and A. Perrig.
In Security and Privacy (SP), 2010 IEEE Symposium on, pages 414-429, 2010.
[Sailer+04]Design and implementation of a tcg-based integrity measurement architecture..
Reiner Sailer, Xiaolan Zhang, Trent Jaeger, and Leendert Van Doorn.
In Proc.\ USENIX, 2004.
[McCun+08]Flicker: an execution infrastructure for tcb minimization.
McCune Jonathan M., Parno Bryan J., Perrig Adrian, Reiter Michael K., and Isozaki Hiroshi.
In Proceedings of the 3rd ACM SIGOPS/EuroSys European Conference on Computer Systems 2008, pages 315–328, 2008. ACM.
[McCun+10]Trustvisor: efficient tcb reduction and attestation.
J.M. McCune, Yanlin Li, Ning Qu, Zongwei Zhou, A. Datta, V. Gligor, and A. Perrig.
In Security and Privacy (SP), 2010 IEEE Symposium on, pages 143-158, 2010.
[Bessey+10]A few billion lines of code later: using static analysis to find bugs in the real world.
Al Bessey, Ken Block, Ben Chelf, Andy Chou, Bryan Fulton, Seth Hallem, Charles Henri-Gros, Asya Kamsky, Scott McPeak, and Dawson Engler.
Commun. ACM, 53(2):66–75, February 2010. ACM.
[Engler+00]Checking system rules using system-specific, programmer-written compiler extensions.
Dawson Engler, Benjamin Chelf, Andy Chou, and Seth Hallem.
In Proceedings of the 4th Conference on Symposium on Operating System Design \& Implementation - Volume 4, pages 1–1, 2000. USENIX Association.
[Godef+05]Dart: directed automated random testing.
Patrice Godefroid, Nils Klarlund and Koushik Sen.
In ACM Sigplan Notices, pages 213–223, 2005.
[Cadar+06]Exe: automatically generating inputs of death.
Cadar Cristian, Ganesh Vijay, Pawlowski Peter M., Dill David L., and Engler Dawson R..
In Proceedings of the 13th ACM Conference on Computer and Communications Security, pages 322–335, 2006. ACM.
[Clarke+04]A tool for checking ansi-c programs.
Edmund Clarke, Daniel Kroening and Flavio Lerda.
In Tools and Algorithms for the Construction and Analysis of Systems, volume 2988 of Lecture Notes in Computer Science, pages 168-176, 2004. Springer Berlin Heidelberg.
[Vasud+13]Design, implementation and verification of an extensible and modular hypervisor framework.
Amit Vasudevan, Sagar Chaki, Limin Jia, Jonathan McCune, James Newsome, and Anupam Datta.
In Proceedings of the 2013 IEEE Symposium on Security and Privacy, pages 430–444, 2013. IEEE Computer Society.
[Ryan01]Mathematical models of computer security.
Peter Y.A. Ryan.
In Foundations of Security Analysis and Design, volume 2171 of Lecture Notes in Computer Science, pages 1-62, 2001. Springer Berlin Heidelberg.
[Volpano+96]A sound type system for secure flow analysis.
Dennis Volpano, Cynthia Irvine and Geoffrey Smith.
J. Comput. Secur., 4(2-3):167–187, January 1996. IOS Press.
[Denning+77]Certification of programs for secure information flow.
Dorothy E. Denning and Peter J. Denning.
Commun. ACM, 20(7):504–513, July 1977. ACM.
[MCG+99]Talx86: a realistic typed assembly language.
K Crary, Neal Glew, Dan Grossman, Richard Samuels, F Smith, D Walker, S Weirich, and S Zdancewic.
In 1999 ACM SIGPLAN Workshop on Compiler Support for System Software Atlanta, GA, USA, pages 25–35, 1999.