18-732 — Spring 2018 — Schedule & Readings


Check back regularly for updates to the schedule.


unit date topic instr. reading notes
Introduction
1/16/18 Introduction LB, BP
Classic Attacks
1/18/18 Attacks: buffer overflows, format string vulns, ... BP [Cowan+03] [Blexim+02] [teso01] Optional: [Szerkeres13] Optional: [Petsios15] Optional: [Bittau14] Optional: [AlephOne] Optional: [Erlingsson07] Tentative: HW1 out
1/19/18 Crypto review for HW1 LB
Run-time Protection
1/23/18 Dynamic taint tracking BP [Newsome05ndss] Optional: [Schwartz2010all] Optional: [TaintDroid]
1/25/18 Control-Flow Integrity (CFI) LB [Abadi+09]
1/30/18 CFI continued + Run-time enforcement: enforceable properties LB [Schneider00]
2/1/18 Run-time enforcement: enforceable properties LB
2/2/18 HW1a checkpoint due
Code analysis
2/6/18 Static analysis BP [Engler+00] [Ganapathy2003buffer] Optional: [Bessey+10]
2/8/18 Symbolic execution BP [Schwartz2010all] [Godef+05] Optional: [Cadar+06]
2/9/18 HW1a due
2/13/18 Software model checking BP [Clarke+04] Optional: [Vasud+13]
2/15/18 Exam 1
2/20/18 Fuzzing BP Optional: [Woo2013fuzzing] Optional: [Skyfire]
Architecture
2/22/18 Basic building blocks: separation, memory protection LB [Saltzer+75] Optional: [Wahbe+94]
2/27/18 Basic building blocks: Java sandboxing, VMs LB [MF99] Optional: [GR+03]
3/1/18 Isolation and confinement in Android LB Optional: [JAF+13] Optional: [Acar+16]
3/2/18 HW1b due
3/6/18 Trusted computing LB [Parno+10] [Sailer+04] [McCun+08] Optional: [McCun+10]
3/8/18 Trusted computing (cont'd) LB
Web
3/13/18 spring break
3/15/18 spring break
3/19/18 HW1c due
3/20/18 Web attacks LB Optional: [Jim+07] HW2 out
3/22/18 Web defenses: native client, app isolation LB [Chen+11] [Yee+09] Optional: [Ansel+11]
3/27/18 Pre-exam review BP
3/29/18 Exam 2
4/2/18 HW2 due
Languages
4/3/18 Programmer assisted verification BP [Leino2010 Dafny] HW3 out
4/5/18 Type systems BP
4/10/18 Type systems (cont'd) + non-interference LB [Ryan01] [Volpano+96] [Denning+77]
4/12/18 Non-interference (cont'd) LB
4/17/18 Typed assembly language BP [MCG+99]
4/19/18 No class, Spring carnival
4/24/18 WebAssembly BP [Haas2017] Optional: [Watt2018]
4/25/18 HW3 due
Usability
4/26/18 Usable security BP
5/1/18 Wrap up and review BP
5/3/18 Exam 3
Instructors: LB = Lujo Bauer; BP = Bryan Parno

[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.
[Szerkeres13]Sok: eternal war in memory.
Laszlo Szekeres, Mathias Payer, Tao Wei, and Dawn Song.
In Proceedings of the IEEE Symposium on Security and Privacy, 2013.
[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.
[Newsome05ndss]Dynamic taint analysis for automatic detection, analysis, and signature generation of exploits on commodity software.
Newsome James and Song Dawn.
In NDSS, 2005.
[Schwartz2010all]All you ever wanted to know about dynamic taint analysis and forward symbolic execution (but might have been afraid to ask).
Schwartz Edward J., Avgerinos Thanassis and Brumley David.
In Proceedings of the 2010 IEEE Symposium on Security and Privacy, pages 317–331, 2010. IEEE Computer Society.
[TaintDroid]Taintdroid: an information-flow tracking system for realtime privacy monitoring on smartphones.
Enck William, Gilbert Peter, Han Seungyeop, Tendulkar Vasant, Chun Byung-Gon, Cox Landon P., Jung Jaeyeon, McDaniel Patrick, and Sheth Anmol N..
ACM Trans. Comput. Syst., 32(2):5:1–5:29, June 2014. ACM.
[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.
[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.
[Ganapathy2003buffer]Buffer overrun detection using linear programming and static analysis.
Vinod Ganapathy, Somesh Jha, David Chandler, David Melski, and David Vitek.
In CCS, 2003.
[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.
[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.
[Woo2013fuzzing]Scheduling black-box mutational fuzzing.
Maverick Woo, Sang Kil Cha, Samantha Gottlieb, and David Brumley.
In CCS, 2013.
[Skyfire]Skyfire: data-driven seed generation for fuzzing.
J. Wang, B. Chen, L. Wei, and Y. Liu.
In 2017 IEEE Symposium on Security and Privacy (SP), pages 579-594, 2017.
[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
[Acar+16]Sok: lessons learned from android security research for appified software platforms.
Yasemin Acar, Michael Backes, Sven Bugiel, Sascha Fahl, Patrick McDaniel, and Matthew Smith.
In Proceedings of the IEEE Symposium on Security and Privacy, 2016.
[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.
[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.
[Leino2010 Dafny]Dafny: an automatic program verifier for functional correctness.
Leino K. Rustan M..
In Proceedings of the Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR), 2010.
[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.
[Haas2017]Bringing the web up to speed with webassembly.
Haas Andreas, Rossberg Andreas, Schuff Derek L., Titzer Ben L., Holman Michael, Gohman Dan, Wagner Luke, Zakai Alon, and Bastien JF.
In PLDI, 2017.
[Watt2018]Mechanising and verifying the webassembly specification.
Conrad Watt.
In CPP, 2018.