seL4 Summit 2023

Minneapolis, USA

19 - 21 September 2023

Important Dates

~~Abstracts due: 24 April 2023~~
~~Notification of decisions: 9 June 2023~~
~~Early bird cut-off: 18 August 2023~~
Summit: 19-21 September 2023

About

The seL4 Summit is the annual international summit on the seL4 microkernel, the world's most highly assured OS kernel, as well as on all seL4-related technology, tools, infrastructure, products, projects, and people.

It aims to gather all the seL4 community to learn, share, and connect:

learn about the seL4 technology, its latest progress, use, successes, challenges, plans;
share exciting seL4 development, research, experience, application in the real world;
connect with other seL4 developers, users, providers, customers, supporters, potential partners and enthusiasts.

The seL4 Summit is organised by the seL4 Foundation, in a location aimed to be on a different continent each year, as far as possible.

An open call for presentations invites submissions of short abstracts about cool work on seL4, and a Program Committee made of a wide range of representatives of the seL4 community is in charge of the technical content (reviewing submission, selecting invited speakers, defining the program).

Registration

Registrations are now open here.

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

Tickets include:

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

Location and Venue

All information about location and hotels can be found here.

The seL4 Summit 2023 will be held in Minneapolis, USA, 19 - 21 September 2023, at the Elliot Park Hotel. The summit will be hosted by the Linux Foundation, and will be an in-person event. There will be no option for a live remote participation but the event will be recorded and all talks (for which the presenter accepted to be recorded) will be made available shortly after the summit on the seL4 YouTube channel.

Keynotes

We are pleased to announce that the two keynotes for the seL4 summit 2023 will be Gage from NCSC and Sam Leffler from Google!

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

Gage's keynote will be about "Scoping assurance activities with seL4"

Abstract

In both the safety and security industries, high levels of product assurance are sought to mitigate the risk of product failure. Often this means that software developers need to demonstrate that all functions do what they are supposed to do, the product does not do anything it is not supposed to do, and that the product is free from all known bugs and vulnerabilities.

Whilst none of these requirements have trivial solutions, testing does a reasonable job of checking the correctness of functions. Similarly, taking advantage of tooling (such as static analysis, dynamic analysis), tracking the discovery of bugs and vulnerabilities, and having a refined software patching process helps to mitigate the presence of bugs and vulnerabilities.

However, it is much less obvious how one can gain confidence that the software has no unintended functionality without checking the entire software implementation. Even then, the scope of what you need to check is potentially unbounded (we’re looking for the unknown unknowns after all), issues will still be missed, and the resource requirements are high.

In this talk, I will describe how basing a software product on seL4 facilitates the scoping of this no unintended functionality problem, and in turn, reduces the amount of effort required when it comes to demonstrating assurance of a security product. By walking through an example, we’ll observe the assurance benefits of component isolation, data flow control, how seL4 helps to direct where we should focus our assurance efforts, and any caveats we should be aware of.

Accepting that the assurance effort should be commensurate with the criticality of the security product, my hope is that this presentation provides a sliding scale of seL4 features we should seek to take advantage of, be it for articulating an assurance case, or conducting an independent assessment.

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.

Sam's keynote will be about "CantripOS: An OS for Ambient ML Applications"

Abstract

CantripOS is an open source operating system purpose-built to run ML workloads for embedded systems. It is being developed as part of Google’s project Sparrow, whose charter is to build a low-power embedded platform for ML applications with a focus on security and privacy. CantripOS is built in the Rust programming language, runs under the seL4 microkernel, and uses a modified CAmkES framework. This allows CantripOS to run dynamically loaded applications in a controlled sandbox, while still retaining the benefits of a statically designed system. This paper describes the system design, modifications made to seL4 and CAmkES, and future directions. All the work described here is publicly available on GitHub.

Panellists

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.

Sid Hussmann
Gapfruit

Kent McLeod
Kry10

Juliana Furgala
MIT Lincoln Laboratory

Gernot Heiser
Trustworthy Systems UNSW

Todd Carpenter, Moderator
Galois

Program

Have a look at the seL4 summit Program! 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.