Happy Holiday Season from Proofcraft!
Proofcraft News - 2023
Thank you XCalibyte for your donation towards MCS seL4 verification!
Proofcraft and the seL4 Foundation would like to jointly thank XCalibyte for supporting the continuation of the MCS seL4 verification.
As previously announced, thanks to some initial funding from the seL4 Foundation, Proofcraft was able to start the design-to-code refinement proof of MCS seL4. With further XCalibyte’s support, Proofcraft further progressed this verification step, delivering the completion of the proof framework, setting up all the infrastructure and hierarchy of theorems about the approximately 500 C functions of the kernel.
If, like XCalibyte, you are keen to get a verified MCS seL4, to benefit from a high-assurance support for mixed-criticality systems (MCS), you can contact Proofcraft at contact@proofcraft.systems or you can donate towards the MCS verification project using the seL4 Foundation donation mechanism like XCalibyte has done.
Support for mixed-criticality systems is the latest major seL4 feature and MCS seL4 is aimed to become the default seL4 configuration, once verified. It is indispensable for real-time applications such as automotive use cases and is beneficial beyond such applications. It therefore represents one of the highest priority items in the seL4 formal verification roadmap.
MCS seL4 solves the problem in standard real-time systems where high frequency of tasks is tied to high priority, which in turn implies high trust. This can lead to low-criticality, low-assurance tasks (such as in-car entertainment systems) to be given high-priority because they require high-frequency access to hardware, which can then cause starvation of highly critical tasks (such as engine bus control access). MCS seL4 uniquely solves this problem by adding the essential building blocks for ensuring timeliness in mixed-criticality systems.
Gerwin presenting at the seL4 summit
The seL4 summit 2023 gathered last week a full room of seL4 industry leaders, researchers and enthusiasts in Minneapolis. Gerwin presented Proofcraft’s planned project to reduce the reliance on verification experts for seL4 proofs. This includes, for instance, almost completely automating the verification of platform ports within existing verified architectures of the seL4 kernel. Instead of requiring the involvement of experts, we plan to develop proof automation that greatly reduces the verification overhead of porting to a new platform. The ultimate goal is to reduce the time to produce new ports from months to hours.
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.
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.
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.
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:
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.
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.
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.
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.