Multiprocessor-Kernel Verification

Multiprocessor-Kernel Verification was a research activity of the Trustworthy Systems project.

The Clustered-Multikernel Design

• Problem: The key software component of a computer system is the operating-system kernel. It always needs to be trusted because it runs in the CPU's privileged mode and therefore has access to all system components. Consequently, kernel correctness is crucial for secure, safe and reliable computer systems. Correctness can be improved by careful design, development and testing. However, this is not enough for kernels of high-assurance computer systems used in defence, aviation and the like. Much stronger correctness guarantees can be obtained by formal verification of a kernel's implementation. For example, the L4.verified project has proved that the implementation of the seL4 microkernel adheres to its formal specification.

  However, in order to keep verification complexity at a manageable level, prior kernel verification research only targeted uniprocessor kernels. In other words, the current state of research restricts computer systems that require a verified kernel to running on one CPU/core. This is a problem because manufacturers are increasing computing power of their systems by adding more CPUs and cores.

• Aim: In this project, we aimed to demonstrate that it is possible to extend a verified uniprocessor kernel to utilise multiple CPUs/cores and leverage the existing proofs to obtain a verified multiprocessor version of that kernel.

• Approach: We introduced the clustered multikernel, a point in the design space of multiprocessor kernels. The clustered multikernel is an extension of the multikernel. In our case, every multikernel node consists of a separate instance of a slightly modified version of the verified uniprocessor kernel. In a multikernel, each core runs one node. In a clustered multikernel, however, a node is run by multiple CPUs and its kernel state is protected by a big lock. Hence, the main feature of the clustered-multikernel design is that it reduces concurrent data access to a minimum (to enable verification) while offering a configurable trade-off between scalability and flexibility.

  We developed a conversion scheme to convert a uniprocessor kernel into a clustered multikernel, and based on the clustered-multikernel design, we contributed a refinement lifting framework, which lifts the converted kernel's functional-correctness proof such that it applies to the clustered-multikernel version (under certain assumptions). The support for handling the introduced concurrency is added to the existing verification framework in a non-intrusive way. The refinement lifting framework accounts for weak memory ordering exhibited by TSO (total-store-order) multiprocessor architectures.

• Conclusion: We demonstrated the practicability of our approach by successfully applying it to seL4. We showed that this required relatively low effort, compared to seL4's initial verification.

People

Publications

		Michael von Tessin The clustered multikernel: An approach to formal verification of multiprocessor operating-system kernels PhD Thesis, School of Computer Science and Engineering, UNSW, Sydney, Australia, Sydney, Australia, December, 2013
		Michael von Tessin The clustered multikernel: An approach to formal verification of multiprocessor OS kernels 2nd Workshop on Systems for Future Multi-core Architectures, pp. 1–6, Bern, Switzerland, April, 2012
		Michael von Tessin Towards high-assurance multiprocessor virtualisation 6th International Verification Workshop, pp. 110–125, Edinburgh, UK, July, 2010
		Michael von Tessin Towards a formally verifiable multiprocessor microkernel Poster presented at the 2009USENIX Annual Technical Conference, June, 2009