Proofcraft News - 2023
# 2023-07-19 - Learn about reducing the reliance on verification experts at the next seL4 summit
Proofcraft will be presenting how we are “reducing the reliance on verification experts for seL4 proofs”, at the coming seL4 summit on September 19th 2023 in Minneapolis, USA.
Proofcraft is constantly developing and refining proof engineering techniques to manage what is probably the world’s largest continually maintained formal proof artefact. Importantly, and perhaps paradoxically, proof engineering aims at reducing the reliance on verification experts, in this case through techniques improving the genericity and automation of the seL4 proofs.
In this talk we will present challenges one encounters while maintaining such a large proof base, along with some of Proofcraft’s existing and planned techniques to make seL4 proofs more agile and friendly to change, more robust against predictable change, and less dependent on experts for updates.
# 2023-07-11 - Proofcraft gets funding to complete seL4 AArch64 functional correctness and more
Proofcraft receives further funding from NCSC to complete the functional correctness proofs of AArch64 seL4 and to complete a concurrency framework for the verified multikernel roadmap.
Proofcraft has successfully delivered specifications and proofs of invariants preservation for seL4 on AArch64, as well as a roadmap and first steps towards a verified seL4 multikernel.
The next steps for the verified multikernel are to evaluate and complete a previously developed proof-of-concept concurrency monad framework. We will be completing the set of Rely/Guarantee rules as well as refinement rules for reasoning about abstract concurrent specifications. This means that the seL4 proofs will in the future be able to reason about multiple instances of the kernel at once.
In the AArch64 verification, the remaining steps to complete the functional correctness proof are the abstract-to-design and the design-to-C refinement proofs. Together, they will show that the C code of seL4 on AArch64 behaves exactly as its specification mandates.
# 2023-07-05 - Towards a verified multikernel seL4: adding parametrisation
Demand for a verified multicore seL4 is increasing. The seL4 microkernel is the most highly assured OS kernel, but all current seL4 proofs hold for unicore platforms only. Proofcraft is taking the first steps towards providing developers with the use of multiple cores while running on a verified kernel: static multikernel configurations of seL4, where each core runs a separate copy of the (verified) kernel, with minimal cross-core communication.
Thanks to funding from NCSC, we have made progress in the verified multikernel roadmap by adding initial parametrisation to the seL4 proofs.
In particular, the memory locations where the kernel is located and is allowed to interact with are no longer hard-coded to be equal to the physical memory layout of particular hardware boards. Instead, the proofs are now parametrised over these locations. This means that for verified configurations of seL4 the kernel’s memory location can be freely changed within certain boundaries while automatically preserving the proofs, without any involvement needed from proof experts.
This parametrisation is one of the steps necessary for the proof to later support the presence of multiple kernels in memory at once.
# 2023-06-27 - Learn more about Proofcraft's family: Corey, Michael and Ryan
In May 2022, we shared with you that Proofcraft’s family was getting bigger. Learn a bit more about our top proof engineers Corey, Michael and Ryan:
# 2023-05-04 - Proofcraft leaders among ACM Software Systems award recipients!
Gerwin, June and Rafal, the 3 founders and leaders of Proofcraft, have received, together with their former colleagues at the Trustworthy Systems group, the prestigious ACM Software System Award, for the “development of the first industrial-strength, high-performance operating system to have been the subject of a complete, mechanically-checked proof of full functional correctness”.
This award, from the Association of Computing Machinery, the world’s largest scientific and educational computing society, recognises the development of a software system that has had a lasting influence, reflected in contributions to concepts, in commercial acceptance, or both.
The award highlights how much seL4 has fundamentally changed the research community’s perception of what formal methods can accomplish: it showed that not only is it possible to complete a formal proof of correctness and security for an industrial-strength operating system but that this can be accomplished without compromising performance or generality. The continuously maintained and growing proofs on seL4 have helped to give rise to a new discipline of proof engineering—the art of proof process modelling, effort estimation, and the systematic treatment of large-scale proofs.
Proofcraft is dedicated to keep pushing the application of formal methods and proof engineering to real-world systems software, increasing its reliability, safety and security.
# 2023-04-14 - Proofcraft celebrates its 2nd anniversary!
People often ask us how things are going at Proofcraft.
As we are celebrating 2 years since we launched this new adventure, we are happy to share that things are looking good! :)
Working at Proofcraft is great and we are having a lot of fun pushing the vision of a verified future.
Our second year has seen us delivering the invariant proofs for seL4 on the latest 64-bit Arm architecture, starting on the design-to-code refinement proof of the Mixed-Criticality-System configuration of seL4, presenting our roadmap for seL4 verification at the seL4 summit, and importantly seeing the Proofcraft family getting bigger with Corey, Michael and Ryan joining!
Amongst other things :)
Looking forward to the years ahead.
# 2023-03-30 - Proofcraft completes the proof that seL4 AArch64 preserves all key invariants
The level of assurance for seL4 on AArch64 is getting stronger.
After having formalised, in March 2022, the abstract specification (what the kernel is supposed to do), and the design specification (how the kernel is designed), Proofcraft has now completed the proof that the abstract specification preserves all key invariants about kernel data structures. This represents a significant proportion of the effort needed to establish the full functional correctness of seL4 on AArch64.
# 2023-02-04 - Listen to Gerwin's interview on Type Theory Forall podcast
Listen to Gerwin talk about his formal verification journey and thoughts on the field, from his PhD on Java Virtual Machine verification and him leading the landmark verification of the seL4 kernel, to creating Proofcraft to provide commercial support in formal verification, and much more. Grab a cup of coffee, or go for a walk with your earphones, or save it for your next flight, and listen to Gerwin sharing his insights, thoughts and anecdotes on this Type Theory Forall podcast.