Towards High-Assurance Multiprocessor Virtualisation

Select |




Print


von Tessin, Michael

von Tessin, Michael


2010-07-20


Conference Material


6th International Verification Workshop


Edinburgh, UK


110-125


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, we 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 us for uniprocessors. This work-in-progress paper explores possible multiprocessor designs of seL4 and their amenability to verification. For the chosen design, it contributes a formal multiprocessor execution model to lift seL4's uniprocessor model and proofs into a multiprocessor context using only minor modifications. The theorems proving the validity of the lift operation are machine-checked in Isabelle/HOL and walked-through in the paper.


EasyChair


formal verification, multiprocessor, microkernel, virtualisation, seL4, Isabelle/HOL


http://www.mais.informatik.tu-darmstadt.de/verify2010


2040-557X


nicta:3849


von Tessin, Michael. Towards High-Assurance Multiprocessor Virtualisation. In: Markus Aderhold, Serge Autexier and Heiko Mantel Editor, editor/s. 6th International Verification Workshop; Edinburgh, UK. EasyChair; 2010-07-20. 110-125.



Loading citation data...

Citation counts
(Requires subscription to view)