Proofcraft News - 2024

News from other years: 2023 2022 2021

Proofcraft sponsor of the seL4 summit 2024

seL4 summit 2024

Proofcraft is proud to be sponsoring the 2024 seL4 summit, which will be held in its home town of Sydney, Australia, on Oct 15-17, 2024!

This annual international summit on the world’s most highly assured OS kernel gathers participants from industry, government and universities, including the creators and maintainers of the seL4 technology such as the Proofcraft team.

Proofcraft sponsor of HCSS'24 in Annapolis, USA


Proofcraft is a proud sponsor of the 24th High Confidence Software and Systems (HCSS) Conference that will be held on May 6-8, 2024 in Annapolis Maryland.

Every year, HCSS gathers researchers, practitioners, and leaders from government, universities, non-profits, and industry around themes dear to Proofcraft: mathematically-based tools and techniques, scientific foundations supporting evidence creation, systems assurance, and security. HCSS aims for the development of scientific foundations for the assured engineering of software-intensive complex computing systems and the transition of science into practice.

Proofcraft’s 3 co-founders, June, Gerwin and Rafal, will be attending HCSS'24.

June's keynote on the vision for a verified future, at MatchPoints, Denmark

“Cybersecurity: How do we maintain trust in our digital society?” is the question asked at this year’s MatchPoints conference, at Aarhus University, Denmark.

June was one of the 3 keynote speakers at this event that gathered around 400 leading cybersecurity experts from industry, government and academia across the world.

She presented seL4: a formally verified kernel as a defense against cyber attacks, followed by an interview by journalist Jacob Rosenkrands. She also participated in a “Meet the Expert lunch” with industry leaders, professors and students keen to exchange on seL4 and formal verification related topics with her.

June Andronick

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

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