Trustworthy Systems

Our Partners NCSC Breakaway Consulting

Verifying the seL4 Core Platform

Aim

Formally verify two core aspects of the seL4 Core Platform:

Approach

seL4CP to CapDL to system initialiser

System initialisation

We are working on an automatic, verified mapping of the seL4CP 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 seL4CP.

Support

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

Contact

People

Current

Past