CS 260r 2017 L2: seL4: Formal Verification of an Operating-System Kernel (1/25)
The core of the seL4 correctness proof is the forward simulation relation described in §4.4 and illustrated in Figure 6. (I believe insane category theorists would describe this as a kind of “Galois connection.”) Explain how the forward simulation relation would work in the restricted domain of seL4’s scheduling policy (Figure 3). What abstract state (σ) is implied by Figure 3? What concrete state would you expect the implementation to maintain? What does an abstract scheduling operation perform (what does M_1 do)? Finally, what is the relation between abstract and concrete states?
Never submit passwords through Google Forms.
This form was created inside of Google Apps for Harvard.
Terms of Service