Proofcraft News - 2024

Impactful on-stage presence from Proofcraft at the 2024 seL4 summit

Proofcraft had an impactful presence at the 2024 seL4 Summit in Sydney, which set a new attendance record of 89 participants and brought together the key players in the seL4 ecosystem. Not only was Proofcraft a sponsor of the summit, but the company also had a strong on-stage presence, delivering two key technical talks and participating in the seL4 anniversary panel.

Michael McInerney presented Proofcraft’s seL4 verification status and plans, including the completion of the functional correctness proof of seL4 on AArch64 and progress on verifying seL4’s extensions for mixed-criticality systems (MCS).

Corey Lewis shared Proofcraft’s roadmap for producing a verified static multikernel configuration of seL4, which will enable the use of multiple CPU cores with one kernel per core, with incrementally increased formal assurance.

Proofcraft’s three co-founders, Gerwin Klein, June Andronick and Rafal Kolanski, participated in this year’s panel discussion celebrating seL4’s multiple anniversaries. They shared their insights on past achievements, challenges and lessons learned, as well as their vision for the 20 years ahead.

With Ryan Barry also present (and contributing his photography skills for the summit group photo), the whole team was together for this key seL4 event.

All the Summit sessions can be watched online on the seL4 Youtube channel.

Proofcraft sponsor of the 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.

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.

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.

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).