Happy Holiday Season from Proofcraft!
Proofcraft News - 2024
Proofcraft part of DARPA's PROVERS program to reduce reliance on experts
The US Defense Advanced Research Projects Agency (DARPA) is funding a large-scale, high-impact program, called PROVERS. The goal of the program is to make formal methods accessible to non-experts, such as traditional software developers and systems engineers, while minimizing the impact on their existing processes and performance.
Proofcraft is part of the program’s successful INSPECTA team, led by Darren Cofer from Collins Aerospace, with contributions from UNSW Sydney, DornerWorks, Carnegie Mellon University, The University of Kansas, and Kansas State University.
As part of INSPECTA, Proofcraft will reduce the reliance on experts for seL4 formal proofs in 3 ways: automated platform port verification, architecture-split of proofs, and completion of the MCS seL4 functional correctness proof.
Firstly, Proofcraft will automate the verification of seL4 for new hardware platforms, allowing engineers to use a verified configuration of seL4 on an increasing number of platforms without needing Formal Methods expertise.
Secondly, Proofcraft will significantly increase the subset of existing seL4 proofs which are split into architecture-dependent and architecture-independent parts. This will decrease the need for Formal Methods expertise when verifying code changes, as changes to architecture-dependent parts will no longer affect the architecture-independent parts of the proofs, and verification of architecture-independent changes will be done once for all architectures.
Finally Proofcraft will complete the MCS seL4 functional correctness proof, which will provide a kernel that both supports mixed-criticality systems and has a formal proof of functional correctness. This will allow engineers to build software systems that can enforce timing integrity (i.e. no application can overrun its timing budget), while being able to provably isolate applications.
The White House, NCSC, Amazon, Meta... and Proofcraft advocating Formal Methods
The White House’s “Back to the Building Blocks: A Path Toward Secure and Measurable Software” report prompted a special seminar on Formal Specification and Validation at Scale, held at the Isaac Newton Institute in Cambridge, UK in October 2024.
This event brought together key invited experts and policymakers all driven by a common goal to advance formal methods and strengthen cybersecurity.
Proofcraft CEO June Andronick presented insights and lessons learned from seL4’s formal verification journey and its impact in deployed systems, alongside presentations from Anjana Rajan from the White House, Byron Cook from Amazon, Peter O’Hearn from Meta, Paul W2 from UK’s National Cyber Security Centre, and many more.
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).
