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