Hi Ben, Someone else may provide a more complete answer than me, but here is a partial answer that may be sufficient. - The current kernel implementation for multicore uses a single lock for serializing any access to the kernel by different cores. One part of the multicore verification is to incorporate this into the abstract models and existing security proofs. I'm not 100% sure how extensive the changes to the abstract model are expected to be, but these changes would likely result in changes to the existing implementation to maintain the refinement proofs. - The implementation of the locking mechanisms for implementing the abstract model will likely be incorrect. A big part of the verification effort will be ensuring that executing parts of the kernel that happen outside of the lock don't update or access shared state incorrectly as this is new behavior that doesn't exist in the current verified configurations. - Additionally, there are additional kernel object invocations to support multicore, such as for pinning a thread to a different core, registering interrupts on different cores etc. These are currently unverified under any configuration as they don't exist for the existing verified configurations. Using camkes to statically pin threads to different cores still depends on a correct implementation of the above mechanisms and so will require a verified multicore kernel to leverage any proof guarantees.
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. I hope this answered your questions. _______________________________________________ Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel
