seL4 News

Each year, DARPA leadership selects the Game Changer program that was the most impactful in the preceding 10 years.

This year, the award goes to HACMS, the High-Assurance Cyber Military Systems program, which has been instrumental in demonstrating how seL4 can be embedded in real-world products (unmanned air and ground vehicles) and truly protect them from cyber attacks.

The award was presented by DARPA Director Stefanie Tompkins to the three HACMS program managers, Kathleen Fisher, John Launchbury, and Ray Richards. We truly thank all three for their visionary leadership.

Our deep thanks to Darren Cofer as well, who masterfully lead the team, made of Collins, Galois, Boeing, University of MN and the Trustworthy Systems group (home of seL4 at the time) who demonstrated the technology on Boeing’s Unmanned Little Bird helicopter, including cyber attacks during flight!

A true game changer indeed.

We are excited to share that NIO recently unveiled their seL4-based SkyOS operating system, designed for Software Defined Vehicles, which they have been working on relentlessly for the past two years. At the seL4 Summit 2023 Qiyan Wang, NIO’s Global VP of Digital Systems, announced that NIO cars based on seL4 are planned for next year!

The seL4 Microkit, formerly known as the Core Platform, is an operating system framework on top of seL4 provides a small set of simple abstractions that ease the design and implementation of statically structured systems on seL4, while still leveraging the kernel’s benefits of security and performance. The Microkit is distributed as an SDK that integrates with the developer’s build system of choice, significantly reducing the barrier to entry for new users of seL4.

The seL4 Microkit was developed in collaboration between Breakaway Consulting Pty Ltd and Trustworthy Systems, UNSW, and is now an official seL4 Foundation project, making it part of the seL4 eco-system.

For the last year, Nick Spinale, funded by the seL4 Foundation, has been developing support for the Rust programming language in seL4 userspace.

Nick has created a comprehensive language support infrastructure that integrates well with the rest of the seL4 ecosystem (capDL, Microkit, sel4test) and also integrates well with what Rust programmers would expect from the language side. This work has now been accepted by the seL4 Foundation Technical Steering Committee and can be found on GitHub. Nick’s talk at the recent seL4 summit is on seL4’s Youtube channel. A demo system that uses the device driver framework, asynchronous programming in Rust and library support from the Rust ecosystem to implement a small web server is available on GitHub.

The overall outcome will be to allow people to write safer user-level code on top of seL4 without needing full formal verification, with a language that is receiving increasing interest and that aligns extremely well with security and safety critical embedded systems programming.

Foundation member Proofcraft has delivered a work package towards the verification of the MCS variant of seL4.

Having earlier started the design-to-code refinement proof of MCS seL4, funded by the Foundation, Proofcraft has now delivered the completion of the proof framework, setting up all the infrastructure and hierarchy of theorems about the approximately 500 C functions of the kernel.

This was made possible by a generous donation from Foundation member XCalibyte, for which the seL4 Foundation is very grateful. We are looking for further funding that will allow completion of the verification of the MCS variant. Once verified, MCS will become the default configuration of seL4, bringing the highest levels of assurance to mixed-criticality real-time systems.

Videos of the seL4 Summit 2023 are now available on the seL4 YouTube channel! Links and slides can be found on the summit Program and Abstracts pages. Thanks to all the speakers for making the seL4 Summit 2023 a great success!

The seL4 Foundation is pleased to welcome The University of Kansas as Associate Member. KU has collaborated with a number of seL4 Foundation members along the years, including in the DARPA CASE project, which produced a set of formal methods tools that can be applied throughout the design and build process to create seL4-based high-assurance cyber-resilient systems.

The seL4 Foundation thanks NIO for sponsoring both the reception and dinner for the seL4 Summit 2023. NIO is also a gold sponsor of the summit.

Email us at summit@sel4.systems if you are interested in sponsoring the seL4 Summit. More on sponsorship here.

We are very fortunate to welcome five industry leaders to participate at the seL4 Summit 2023, in a session OS on seL4: so many options!. Gapfruit, Kry10, Magnetite (MIT), and UNSW will present their views on the priorities and vision for their OS on seL4. The panel will be moderated by Todd Carpenter from Galois.

The seL4 Foundation thanks TII for becoming a Gold sponsor of the seL4 Summit 2023.

The Technology Innovation Institute’s (TII) Secure Systems Research Centre (SSRC) aims to drive end-to-end security and resilience in cyber-physical and autonomous systems that will ensure safety. The research center adopts an applied research approach, emphasizing practical applications. By employing seL4 as both a microkernel and a hypervisor, SSRC seamlessly aligns its dedication to security with the foundational technology crucial to achieving its objectives. This critical technology forms the cornerstone of secure software stacks for diverse edge devices, including secure communicators and drones. TII’s research not only contributes to but propels the evolution of cutting-edge high-end edge device environments. TII’s SSRC focus centers on resilience, isolation, trust, and security, all with the intention of fostering a more secure digital landscape.

Email us at summit@sel4.systems if you are interested in sponsoring the seL4 Summit. More on sponsorship here.

The seL4 Foundation thanks Kry10 for becoming a Gold sponsor of the seL4 Summit 2023.

Kry10 offers a full-featured operating system on top of the seL4 kernel, along with tooling, services, key management and more. The Kry10 Platform is a fast and easy way to build highly secure, next-generation cyber-physical devices. It leverages the verification of seL4 to provide a secure, self-healing, truly dynamic system with minimal downtime, even during upgrades.

Kry10 is an Endorsed Service Provider of the seL4 Foundation, offering support to enable seL4-based secure projects to be affordable, maintainable, and remotely manageable.

See here if you are interested in sponsoring the seL4 Summit 2023.

The seL4 Foundation thanks NIO for becoming our first Gold sponsor of the seL4 Summit 2023.

NIO is a global EV company funded in 2015 and that went public in the U.S. in 2018. NIO emphasizes user experience and technology innovation. NIO is a strong supporter of seL4 and a premium member of the seL4 Foundation. It has been investing heavily on building a full-fledge software platform for modern vehicles based on seL4.

See here if you are interested in sponsoring the seL4 Summit 2023.

The seL4 Foundation thanks Collins Aerospace for becoming a Silver sponsor of the seL4 Summit 2023.

Collins Aerospace, part of seL4 Foundation member Raytheon Technologies, has been a long-time core participant in the seL4 ecosystem. It 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 team also led 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 Summit 2023 will take place in Minneapolis, home town of this Collins Aerospace team involved in seL4.

See here if you are interested in sponsoring the seL4 Summit 2023.

Have a look at the program of the seL4 Summit 2023! We have a great line-up of interesting seL4 work, with a combination of technical research and development, experience reports of seL4 in the field, technical discussions and birds-of-a-feather sessions, as well as a training session on getting started with seL4.

We are pleased to announce that the two keynotes for the seL4 Summit 2023 will be Gage from NCSC and Sam Leffler from Google! Gage will talk about Scoping assurance activities with seL4 and Sam about CantripOS: An OS for Ambient ML Applications.

Gage is an Assurance Lead in NCSC with expertise in cryptography, software assurance and verification. He is part of a larger team that seeks to provide assurance and articulate risk for a wide range of products and customers. Whilst he is not a product developer himself, he has been responsible for presenting assurance cases for products that rely on seL4 to uphold security requirements.

Sam Leffler has worked at Google for nearly 15 years. He was part of the original team that developed ChromeOS and the ChromeBook, was responsible for the networking components of Project Loon, and worked on various infrastructure projects before joining Project Sparrow to help build the CantripOS embedded operating system. Prior to joining Google he was an independent contractor focused on wireless networking and operating systems. Before contracting he worked for VMware, Silicon Graphics, Pixar, Lucasfilm, and the Computer System Research Group (CSR) at UC Berkeley where he was responsible for the 4.2BSD release of the UNIX operating system. At CSRG he co-designed and implemented many of the facilities found in contemporary UNIX systems including sockets, networking support (IP/TCP), reliable signals, and more.

We are pleased to have Galois now part of the seL4 Foundation, following its acquisition of Adventium labs, which has been a member since 2020 and user of seL4 technologies for years before that. Galois develops technology to guarantee the trustworthiness of systems where failure is unacceptable. They apply cutting edge computer science and mathematics to advance the state of the art in software and hardware trustworthiness. The seL4 Foundation looks forward to our continuing collaboration.

The seL4 Summit 2023 will be held in Minneapolis, USA, 19 - 21 September 2023.

The seL4 Summit will cover the complete seL4 ecosystem, consisting of the verified microkernel, as well as all seL4-related technology, tools, infrastructure, products, projects, and people.

Tickets include:

• Participation in the 3-day conference, including talks, keynotes, seL4 updates & discussions
• Networking with other seL4 experts and enthusiasts
• Reception and Dinner

Register here

The early bird cut-off date is 18 August 2023.

The 2022 ACM Software System Award recognises seL4 as the first industrial-strength, high-performance operating system to have been the subject of a complete, mechanically-checked proof of full functional correctness, proofs of enforcement of the core security properties of integrity and confidentiality, a proof to the binary code of the kernel, and the first sound and complete worst-case execution-time analysis of a protected mode OS.

The award, recognising the development of a software system that has had a lasting influence, goes to Gernot Heiser, University of New South Wales; Gerwin Klein, Proofcraft; Harvey Tuch, Google; Kevin Elphinstone, University of New South Wales; June Andronick, Proofcraft; David Cock, ETH Zurich; Philip Derrin, Qualcomm; Dhammika Elkaduwe, University of Peradeniya; Kai Engelhardt; Toby Murray, University of Melbourne; Rafal Kolanski, Proofcraft; Michael Norrish, Australian National University; Thomas Sewell, University of Cambridge; and Simon Winwood, Galois.

We are committed to make sure that seL4’s recognised “lasting influence” live on for the decades ahead!

The seL4 Summit 2023 will be held 19 - 21 September 2023 at the Elliot Park Hotel, Minneapolis, USA.

The summit will be hosted by the Linux Foundation, and will be an in-person event.

Registration details to follow soon!

Remember that you have until 24 April 2022 to propose a talk. To propose a talk, upload an abstract of one page or less to the submission portal.

The seL4 Foundation welcomes the Autoware Foundation as a member.

The Autoware Foundation hosts the Autoware Project, the world’s leading open-source software project for autonomous driving.

As a member of the seL4 Foundation, the Autoware Foundation will work with members of the seL4 Foundation to implement a safe and secure Autonomous Driving software stack based on Autoware, leveraging the formally-verified and mixed-criticality capabilities of seL4.

Call For Presentations for the seL4 Summit 2023

• Share your seL4 work
• Share your seL4 experience
• Share your seL4 thoughts

Check the full Call For Presentations. To propose a talk, upload an abstract of one page or less by 10 April 2023 to the submission portal.

We are thrilled to announce our program committee for the seL4 Summit 2023. Our awesome team comes from various parts of the seL4 ecosystem: users, contributors, committers, experts, advocates, researchers, and engineers.

It is our pleasure to confirm that the seL4 Summit 2023 will be in:

The summit will be hosted by the Linux Foundation, and will be an in-person event.

We will announce a Call for Presentations in the coming weeks. Stay tuned!