seL4

News about seL4 and the seL4 Foundation

19 Feb 2021: HENSOLDT Cyber receives interim endorsement

HENSOLDT Cyber The seL4 Foundation has extended Interim Endorsement as Trusted Service Provider to HENSOLDT Cyber, for consulting and development services for seL4-based systems. More on:

11 Feb 2021: seL4 Foundation endorses service providers

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.

DornerWorks logo Breakaway Consulting logo Cog logo

8 Feb 2021: Penten joins the seL4 Foundation

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.

31 Dec 2020: seL4 YouTube Channel

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.

9 Nov 2020: seL4 12.0.0 release

seL4 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:

15 Oct 2020: 3rd seL4 summit to take place on 15-18 Nov

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

22 Jul 2020: Adventium Labs joins the seL4 Foundation!

Adventium Labs logo 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.

9 Jun 2020: functional correctness proof of seL4 RISC-V

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.

2 Jun 2020: UNSW seL4 teaching videos available

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.

25 May 2020: seL4 Foundation whitepaper released

seL4 Whitepaper 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.

9 Jun 2020: Breakaway Consulting joins the seL4 Foundation!

Breakaway logo 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.

7 Apr 2020: Launch of the seL4 Foundation

seL4 foundation launch 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.

More information on the Blog post about "The seL4 Foundation — What and Why", and in the press releases from the Linux Foundation and from CSIRO's Data61.