18-732 — Spring 2021 — Tentative Schedule & Readings

Back to Main Course Page


Check back regularly for updates.


unit date topic instr. reading notes
Introduction
2/1/21 Introduction BP
Classic Attacks
2/3/21 Web attacks BP [Tools and Jewels] Ch. 9 (Portions on HTTP proxies, as well as 9.8 onwards, are optional)    Optional: [Jim+07]    HW1 out
2/8/21 Attacks: buffer overflows, format string vulns, ... BP [Cowan+03]    [Blexim+02]    [teso01]    Optional: [Szerkeres13]    Optional: [Petsios15]    Optional: [Bittau14]    Optional: [AlephOne]    Optional: [Erlingsson07]   
Run-time Protection
2/10/21 Dynamic taint tracking BP [Schwartz2010all]    Optional: [Newsome05ndss]    Optional: [TaintDroid]   
2/15/21 Control-Flow Integrity (CFI) BP [Abadi+09]    
2/17/21 Run-time enforcement: enforceable properties BP [Schneider00]    
2/18/21 Homework 1 due at 5pm
2/19/21 Crypto review for HW2 BP
2/22/21 Run-time enforcement: enforceable properties (continued) BP
Code analysis
2/24/21 Fuzzing BP Optional: [Woo2013fuzzing]    Optional: [Skyfire]   
3/1/21 Static analysis BP [Engler+00]    [Ganapathy2003buffer]    Optional: [Bessey+10]   
3/3/21 Symbolic execution BP [Schwartz2010all]    [Godef+05]    Optional: [Cadar+06]   
3/4/21 Homework 2a checkpoint 5pm
3/5/21 Exam Review Session BP
3/08/21 Software model checking BP [Clarke+04]    Optional: [Vasud+13]   
3/10/21 Exam 1
Architecture
3/15/21 Separation Mechanisms BP [Saltzer+75]    Optional: [Wahbe+94]    Optional: [GR+03]    Homework 2a due 2pm
3/17/21 Separation Challenges BP [Lamp73]    
3/19/21 University holiday -- No Recitation
3/22/21 Separation Policies BP [Roesner12]    Optional: [JAF+13]    Optional: [Acar+16]   
3/24/21 Trusted computing BP [Parno+10]    [Sailer+04]    [McCun+08]    Optional: [McCun+10]   
Languages
3/29/21 Programmer assisted verification - Part 1 BP [Program Proofs] Ch 2 (skipping 2.3.4 and 2.7-2.12)    
3/30/21 Homework 2b due 10pm
3/31/21 Programmer assisted verification - Part 2 BP [Program Proofs] Ch 1, Ch 11, 13.0, 13.1     HW3 out
4/5/21 University Holiday - No Class
4/7/21 Type systems BP [Program Proofs] Ch 4 (skipping 4.3, 4.5) and Ch 5.1-5.2, 5.8     Homework 2c due 2pm
4/9/21 Exam Review Session BP
4/12/21 Exam 2
4/14/21 Type systems (cont'd) + non-interference BP [Ryan01]    [Volpano+96]    [Denning+77]    
4/16/21 University Holiday - No Recitation
4/19/21 Non-interference (cont'd) BP
4/21/21 Typed assembly language BP [MCG+99]    
4/26/21 WebAssembly BP [Haas2017]    Optional: [Watt2018]   
Usability
4/28/21 Usable security BP
4/30/21 Homework 3 due at 5pm
5/3/21 Wrap up and review BP
5/5/21 Exam 3
Instructors: BP = Prof. Bryan Parno

[Tools and Jewels]Computer security and the internet: tools and jewels.
Paul van Oorschot.
2019.
[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.
[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.
[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.
[Newsome05ndss]Dynamic taint analysis for automatic detection, analysis, and signature generation of exploits on commodity software.
Newsome James and Song Dawn.
In NDSS, 2005.
[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.
[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.
[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.
[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.
[GR+03]A virtual machine introspection based architecture for intrusion detection..
Garfinkel Tal, Rosenblum Mendel and others.
In NDSS, pages 191–206, 2003.
[Lamp73]A note on the confinement problem.
Butler Lampson.
In CACM, 1973.
[Roesner12]User-driven access control: rethinking permission granting in modern operating systems.
Roesner Franziska, Kohno Tadayoshi, Moshchuk Alexandee, Parno Bryan, Wang Helen J., and Cowan Crispin.
In Proceedings of the IEEE Symposium on Security and Privacy (Oakland), 2012.
[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.
[Program Proofs]Program proofs.
Rustan Leino.
2020.
[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.