Automated proof checks for more verified platforms
Proofcraft, with funding from the seL4 Foundation, has extended the seL4 proof checks
to automatically include other verification platforms and configurations. As a
result, there are now two further verified platforms available and proof-checked
regularly, bringing the total number of verified platforms to six, with
more in progress. The proofs are now also automatically checked with and
without the domain scheduler feature. This creates a base line for further
improvements in proof genericity and automated platform verification.
So far the seL4 proof check infrastructure has been targeting only
precisely one platform and kernel configuration for each supported architecture.
For instance, for the ARM 32-bit architecture, the proof check only targets the imx6
Sabre Lite board (with 16 domains and no FPU). Nevertheless, the functional
correctness proof also holds for any other number of domains and for multiple
additional boards, some with FPU.
Our previous work on generating verification configurations from kernel
configurations has made it possible to relatively easily re-run the proofs for
multiple configurations.
We have now extended the proof check infrastructure by adding a GitHub action that
automatically attempts to rebase all platform branches over each new push to the
master branch and run a full proof check for this branch. If the check succeeds,
the branch is automatically updated (else, manual intervention is needed, as
before).