Many of those following the DeepSpec project will have heard of the verification of the seL4 microkernel. This talk will recap the seL4 verification project when first completed, and the engineering work that has been done to maintain and extend the proofs over nearly ten years since then.

Nearly all modern hardware is now multi-core. To support this, we have begun the most substantial change to the seL4 proofs to date. Supporting multi-core platforms requires new kernel mechanisms, but more importantly, requires the correctness properties of the kernel to handle concurrency. This talk will present the verification approach we have designed, and give an overview of the effort that remains to adapt the existing proofs into the new framework.

Tue 19 Jun

14:00 - 15:40: DeepSpec 2018 - Concurrency and Concurrent Operating Systems at Columbus Ballroom B
deepspec-2018-papers14:00 - 14:30
Jieung KimYale University, USA
deepspec-2018-papers14:30 - 15:00
Thomas SewellUNSW, Australia
deepspec-2018-papers15:00 - 15:30
William ManskyPrinceton University