Lecture preparation
Before lecture, read the paper assigned below, and submit two items
to the
submission website:
- Submit your own question about the paper (e.g., what you find most
confusing about the paper or the paper's general context/problem), before
lecture (i.e., 1pm). You cannot use the question below. To the extent
possible, during lecture we will try to answer questions submitted
beforehand.
- Submit your answer for the question below, before the beginning of the lecture.
Also keep in mind that you will need to write a
paper summary for your choice of papers
throughout the semester.
Assignment
Read the paper
Everest: Towards a Verified, Drop-in Replacement of HTTPS
by a large team mostly associated with Microsoft Research.
Why are we reading this paper?
-
Ambitious use of formal methods in a problem domain that seems like
a good fit for these techniques.
-
Range of specifications and challenges in one unified,
well-motivated system.
-
Although the full stack has not been fully verified yet as of this
paper's writing, there are already important successes in verification
of individual components.
What to learn from this paper?
-
Look for the different specifications, both desired properties
and models of the system.
-
Understand what it really means to "verify TLS".
Answer this question
The paper talks about game-based cryptographic proofs, which show that
the Everest TLS implementation implements an idealized secure channel,
assuming the underlying cryptography is correct. What cryptographic
primitives do the authors assume correct? How do they encode the
assumption that these primitives are correct?
