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.