Our Partners

Verifying the seL4 Core Platform

Aim

Formally verify two core aspects of the seL4 Core Platform:

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

• Zoltan Kocsis, z.kocsis<at>unsw.edu.au

People