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

On 18 Mar 2020, at 08:59, Demi Obenour wrote:

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).

You can set up a system to be completely separated from the root task, and yes, that would increase confidence. There was a PhD thesis a while ago that had a semi-formal but fairly rigorous argument for why and how this will work, but you’d still not be running the verified configuration of the kernel, i.e. you’d have code in there that was not verified, even if that code doesn’t do much in this setup and you can probably convince yourself manually that it is fine.

Also, why is verifying fine-grained locking so difficult? CertiKOS managed to do it, so I am probably missing something.

I don’t see that much fine-grained locking in CertKOS, it mostly uses separation. It’s easier for it to do so, because it has a significantly simpler API (in fact, it’s probably quite similar to a multikernel setup in seL4 + messaging between cores. The only setups I’ve seen have precisely one VM per core). There is a concept of locking in the reasoning inherent to separation logic with permissions (which is what the CertiKOS verification uses), but these are not necessarily actual locks, just statements that it is known at this point that one thread has exclusive access to a resource. That might be via separation or it might be by protocol or it might be by an actual lock. This sounds very good and it is in fact very nice when it works, but you do need separation logic to work for your setup, which likes trees and lists, i.e. data structures that don’t have sharing, but not arbitrary graphs with sharing. seL4 has a lot of the latter (mostly anything to do with caps). You can talk about the seL4 API in terms of separation logic for user-level proofs where you tend to set things up separated, but formulating the kernel invariants in separation logic is an unsolved problem — as in, we have tried in the past and given up on that avenue. I don’t think it makes any sense to use separation logic for the seL4 refinement, because the inherent sharing in those data structures destroys the nice reasoning principles of that logic. It doesn’t matter if you'd manage to somehow express the invariants, the sharing is real and central to the argument, you can’t sweep it under the rug. The CertiKOS design avoids that, but pays for it in performance and API power. That all said, it’s not the locking that is that hard. It’s a bit annoying, but not so bad. It’s the fact that the underlying model of the proofs changes. Execution is not just sequential execution any more, but concurrent execution of multiple CPUs, which means the underlying logic changes, and several hundred thousand lines of proof that took years to write are now invalid. Most of these can be re-established, potentially even easily, but only if you manage to make the reasoning look exactly like it did before to the theorem prover. We think we’ve solved that problem on the research level last year, but still need to apply it at scale. After that, the problem is reduced to the points Kent mentioned, which are work, but not unsurmountable. Cheers, Gerwin