Course Components

Each week, you will be responsible for reviewing one of the required readings (if there are any). Reviews are typically due Tuesday at midnight via the course HotCRP site (linked from Canvas) so discussion leads have time to read them before the Thursday 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.

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.

Unit 0: Course Intro

Date

Topic

Assignment

Week 1

8/26

Lecture

Course Overview: Syllabus, classroom expectations, course motivation

Required Readings:

  1. Thoughts on Reviewing, Mark Allman 
  2. Notes on Constructive and Positive Reviewing, Mark Hill and Kathryn S McKinley
  3. USENIX Orientation slides, adapted from slides developed by Lujo Bauer and Giancarlo Pellegrino

No reviews due this week

8/28

Discussion

How to write a review and lead a discussion

Discussion lead: McKenna

Bid on papers on HotCRP by midnight 8/29 (you’ll receive an invitation by email)

Unit 1: Security and Privacy

Date

Topic

Assignment

Week 2

9/2

Lecture

Threats and Attackers: Threat modeling, STRIDE, hacking humans

Required Readings:

  1. Why Cryptosystems Fail. Ross Anderson (CCS ‘93).
  2. A Framework for Reasoning About the Human in the Loop. Lorrie Faith Cranor (UPSEC ‘08).

Review due 9/2 at midnight

9/4

Discussion

Required readings, reviews

Discussion lead: Student(s)

Week 3

9/9

Lecture

Security and Privacy Goals and Metrics: Information security properties, usable security metrics, side & covert channels

Required readings:

  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 ‘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 readings:

  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

Review due 9/9 at midnight

9/11

Discussion

Required readings, reviews

Discussion lead: Student(s)

Week 4

9/16

Lecture

Introduction to Cryptography and Security Protocols: Terminology, symmetric and public key algorithms

Optional readings:

  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

No reviews due this week

9/18

Lecture

Introduction to Buffer Overflows: Vulnerabilities and mitigations

Course Project overview

Unit 2: Formal Methods

Date

Topic

Assignment

Week 5

9/23

Lecture

Introduction to Formal Methods: Static and dynamic analysis

Optional readings:

  1. Proving the Correctness of Multiprocess Programs. Leslie Lamport (IEEE Trans. On Software Engineering ‘77).
  2. A High-Level View of TLA+. Leslie Lamport.

No reviews due this week

9/25

Lecture

Model Checking: Finite state machines, safety and liveness properties

Project proposals due 9/25 at midnight

Week 6

9/30

Lecture

Type Systems and Program Semantics: Noninterference, information flow control

Required readings:

  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 readings:

  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).

Review due 9/30 at midnight

10/2

Discussion

Required readings, reviews

Discussion lead: Student(s)

Unit 3: Usable Security

Date

Topic

Assignment

Week 7

10/7

Lecture

Introduction to Usable Security: What is “usable”?, parts of a usable security study

Required Readings:

  1. Why Johnny Can’t Encrypt: A Usability Evaluation of PGP 5.0. Alma Whitten and J.D. Tygar (USENIX Security ‘99)
  2. Evaluating the Usability of Privacy Choice Mechanisms. Hana Habib and Lorrie Faith Cranor (SOUPS ‘22).

Optional reading:

  1. “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.
  2. 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.

Review due 10/7 at midnight

10/9

Discussion

Required readings, reviews

Discussion lead: Student(s)

Week 8

10/14

Lecture

Surveys and Interviews: Pros, cons, and development

Required readings:

  1. Do Users Write More Insecure Code with AI Assistants? Neil Perry, Megha Srivastava, Deepak Kumar, and Dan Boneh (CCS ’23).

Optional readings:

  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.

Reviews due 10/14 at midnight

10/16

Discussion

Required readings, reviews

Discussion lead(s): Students

Week 9

10/21

Lecture

Quantitative & Qualitative Analysis: Goals, null hypotheses, how to choose a statistic

Required readings:

  1. Misuse, Misreporting, Misinterpretation of Statistical Methods in Usable Privacy and Security Papers. Jenny Tang, Lujo Bauer, and Nicolas Christin (SOUPS ‘25).

Optional readings:

  1. Chapters 2.2, 2.4, 4, and 11 of Research Methods in Human-Computer Interaction. Jonathan Lazar, Jinjuan Heidi Feng, and Harry Hochheiser.
  2. Availability of cookies during an academic course session affects evaluation of teaching. Michael Hessler, Daniel M Pöpping, Hanna Hollstein, Hendrik Ohlenburg, Philip H Arnemann, Christina Massoth, Laura M Seidel, Alexander Zarbock, and Manuel Wenk 

Review due 10/21 at midnight

10/23

Discussion

Required readings, reviews

Discussion lead(s): Students

Unit 4: Usability in Formal Methods

Date

Topic

Assignment

Week 10

10/28

Lecture

Smart Homes

Required readings:

  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.

Optional readings:

  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).

Review due 10/28 at midnight

10/30

Discussion

Required readings, reviews

Discussion lead: Student(s)

Project check-in 1 due 10/30 at midnight

Week 11

11/4

Lecture

Information Flows on the Web

Required readings:

  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).

Review due 11/4 at midnight

11/6

Discussion

Required readings, reviews

Discussion lead: Student(s)

Unit 5: Research Ethics and Limitations

Date

Topic

Assignment

Week 12

11/11

Guest Lecture

Lorrie Cranor

11/13

McKenna traveling

No class

Week 13

11/18

Lecture

What is (Ethical) Human Subjects Research?: IRBs, research ethics

Required readings:

  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 readings:

  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).

Review due 11/18 at midnight

11/20

Discussion

Research ethics, required readings, reviews

Discussion lead: McKenna

Project check-in 2 due 11/21 at midnight

Week 14

11/25

Fall recess

No class

Week 15

12/2

Lecture

Limitations of Formal Methods and Usable Security: Revisiting attacker models and side channels, assumptions, and generalizability

Required readings:

  1. Key Reinstallation Attacks: Forcing Nonce Reuse in WPA2. Mathy Vanhoef and Frank Piessens (CCS ‘17).
  2. 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).

Review due 12/2 at midnight

12/4

Discussion

Required readings, reviews

Discussion lead: McKenna

Final Projects and Reports

Date

Topic

Assignment

Week 16

12/9-12/11

Final project presentations

Final reports due 12/12 at midnight