Proofcraft News - 2024

News from other years: 2023 2022 2021

# 2024-01-26 - 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).

Automated Platform Proofs Checks