Lecture preparation

Before lecture, read the paper assigned below, and submit two items to the submission website:

Also keep in mind that you will need to write a paper summary for your choice of papers throughout the semester.


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.

  1. 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?
  2. 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?