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
End-to-End Verification of Information-Flow Security for C and Assembly Programs
by Costanzo et al.
Why are we reading this paper?
What to learn from this paper?
Answer this question
Suppose we want to make sure that a two-block disk can securely store two
users' data (one block for each user). In particular, if user A calls
Write(0, data) to write their data to block 0, then as long as
user B invokes the same disk API (Read() and Write()),
but does not call Read(0), then user B cannot retrieve A's data.
-
Why does the OneDiskAPI specification from the lab assignments not
guarantee this property? In other words, what implementation might
both satisfy OneDiskAPI and still leak data in violation of our security
goal above?
-
How does the observation function help CertiKOS prove the absence of
such bugs? What part of the proof do you expect will fail to go through?
