CS 7480: Special Topics in PL:
Formal Security for Cryptography

Course Info

Time and Place:
Tuesdays and Fridays, Hayden Hall 321, 3:25 pm - 5:05pm

Quick links: Final Project | Schedule | Paper Reflections | Class Policies

Instructor:

Description

Virtually all digital communications infrastructure relies on cryptography for security. While crypto is essential, it's also extremely brittle --- any coding error or mistake in a security proof can compromise the entire system's security. Since cryptographic security can have such high stakes, it's a perfect fit for techniques from PL (e.g., type systems and theorem provers), which can deliver provable, fully formal security guarantees.

This seminar will cover the science and practice of building cryptographic code with formally proven security guarantees. We will cover the "full stack", ranging from cryptographic security for complex protocols (e.g., TLS and secure VPNs), to the security of their underlying cryptographic algorithms (e.g., symmetric ciphers and elliptic curves) and associated high-performance implementations in C and assembly.

The intended audience is graduate students with an interest in formal methods or applied cryptography, and will consist of lectures, student-led paper presentations, and a course project. The course will assume some amount of programming experience, and familiarity with concepts from programming languages (e.g., operational semantics, type systems, and first-order logic); supplemental background reading will be supplied as well. There is no formal textbook requirement for the course.

Assignments and Evaluation

After an initial set of lectures, the course will consist of paper discusions and a final project. The course grade will be determined by: All graded material will be submitted via Canvas.

Paper Reflections and In-Class Discussion

For each paper we read, you will submit a paper reflection, in the form of a questionnaire, via Canvas. Each paper's reflection will be due by 11:59 PM the day before the class that we read the paper. Please spend some time to think critically about your answers! The following paper discussion will directly be informed by your answers to the questionnaire.

You may skip up to four paper reflections, and (separately) four in-class discussions for free.

Grading Policy for Paper Reflections
Paper reflections will be graded on a binary complete/did not complete scale. Don't worry if you can't come up with answers to every question! If you turn in a paper reflection, I will trust that you put in a good faith effort to think deeply about the paper and respond accordingly.

Final Project

See here.

Background Reading

The readings for this class will utilize a mix of ideas from PL, verification, security, and cryptography. If you are interested, see here for some suggested background reading.

Schedule (under construction / subject to change)

A growing list of papers can be found here.

Date Topics Notes
Part 1: Course Overview
1 Sep 6 Course Overview slides
2 Sep 10 Foundations slides
Part 2: Protocol Security
3 Sep 13 A Comprehensive Symbolic Analysis of TLS 1.3 Additional Readings:
4 Sep 17 Computationally sound mechanized proofs for basic and public-key Kerberos
5 Sep 20 DY Fuzzing: Formal Dolev-Yao Models Meet Cryptographic Protocol Fuzz Testing
6 Sep 24 SSProve: A Foundational Framework for Modular Cryptographic Proofs in Coq Repository
7 Sep 27 OWL: Compositional Verification of Security Protocols via an Information-Flow Type System
8 Oct 1 The Squirrel Prover and its Logic This is a journal article, and doesn't have all of the technical details.
Part 3: Implementation Security
9 Oct 4 Simple High-Level Code For Cryptographic Arithmetic: With Proofs, Without Compromises
10 Oct 8 FaCT: a DSL for timing-sensitive computation
11 Oct 11 Vale: Verifying High-Performance Cryptographic Assembly Code Repository
12 Oct 15 EverParse: Verified Secure Zero-Copy Parsers for Authenticated Message Formats
13 Oct 18 The Last Yard: Foundational End-to-End Verification of High-Speed Cryptography
14 Oct 22 Jolt: Recovering TLS Signing Keys via Rowhammer Faults Project proposals due
Part 4: Topics
15 Oct 25 No class: OOPSLA 2024
16 Oct 29 CryptOpt: Verified Compilation with Randomized Program Search for Cryptographic Primitives
17 Nov 1 On Separation Logic, Computational Independence, and Pseudorandomness Presenter: Shubh
18 Nov 5 Wysteria: A Programming Language for Generic, Mixed-Mode Multiparty Computations
19 Nov 8 Computer-aided proofs for multiparty computation with active security
20 Nov 12 Certifying Zero-Knowledge Circuits with Refinement Types Repository
21 Nov 15 Mechanized Proofs of Adversarial Complexity and Application to Universal Composability Project check-in due
22 Nov 19 A Core Calculus for Equational Proofs of Cryptographic Protocols Presenter: Conrad
23 Nov 22 EasyBC: A Cryptography-Specific Language for Security Analysis of Block Ciphers against Differential Cryptanalysis
24 Nov 26 SpecMon: Modular Black-Box Runtime Monitoring of Security Protocols
25 Dec 3 AutoVerus: Automated Proof Generation for Rust Code
26 Dec 6 Office Hours / Discussion Attendence optional
Project Presentations
27 Dec 10
28 Dec 13 Project reports due

Class Policies

Academic Integrity Policy

For paper reflections, you are to complete them by yourself, with no feedback from others or AI assistants. For the final project, you are free to build upon the work of prior papers and open-source projects with the appropriate citations. In particular, any code or text not written by you personally must be cited. Minor coding tasks and grammar cleanup by AI is allowable, but must be cited. You may incorporate feedback from others outside of your group with appropriate citations as well.

Accommodations for Disabilities

Students who wish to receive academic services or accommodations should visit the Disability Access Services. Please provide a letter from the DAS to me early in the semester so that I can arrange the appropriate accommodations.

Auditing Policy

Auditors are welcome to join in class discussions and submit a final project. If you would like to submit paper reflections or final project materials, instead of using Canvas, please email me with the subject line subject line including CS7480.