Proofcraft News - 2024
# 2024-04-29 - 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.
# 2024-04-17 - 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.
# 2024-04-14 - 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.
# 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).
