Homework: Reading questions

Submit two items to the submission website (see link in the navigation bar at the top of the page):

Answer the following 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?

Questions or comments regarding 6.826? Contact us on Piazza or send e-mail to the 6.826 staff at 6826-staff@lists.csail.mit.edu.

Creative Commons License