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
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:
- 20% in-class participation;
- 40% written paper reflections; and
- 40% a final course project.
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.
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.