Trustworthy Systems

Our Partners NCSC

Verifying seL4 Microkit-based systems

Aim

Formally verify four core aspects of the seL4 Microkit library and Microkit-based systems:

Approach

Microkit to CapDL to system initialiser

This figure gives an overview of the various constituents and steps for verifying the Microkit and Microkit-based systems.

In summary:

Proof items 1 (Microkit library) and 2 (CapDL generation for system initialisation) are the result of recent work.

Proof item 3 (SMT-suitable kernel abstraction) is still required to achieve end-to-end proof of PD functionality. Proof item 4 will cover verification of OS components built with the Microkit.

Proof item 1: Microkit library verification

We have successfully evaluated the usage of SMT-based verification to prove local correctness properties of the Microkit implementation.

Proof item 2: System initialisation

We are working on an automatic, verified mapping of the Microkit system description to a CapDL specification, which describes the access rights of an seL4-based system (as represented by capabilities to seL4 objets).

From the CapDL specification we can use provably correct generation of the system initialisation code of the kind that was developed as part of the DARPA CASE project.

Proof item 3: SMT-suitable kernel abstraction

We are working on a proof of correspondence between the SMT-suitable Microkit-facing specification of the seL4 kernel (MSpec), against which the Microkit's SMT-based verification is carried out, and seL4's abstract specification (ASpec), against which seL4's implementation is verified.

Proof item 4: OS component verification

We are exploring and developing further the use of SMT-based verification of the kind used in the Microkit library verification to verify OS components built on top of the Microkit, including device drivers and other components of the Lions OS.

Support

This work is supported by the UK government's National Cyber Security Centre.

Documentation

Availability

Gordian is open-sourced on GitHub.

Artefacts from early developments are still available for download.



Latest News

Contact

People

Publications

Abstract PDF Trudy Weibel, Zoltan Kocsis, Mathieu Paturel, Rob Sison, Isitha Subasinghe and Gernot Heiser
Verifying the seL4 Microkit
https://trustworthy.systems/publications/papers/Weibel_KPSSH_24.pdf, June, 2024
Abstract PDF Mathieu Paturel, Isitha Subasinghe and Gernot Heiser
First steps in verifying the seL4 Core Platform
Asia-Pacific Workshop on Systems (APSys), Seoul, KR, August, 2023
Abstract
Slides
PDF
Presentation Video
Gernot Heiser, Lucy Parker, Ivan Velickovic, Peter Chubb and Ben Leslie
Can we put the "S" into IoT?
IEEE World Forum on Internet of Things, Yokohama, JP, November, 2022