Our Partners

Verifying the seL4 Microkit

Aim

Formally verify two core aspects of the Microkit:

• correctness of the implementation, i.e., its abstractions function as specified;
• correctness of the system initialisation, i.e., the collection of underlying seL4 objects are fairly represented by the system specification.

Approach

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 re-use the provably correct generation of the system initialisation code that was developed as part of the DARPA CASE project.

Implementation verification

We are evaluating the suitability of push-button techniques, using SMT solvers, to prove the correctness of the implementation of the Microkit.

Support

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

Collaborations

We collaborate with with Breakaway Consulting, the original creators of the seL4 Microkit.

Documentation

• Verification of the Microkit implementation: Step 2: Initial Verifier of 2022-12
• Verified mapping of Microkit spec to CapDL: Step 2: Mapping Prototype and Verification Plan of 2022-12
• Verification of the Microkit implementation: Step 1: High-Level Specification and Approach of 2022-12
• Verified mapping of Microkit spec to CapDL: Step 1: SDF Specification and Verification Approach of 2022-12

Latest News

• 2022-10-10: Zoltan Kocsis presents the seL4 Microkit and our work on verifying it at the seL4 Summit.

Contact

• Gernot Heiser, gernot<at>unsw.edu.au

People

Publications

		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
		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

Artefacts

Initial artefacts are available here .