Course Components
Each week, you will be responsible for reviewing one of the required readings (if there are any). Reviews are typically due Sunday at midnight via the course HotCRP site (linked from Canvas) so discussion leads have time to read them before the Tuesday class.
Except where otherwise noted, discussions will be led by one or two students. Everyone should read the required readings, but discussion leads should also read all of the on-time reviews (i.e., you are not responsible for reading anything submitted at the last minute) to be prepared to lead a discussion.
There will also be opportunities to participate during lectures, so be sure to attend class!
The final project will be an opportunity to explore additional topics in formal methods and/or usable security or propose your own research project in usable formal methods. More details will be posted soon.
Schedule
This a tentative course schedule. It may change over the course of the semester, so be sure to check back here before starting on any assigned readings. Some of the materials for this course have been borrowed and/or adapted from content developed by Professors Lorrie Cranor, Limin Jia, and Hanan Hibshi at Carnegie Mellon University.
Unit 0: Course Intro
Week 1
8/25 Course Overview
Syllabus, classroom expectations, course motivation
Required Reading:
1. Thoughts on Reviewing, Mark Allman
2. Notes on Constructive and Positive Reviewing, Mark Hill and Kathryn S McKinley
Unit 1: Security and Privacy
Week 1 (continued)
8/27 Threats and Attackers
Threat modeling, STRIDE, hacking humans
How to write reviews and lead a discussion
Required Reading:
1. Why Cryptosystems Fail. Ross Anderson (CCS ‘93)
2. A Framework for Reasoning About the Human in the Loop. Lorrie Faith Cranor (UPSEC ‘08)
Due this week:
Bid on papers on HotCRP due 8/30 at midnight (you’ll receive an invitation by email)
Review 1 on required reading from 8/17 lecture due 8/30 at midnight
Week 2
9/1 Discussion 1
Discussion lead: McKenna
9/3 Security and Privacy Goals and Metrics
Information security properties, usable security metrics, side & covert channels
Required Reading:
1. Hertzbleed: Turning Power Side-Channel Attacks Into Remote Timing Attacks on x86. Yingchen Wang, Riccardo Paccagnella, Elizabeth Ta ng He, Hovav Shacham, Christopher W. Fletcher, and David Kohlbrenner (USENIX Security ‘22)
2. Is it a concern or a preference? An investigation into the ability of privacy scales to capture and distinguish granular privacy constructs. Jessica Colnago, Lorrie Faith Cranor, Alessandro Acquisti, and Kate Hazel Stanton (SOUPS ‘22)
Optional Reading:
1. Chapters 1.1-1.2, 1.4 of Handbook of Applied Cryptography. Alfred J. Menezes, Paul C. van Oorschot and Scott A. Vanstone
2. Chapters 5.2-5.2.2 (before 5.2.2.1) of An Introduction to Privacy for Technology Professionals. Florian Schaub and Lorrie Faith Cranor
3. Investigating Influencer VPN Ads on YouTube. Omer Akgul, Richard Roberts, Moses Namara, Dave Levin, and Michelle L. Mazurek (IEEE S&P ’22)
4. Spectre attacks: exploiting speculative execution. Paul Kocher, Jann Horn, Anders Fogh, Daniel Genkin, Daniel Gruss, Werner Haas, Mike Hamburg, Moritz Lipp, Stefan Mangard, Thomas Prescher, Michael Schwarz, and Yuval Yarom. Communications of the ACM, 63(7), 2020
5. The privacy paradox – Investigating discrepancies between expressed privacy concerns and actual online behavior – A systematic literature review. Susanne Barth and Menno D.T. de Jong. Telematics and informatics, 34(7), 2017
Due this week:
Review 2 on required reading from 9/3 lecture due 9/6 at midnight
Week 3
9/8 Discussion 2
Discussion lead: Student
9/10 Introduction to Cryptography
Terminology, symmetric and public key algorithms
Course Project overview
Optional Reading:
1. Chapter 1 (through 1.9) of Handbook of Applied Cryptography, Alfred J. Menezes, Paul C. van Oorschot and Scott A. Vanstone
2. Prudent Engineering Practice for Cryptographic Protocols, Martín Abadi and Roger Needham
Due this week:
No reviews due this week
Week 4
9/15 Applications of Cryptography
Security Protocols
Unit 2: Formal Methods
Week 4 (continued)
9/17 Introduction to Formal Methods
Static and dynamic analysis
Optional Reading:
1. Proving the Correctness of Multiprocess Programs. Leslie Lamport (IEEE Trans. On Software Engineering ‘77)
2. A High-Level View of TLA+. Leslie Lamport
Due this week:
Project proposals due 9/20 at midnight
No reviews due this week
Week 5
9/22 Model Checking:
Finite state machines, safety and liveness properties
9/24 Type Systems and Program Semantics
Noninterference, information flow control
Required Reading:
1. Reactive Noninterference. Aaron Bohannon, Benjamin C. Pierce, Vilhelm Sjöberg, Stephanie Weirich, and Steve Zdancewic (CCS ’09)
2. Noninterference Through Secure Multi-Execution. Dominique Devriese and Frank Piessens (IEEE S&P ‘10)
Optional Reading:
1. A Lattice Model of Secure Information Flow. Dorothy E. Denning (Comm. of the ACM ’76)
2. Dynamic vs. Static Flow-Sensitive Security Analysis. Alejandro Russo and Andrei Sabelfeld (CSF ‘10)
Due this week:
Review 3 on required reading from 9/24 lecture due 9/27 at midnight
Week 6
9/29 Discussion 3
Discussion lead: Student
10/1 Applications of formal methods:
Optional Reading:
TBD
Due this week:
No reviews due this week
Project check-in 1 due 10/4 at midnight
Unit 3: Usable Security
Week 7
10/6 Introduction to Usable Security
What is “usable”?, parts of a usable security study
Optional Reading:
1. Why Johnny Can’t Encrypt: A Usability Evaluation of PGP 5.0. Alma Whitten and J.D. Tygar (USENIX Security ‘99)
2. “You do understand that people don’t trust technology?”: Explaining Trusted Execution Environments to Non-Experts. McKenna McCall, Carolina Carreira, Miguel Flores, and Lorrie Faith Cranor
3. Chapters 2.1, 2.3, 3.1-3.3, and 3.6 of Research Methods in Human-Computer Interaction. Jonathan Lazar, Jinjuan Heidi Feng, and Harry Hochheiser
10/8 Surveys and Interviews
Pros, cons, and development
Required Reading:
1. Evaluating the Usability of Privacy Choice Mechanisms. Hana Habib and Lorrie Faith Cranor (SOUPS ‘22)
2. Do Users Write More Insecure Code with AI Assistants? Neil Perry, Megha Srivastava, Deepak Kumar, and Dan Boneh (CCS ’23)
Optional Reading:
1. Chapters 5.2-5.3, 5.6, 8.2, and 8.6 of Research Methods in Human-Computer Interaction. Jonathan Lazar, Jinjuan Heidi Feng, and Harry Hochheiser
Due this week:
Review 4 on required reading from 10/8 lecture due 10/11 at midnight
Week 8
10/13 Discussion 4
Discussion lead: Student
10/15 Quantitative Analysis
Goals, null hypotheses, how to choose a statistic
Required Reading:
1. Misuse, Misreporting, Misinterpretation of Statistical Methods in Usable Privacy and Security Papers. Jenny Tang, Lujo Bauer, and Nicolas Christin (SOUPS ‘25)
Due this week:
Review 5 on required reading from 10/15 lecture due 10/18 at midnight
Project check-in 2 due 10/18 at midnight
Week 9
10/20 Discussion 5
Discussion lead: Student
10/22 Qualitative Analysis
Goals, codebooks and coding
Required Reading:
1. SoK: The Design Space of Usable Privacy Interventions for Parents: A Systemization of Knowledge. Ann-Kristin Lieberknecht, and Sascha Loebner (SOUPS ’26)
2. Speculative Privacy Concerns about AR Glasses Data Collection. Andrea Gallardo, Chris Choy, Jaideep Juneja, Efe Bozkir, Camille Cobb, Lujo Bauer, and Lorrie Cranor. PoPETS 2023 (4).
Optional Reading:
1. Reliability and Inter-rater Reliability in Qualitative Research: Norms and Guidelines for CSCW and HCI Practice. Nora McDonald, Sarita Scfhoenebeck, and Andrea Forte (CSCW ’19)
Due this week:
Review 6 on required reading from 10/22 lecture due 10/25 at midnight
Week 10
10/27 Discussion 6
Discussion lead: Student
Unit 4: Usability in Formal Methods
Week 10 (continued)
10/29 Smart Homes
Required Reading:
1. AutoTap: Synthesizing and Repairing Trigger-Action Programs Using LTL Properties. Lefan Zhang, Weijia He, Jesse Martinez, Noah Brackenbury, Shan Lu, Blase Ur (ICSE ’19)
2. Location-Enhanced Information Flow for Home Automations. McKenna McCall, Ben Weinshel, Kunlin Cai, Ying Li, Eric Zeng, Devika Manohar, Lujo Bauer, Limin Jia, and Yuan Tian. PoPETS 2026 (1)
Optional Reading:
1. How Risky are Real Users’ IFTTT Applets? Camille Cobb, Milijana Surbatovich, Anna Kawakami, Mahmood Sharif, Lujo Bauer, Anupam Das, and Limin Jia (SOUPS ‘20)
Due this week:
Review 7 on required reading from 10/29 lecture due 11/1 at midnight
Project check-in 3 due 11/1 at midnight
Week 11
11/3 Discussion 7
Discussion lead: Student
11/5 Information Flows on the Web
Required Reading:
1. Tainted Secure Multi-Execution to Restrict Attacker Influence. McKenna McCall, Abhishek Bichhawat, and Limin Jia (CCS ‘23)
2. An Empirical Study of Information Flows in Real-World JavaScript. Cristian-Alexandru Staicu, Daniel Schoepe, Musard Balliu, Michael Pradel, Andrei Sabelfeld (PLDI ‘19)
Due this week:
Review 8 on required reading from 11/5 lecture due 11/8 at midnight
Week 12
11/10 Discussion 8
Discussion lead: Student
Unit 5: Research Ethics and Limitations
Week 12 (continued)
11/12 What is (Ethical) Human Subjects Research?
IRBs, history of research ethics
Required Reading:
1. On the Feasibility of Stealthily Introducing Vulnerabilities in Open-Source Software via Hypocrite Commits. Qiushi Wu and Kangjie Lu
2. Experimental evidence of massive-scale emotional contagion through social networks. Adam DI Kramer, Jamie E Guillory, and Jeffrey T Hancock (PNAS ‘14)
Optional Reading:
1. Skilled or Gullible? Gender Stereotypes Related to Computer Security and Privacy. Miranda Wei, Pardis Emami-Naeini, Franziska Roesner, and Tadayoshi Kohno (IEEE S&P ‘23)
2. The Menlo Report: Ethical Principles Guiding Information and Communication Technology Research. David Dittrich and Erin Kenneally (US Department of Homeland Security ‘12)
Due this week:
Review 9 on required reading from 11/12 lecture due 11/15 at midnight
Project check-in 4 due 11/15 at midnight
Week 13
11/16 Discussion 9
Discussion lead: McKenna
11/18 Limitations of Formal Methods and Usable Security
Revisiting attacker models and side channels, assumptions, and generalizability
Required Reading:
1. Replication: How Well Do My Results Generalize Now? The External Validity of Online Privacy and Security Surveys. Jenny Tang, Eleanor Birrell, and Ada Lerner (SOUPS ‘22)
2. Key Reinstallation Attacks: Forcing Nonce Reuse in WPA2. Mathy Vanhoef and Frank Piessens (CCS ‘17)
Optional Reading:
1. Knowledge-Based Security of Dynamic Secrets for Reactive Programs. McKenna McCall, Hengruo Zhang, and Limin Jia (CSF ’18).
Due this week:
Review 10 on required reading from 11/18 lecture due 11/29 at midnight
Week 14
11/23-11/27 Fall Recess
No class
Week 15
12/1 Discussion 10
Discussion lead: McKenna
Final Projects and Reports
Week 15 (continued)
12/3 Final project presentations
Week 16
12/8 Final project presentations
12/10 McKenna traveling
No class
Final reports due 12/15 at midnight
