Today, the seL4 Foundation and RISC-V International announced that the verified seL4 microkernel on the RV64 architecture has been proved down to the executable code by CSIRO’s Data61, thanks to funding provided by HENSOLDT Cyber GmbH. This guarantees that the seL4 microkernel on RV64 will operate to specification even when built with an untrusted C compiler, GCC.
Within and across open collaboration communities it is essential to work together on areas of mutual interest. RISC-V and seL4 are pleased to announce their progress and their alliances as they join forces to enable stronger overall security, combining security-oriented architecture and operating system design.
“We are excited to be one of the first architectures with secure operating system kernels with such a strong formal verification story,” said Mark Himelstein, CTO of RISC-V International. “RISC-V is continuing to increase the security features that encompass the ISA and the secure seL4 kernel is a natural complement.”
“This is another milestone for seL4, which continues to define the state of the art in OS security,” added Prof Gernot Heiser, Chairman of the seL4 Foundation. “Stronger aligning the two open ecosystems makes a lot of sense.”
“The verified seL4 microkernel forms the core of TRENTOS, our secure operating system for our MiG-V chip, a RISC-V processor with supply chain security”, said Sascha Kegreiß”, CTO of HENSOLDT Cyber GmbH. “This unique combination of hardware and software security can protect critical assets from advanced persistent cyber threats.”
”Translation validation ties all of our verification efforts together,” said Dr Zoltan Kocsis, CSIRO Verification Engineer. “Bringing translation validation to a modern, 64-bit processor presented significant scalability challenges but, in the end, we were able to overcome them.”
For more details on binary verification of seL4 on RISC-V see Gernot's blog: seL4 on RISC-V Verified to Binary Code (and seL4 and RISC-V Foundations form an alliance).
The seL4 Foundation is pleased to welcome ETH Zurich as associate member, and is looking forward to further strengthening of ETH's engagement with seL4.
The seL4 Foundation now has an easy way for the general public to support financially the development of seL4 and its open-source ecosystem, using the Linux Foundation's LFX portal.
The seL4 Foundation welcomes Raytheon Technologies as our latest member.
Members of the Raytheon Technologies team have been long-time core participants in the seL4 ecosystem, predating the company’s formation in 2020, which brought together Raytheon Company and United Technologies’ aerospace businesses, Collins Aerospace and Pratt & Whitney. Collins Aerospace was a prime contractor in the DARPA HACMS program, which demonstrated the seL4-based incremental cyber retrofit of autonomous military vehicles. This was a major milestone in the growth of seL4, demonstrating that it protects against cyber attacks on real systems in operation. The same Raytheon Technologies team now leads the follow-on DARPA CASE program, aiming at designed-in cyber-resiliency, including the seL4-based framework for verified initialisation and configuration of systems architectures.
The seL4 Foundation has commenced providing interim endorsement for trusted service providers for seL4. These may apply to consulting and development services as well as for training. In a first step, the Foundation has given interim endorsement to the following trusted service providers (in the order of approval):
Interim endorsement is intended to lead to full certification; the Foundation will work with interim endorsees and the general membership on developing certification schemes. More detail.
The seL4 Foundation welcomes Penten Pty Ltd as our newest member. Penten is based in Canberra, Australia, and specialises in secure communications technology and artificial intelligence. Penten has been developing seL4-based products for a number of years, some of which are in daily use in multiple defence forces.
There is now a YouTube channel run by the seL4 Foundation. It presently has two playlists, one with the recordings of the seL4 material from this year’s UNSW Advanced Operating Systems course, and one with seL4 Summit talks from Trustworthy Systems. More to come, enjoy.
Announcing the releases of seL4, CAmkES and CapDL under the seL4 Foundation. Below you can find links to release notes with updates to other supporting projects to come before the end of the year. Versioned Releases:
The 3rd seL4 Summit will take place (virtually) on 15–18 November (US East Coast time). The program features a tutorial and 3 days packed with great talks and panels. Presentations will be streamed according to the schedule and available for download right after, and there will be an on-line discussion forum. Registration is only $80US
We’re happy to announce the newest member of the seL4 Foundation: Minneapolis-based company Adventium Labs. Adventium Labs develops solutions for safe and secure software-intensive complex systems, with specialties in separation architectures, model-based system engineering, and mathematical analysis technologies. They are leveraging these capabilities to extend seL4 into safety and security critical industries, including medical devices, defense and commercial avionics, and industrial control.
RISC-V (RV64) is the third ISA with verified seL4. The functional correctness proof of seL4 on the RV64 ISA has completed. Congratulations to the awesome Proof Engineering Team of the Trustworthy Systems group on achieving this major milestone for seL4! And many thanks to HENSOLDT Cyber for making it possible. What we have now is the refinement proof from the seL4 formal spec to the C implementation, putting RV64 on the same level as x64 in terms of seL4 verification. The binary verification, which extends this refinement to the binary code of the kernel is progressing, stay tuned for more news on that in the foreseeable future. More on this in this blog post.
Yet another contribution of UNSW Sydney to the seL4 community: This year Gernot Heiser is making the seL4-related videos from his UNSW Advanced Operating Systems class freely available. You’ll find them at the UNSW CSeLearning COMP9242 YouTube channel. At present there are the first two modules, which provide some background on microkernels and seL4, and discuss the seL4 API. More material will show up over the next two months. The complete course material, including all lecture slides, the project spec and code, are available, as always, from the COMP9042 web site.
The whitepaper "The seL4 Microkernel – An Introduction" provides an introduction to and overview of seL4. We explain what seL4 is (and is not) and explore its defining features. We explain what makes seL4 uniquely qualified as the operating-system kernel of choice for security- and safety- critical systems, and generally embedded and cyber-physical systems. In particular, we explain seL4’s assurance story, its security- and safety-relevant features, and its benchmark-setting performance. We also discuss typical usage scenarios, including incremental cyber retrofit of legacy systems. You can download here.
We’re happy to announce the first new member since the launch of the seL4 Foundation: Sydney-based company Breakaway Consulting. Through Founder and Managing Director Ben Leslie, Breakaway comes with 20 years of experience in L4 microkernels and systems based on various L4 kernels. Prior to founding Breakaway, Ben was a student with what is now the TS Group, and then VP Engineering of Open Kernel Labs. Breakaway offers consulting services on architecture, design and implementation of seL4-based systems.
The Trustworthy Systems group is excited to announce the creation of the seL4 Foundation. Its aim is to provide a neutral and independent organisation to ensure the longevity of seL4, and grow its ecosystem of adopters and contributors. It has a high-profile Board consisting of Gernot Heiser (Chair), June Andronick, Gerwin Klein, John Launchbury, Sascha Kegreiß, Daniel Potts. It already has a number of members, including major adopters HENSOLDT Cyber and Ghost Systems, and providers of services for seL4, Cog Systems and DornerWorks. Please check the membership page for details and how to join. The seL4 Foundation is set up under the Linux Foundation, which provides a mature and well-known framework.