On Tue, Mar 17, 2020, 7:32 PM Mcleod, Kent (Data61, Kensington NSW) < Kent.Mcleod@data61.csiro.au> wrote: The closest you could get to a multicore system that leverages verified
kernel configurations would be to setup a multikernel implementation where each core had its own instance of a verified seL4 configuration where any hardware resources are strictly partitioned between them. I'm not aware of any examples of this setup but there have been research projects that have used multikernel implementations of seL4 in the past. Also this still wouldn't give you an overall system with the same guarantees as a single seL4 as the different instances would need to trust each other to not overwrite each other's kernel data structures and is outside of the current proof assumptions.
Assuming that the root tasks drop capabilities that could be problematic, would this still be correct? This seems to follow from the existing seL4 specification (no way to get rights to memory from nothing). Also, why is verifying fine-grained locking so difficult? CertiKOS managed to do it, so I am probably missing something. Sincerely, Demi