Proofcraft News - 2024

News from other years: 2023 2022 2021

# 2024-04-14 - Proofcraft is 3 years old

Proofcraft is 3 years old

Proofcraft is 3 years old and we’re still having fun while building a more verified future!

Amongst other things, our third year has seen us deliver the functional correctness proof of sel4 on AArch64, progress on the verification of MCS seL4, receive the ACM Software System Award, and present at the seL4 summit 2023 in Minneapolis.

Much more to come! Stay tuned.

# 2024-04-01 - seL4 on AArch64 is now verified for functional correctness

Proofcraft has completed the formal mathematical proof that the seL4 code behaves exactly as its abstract specification mandates on AArch64, thanks to continued support from NCSC.

This functional correctness property is the strongest assurance that can be given about the correctness of software, orders of magnitude stronger than merely showing the absence of known flaws. Moreover, functional correctess is the corner stone of even stronger assurance like security properties of integrity and confidentiality.

The latest 64-bit Arm architecture is now on par with Arm 32-bit, RISC-V 64-bit and Intel’s x86 64-bit architectures with respect to seL4’s functional correctness proof.

seL4 on AArch64

# 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