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
Formal Proofs, the Fine Print and Side Effects
by Murray et al.
Why are we reading this paper?
- Security is a significant motivation for formal verification.
- Even verified systems can have security vulnerabilities.
- Formal verification might have unintended side-effects on a system being developed for verification.
What to learn from this paper?
- Why might proofs be valuable even if they are not perfectly applicable to real systems.
- How formal verification might induce undesirable side-effects.
- How to think about the relation between formal proofs and security.
Answer this question
In Figures 2-5, the paper presents Venn diagrams showing possible
changes to the system's code. Thinking about these diagrams from the
perspective of the lab assignments in this class, where do you think
your code changes lie? Did formal verification force you to fix bugs
(P and A)? Did formal verification force you to make irrelevant changes
(P but not A)? Were there any bugs you introduced during verification (V)
or issues you realized were there but not required for formal verification
(A but not P)? What are the most interesting examples of these bugs
from your experience?
