Proofcraft News - 2022
# 2022-05-22 - NCSC supports Proofcraft's seL4 verification roadmap!
The UK Government uses the seL4 Microkernel to enforce separation in a number of high-assurance situations, and has announced its support for “the seL4 ecosystem via research and development funding for projects led by the University of New South Wales and Proofcraft”.
This funding kick starts the verification of seL4 on AArch64, the latest 64-bit Arm architecture, for which we have started delivering specifications. It will also support investigations to pursue the verification of seL4 on multicore platforms, and improving the binary correctness toolchain, in collaboration with Kry10.
If you are interested in supporting the next stages of the AArch64 seL4 verification, contact us at email@example.com. You can also donate towards the AArch64 verification project through the seL4 Foundation.
# 2022-05-02 - Proofcraft's family gets bigger, welcoming Corey, Michael and Ryan!We are very excited to welcome Corey Lewis, Michael McInerney and Ryan Barry! After working together in the Trustworthy Systems group, we are now reunited in Proofcraft, with ever more expertise and strength to tackle the challenge of a verified future!
They are all top proof engineers, already known for their achievements in the seL4 proof world: Corey in the area of multicore verification and the DARPA CASE project, Michael in the verification of MCS seL4’s first refinement and Ryan for the verification of seL4 security properties on RISC-V!
# 2022-04-14 - Proofcraft completes its 1st year!One year after incorporation, Proofcraft is looking good! We landed some big projects, we are delivering on significant milestones, we are about to welcome new key experts to the company, and, most importantly, we are having a lot of fun!
# 2022-03-31 - Proofcraft delivers seL4 AArch64 specs!The verification of seL4 on AArch64 is progressing! The first step in the proof of functional correctness (the proof that the C code behaves exactly as its abstract specification says) is to formalise the specification. There are two levels of specification for seL4: the abstract specification, describing what the kernel is supposed to do, and the design specification, which details design decisions and many data structures. Both of these specifications are now formalised for seL4 on AArch64.
# 2022-03-04 - Proofcraft gets contract to deliver on seL4 verification roadmap!
Proofcraft signs significant project to push the seL4 verification roadmap forward, including starting the verification of seL4 on AArch64, the latest 64-bit Arm architecture.
The seL4 microkernel is currently verified (to various degrees of depth) on 32-bit Arm, 64-bit x86 and 64-bit RISC-V. The verification of seL4 on 64-bit Arm, the main modern embedded platform, is in high-demand in the ecosystem. Proofcraft has started working on it!
# 2022-01-18 - Invited talk on the reality of commercial support for seL4Alongside Andrew Appel and Cesar Munoz, June gave one of the 3 invited talks at the international conference on Certified Programs and Proofs 2022 (CPP'22), co-located with POPL (Principles of Programming Languages).
In her talk, titled “The seL4 verification: the art and craft of proof and the reality of commercial support”, June reflects on the seL4 verification journey, past, present and future, and the challenges to combine the art and craft of proof with the reality of meeting industry demand for verified software.
The talk can be viewed online.
# 2022-01-12 - seL4 Proof Improvements delivered!
Raf and Gerwin delivered two neat improvements to the seL4 proof infrastructure in two projects: “NumDomains” and “AbsConfig”.
NumDomains made the seL4 proofs fully generic in the number of protection domains. Previously, the number of domains was hard-coded in the proofs. With this change, the proofs only need to be (automatically) re-run for a config change rather than needing an expert to update the proofs themselves.
AbsConfig tackled the duplication of seL4 configuration constants across all of the specification levels (abstract, design, and C) by automatically generating the abstract and design specification constants from the kernel build system. This will accelerate specification and proof updates when these values change, thereby reducing cost of porting seL4 proofs to new platforms.