Towards High-Assurance Multiprocessor Virtualisation
Virtualisation is increasingly being used in security-critical systems to provide isolation between system components. Being the foundation of any virtualised system, hypervisors need to provide a high degree of assurance with regards to correctness and isolation. Microkernels, such as seL4, can be used as hypervisors. Functional correctness of seL4's uniprocessor C implementation has been formally verified. The framework employed to verify seL4 is tailored to facilitate reasoning about sequential programs. However, the authors want to be able to use the full power of multiprocessor/multicore systems, and at the same time, leverage the high assurance seL4 already gives one for uniprocessors. This work-in-progress paper explores possible multiprocessor designs of seL4 and their amenability to verification.