Due: Mon, 16 May 2016 23:00:00 -0700
Read Comprehensive Formal Verification of an OS Microkernel, TOCS 2014.
Take a look at the tutorial.
Why does the seL4 verification include a Haskell prototype layer? Is that prototype trusted?
How does the TCB of seL4 compare to that of IronFleet? Are there similarities in the proof structure?
Provide a list of questions you would like to discuss.
Extend seL4 to support multicore.