Proof Robustness in the seL4 Verification

Presented as part of the 2021 HCSS conference. 

ABSTRACT

The seL4 proofs have seen sustained development, maintenance, and extension for over 15 years. They now measure more than a million lines of Isabelle/HOL proof script and therefore likely represent the largest machine-checked interactive proof on the planet. This talk will report on past and ongoing efforts to maintain robustness of this proof and code base. We will give examples of where these efforts were successful and the presented techniques worked well. We will also show examples of where proofs lacked robustness and these efforts failed or did not apply, together with our thoughts of what can be done in such cases. With the creation of the seL4 Foundation and increasing contributions to both code and proofs from open source collaborators as well as companies from the US and Europe, the importance of proof robustness in seL4 continues to increase. We will discuss the measures already in place as well as planned efforts to make verified seL4 development more agile and more suitable for a vibrant open source community. These include adjustments to our automatic continuous integration and deployment pipeline for the high-assurance artifact of the seL4 kernel itself, as well as the ecosystem of components and platforms around it, which vary in the degree of assurance they provide.

Gerwin Klein, Chief Scientist and co-founder at Proofcraft, and Conjoint

  Professor at UNSW Sydney, is the architect of the seL4 microkernel

  verification. He planned, led, and executed the initial verification of seL4

  as well as many of its extensions, and continues to be actively involved in

  all aspects of the project.

Rafal Kolanski, Chief Engineer and co-founder at Proofcraft, has been

  leading the seL4 Proof Engineering team since 2015. He is responsible for many

  of the modern proof engineering techniques and mechanisms introduced into the

  seL4 verification since then. He was a member of the initial seL4 verification

  and brings with him more than 15 years of experience in large-scale formal

  verification