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.
You may skip up to four paper reflections, and (separately) four in-class discussions for free.
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 | ||
| 7 | Sep 27 | ||
| 8 | Oct 1 | OWL: Compositional Verification of Security Protocols via an Information-Flow Type System | |
| Part 3: Implementation Security | |||
| 9 | Oct 4 | ||
| 10 | Oct 8 | ||
| 11 | Oct 11 | ||
| 12 | Oct 15 | ||
| 13 | Oct 18 | ||
| 14 | Oct 22 | Project proposals due | |
| Part 4: Topics | |||
| 15 | Oct 25 | The Last Yard: Foundational End-to-End Verification of High-Speed Cryptography | |
| 16 | Oct 29 | ||
| 17 | Nov 1 | ||
| 18 | Nov 5 | ||
| 19 | Nov 8 | ||
| 20 | Nov 12 | ||
| 21 | Nov 15 | Project check-in due | |
| 22 | Nov 19 | ||
| 23 | Nov 22 | ||
| 24 | Nov 26 | ||
| 25 | Dec 3 | ||
| 26 | Dec 6 | ||
| Project Presentations | |||
| 27 | Dec 10 | ||
| 28 | Dec 13 | Project reports due | |