Proofcraft News - 2022

Happy Holiday Season from Proofcraft!

Raf's talk on seL4 verification roadmap is up on Youtube

The videos and slides of the seL4 summit 2022 are now available online on the seL4 YouTube channel, including Raf’s presentation of the seL4 verification roadmap.

June is invited speaker at FMCAD

June is giving one of the two invited talks at FMCAD 2022 in Trento, Italy. She is presenting “The seL4 verification journey: how have the challenges and opportunities evolved”.

Almost two decades ago, the seL4 verification journey started as a research project aiming for a highly challenging problem with the potential of significant impact.

Today, seL4’s increased uptake and adoption creates both opportunities and challenges to keep seL4 being the most highly assured OS kernel, with proofs of an increasing number of properties and for an increasing number of hardware architectures: Arm (32-bit), x86 (64-bit) and RISC-V (64-bit), with proofs now starting for Arm (64-bit) at Proofcraft.

Strong presence of Proofcraft at the seL4 summit in Munich!

Raf presented Proofcraft’s seL4 verification roadmap at the seL4 summit 2022, which gathered 70 people in Munich, Germany, featuring all major actors of the seL4 ecosystem and a strong presence from Proofcraft.

As member of the seL4 Foundation’s Technical Steering Committee, Raf, Gerwin and June were together on stage for the “Ask Me Anything” session. Gerwin also gave an overview of the seL4 GitHub test suite, while June co-chaired the whole event.

Proofcraft presenting its seL4 verification roadmap at the seL4 summit 2022

Proofcraft will be presenting its seL4 verification roadmap at the seL4 summit on October 10th 2022 in Munich, Germany. The summit will gather all major actors of the seL4 ecosystem.

Verification makes seL4 unique. With increasing adoption, seL4 is evolving to support more platforms, architectures, configurations, and features, meaning its formal proofs must evolve as well. Proofcraft is committed to keep this evolution alive. In this talk, we will present the status of the seL4 verification roadmap, from tackling the verification of seL4 on the AArch64 architecture, to continuing the verification of MCS seL4 (the Mixed-Criticality-System configuration of the kernel), to investigations to push the verification of seL4 on multicore platforms.

Verification of MCS seL4 continues at Proofcraft

The latest major seL4 feature is the support for mixed-criticality systems (MCS), leading to the new MCS configuration of seL4 (MCS seL4). This configuration is indispensable for real-time applications such as automotive uses cases, and once verified it will become the default seL4 configuration.

The verification of functional correctness for MCS seL4 has seen significant progress in the last few years at the Trustworthy Systems group, with the invariant proofs and the abstract-to-design refinement proof completed.

Proofcraft has now started the design-to-code refinement proof of MCS seL4, the last step to complete functional correctness, thanks to some initial funding from the seL4 Foundation.

If you are interested in supporting these next stages of the MCS seL4 verification, contact us at contact@proofcraft.systems. You can also donate towards the MCS verification project through the seL4 Foundation.

Chairing the international conference on Interactive Theorem Proving

Interactive theorem proving, the technique Proofcraft uses for the formal verification of software systems like seL4, is in the spotlight this August in Haifa, Israel.

June co-chairs ITP'22, a conference featuring the latest research in interactive theorem proving from theoretical foundations to implementation aspects and applications in program verification, security, and the formalization of mathematics.

Every 4 years, ITP is part of FLoC, the Federated Logic Conference (FLoC), gathering leading international conferences related to mathematical logic and computer science. This year, FLoC includes 12 conferences and over 60 workshops on topics of software/hardware verification and logic for computer science.

NCSC supports Proofcraft's seL4 verification roadmap!

Proofcraft and UNSW receive invaluable support from the UK’s National Cyber Security Centre (NCSC).

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 contact@proofcraft.systems. You can also donate towards the AArch64 verification project through the seL4 Foundation.

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!

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!

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.

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!

Invited talk on the reality of commercial support for seL4

Alongside 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.

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.