Formally verify two core aspects of the Microkit:
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.
We are evaluating the suitability of push-button techniques, using SMT solvers, to prove the correctness of the implementation of the Microkit.
This work is supported by the UK government's National Cyber Security Centre.
We collaborate with with Breakaway Consulting, the original creators of the seL4 Microkit.
|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