Our Partners
Verifying seL4 Microkit-based systems
Aim
Formally verify four core aspects of the seL4 Microkit library and Microkit-based systems:
- 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;
- correctness of the kernel abstraction, i.e., the Microkit library is verified against a SMT-suitable abstraction of seL4 that is connected with the rest of seL4's proofs; and
- correctness of system-critical OS components built with the Microkit.
Approach
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
- DRAFT report on Verifying the seL4 Microkit, dated 2023-12-21
- 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
Availability
Gordian is open-sourced on GitHub.
Artefacts from early developments are still available for download.
Latest News
- 2023-12-11: Gordian has been released on GitHub.
- 2023-10-17: Mathieu Paturel presents a poster at the main conference of SOSP.
- 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
Current |
Past |
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 |