News
SysV: Notes on the third question of Problem set 2 (deadline is extended)
Written on 03.01.2021 15:11 by Hamed Nemati
It seems that some of you (and not all) had problem understanding third question, so I try here to clarify this question a bit more and I extend the deadline until Wednesday (January 6) so that you can fix your answers.
The goal of this question is to see how we can apply a compositional approach to prove noninterference for a real world scenario where we have a processor connected to the main memory and the MMU. The interaction between these three components is clearly stated in the third lecture so if you have not heard about them before please refer to the lecture three.
In this scenario the core component is acting on behalf of the user level processes. This means that it receives requests in term of read and write operations from the user processes and tries to execute them and retrive the data from (or write user supplied date into) the memory. As you may remember from your Operating System course processes are using virtual addresses to access the memory. However, the main memory is indexed with physical addresses. This implies that whenever the core receives a memory access request from a user process, it should first translate this address into the corresponding physical address and for this the core queries the MMU.
1- The word "interface" in the first part of the question has a standard meaning. In other words by "interface" we mean a set of functionalities that the core provides to user level processes or to interact with the memory and the MMU.
2- I think the second part of the question is completely clear. What you need to do here is to define an observation relation as required by the noninterference property. The observation relation defines which parts of the memory and core states are visible to an attacker.
In translating virtual-to-physical addresses the MMU uses page tables which store the mapping between virtual and physical addresses. So the page tables are security critical and must be protected from modifications by a user level process. Otherwise they can change the mappings in these tables and get access to secret part of the system and invalidate the noninterference property.
3- The third part of the question asks you to define a predicate which prevents user level processes from changing page tables. We need this to be able to prove the noninterference property and without defining such a constraint we cannot do the proof. In order to answer this question what you will need to define is a function like MMU which takes as input the memory and user request plus some other stuffs (if needed, you figure this out) and return either the corresponding physical address or an error saying that the request is invalid due to permission error or other issues.
4- If you manage to define the previous parts reasoning compositionally about the noninterference property should be easy. What you will need to do here is to split the proof other the noninterference property into two separate parts one about the core components and the other one about the memory.
To help you further with answering this question I ask you to check the section 4 of this paper (link). Please also remember that if you have any problem understanding lectures or exercises YOU SHOULD ASK US thats why we have Q&A sessions.