The seL4 Summit 2023

seL4 Summit 2023 Program

The seL4 Summit 2023 features a combination of technical research and development, real-world seL4 deployment insights, in-depth interactive discussions, thought-provoking keynotes, panel discussions, as well as a training session. Videos are available on the seL4 YouTube channel.

Program-at-a-glance

Keynote
 Keynote
Talks
 Talks
Panel
 Panel
Reception
 Reception
Dinner
 Dinner
Talks
 Talks
Talks
 Talks
BoFs
 BoFs
BoFs
 BoFs
Tue Sep 19
 Tue Sep 19
Wed Sep 20
 Wed Sep 20
Thu Sep 21
 Thu Sep 21
Training
 Training
Day 1
Day 1
Day 2
Day 2
Day 3
Day 3
Talks
 Talks
Talks
 Talks
Talks
 Talks
Talks
 Talks
Talks
 Talks
Talks
 Talks
Keynote
 Keynote
Talks
 Talks
Talks
 Talks

Main Program

All times are local time in Minneapolis, USA (GMT-5). Session chairs shown on right.

Day 1 19 September 2023
9:00 - 9:10
Welcome
Darren Cofer, Ihor Kuz, Collins Aerospace, Kry10
YouTube icon
Slides
Darren Cofer
9:10 - 10:00
Keynote
Scoping assurance activities with seL4
Gage B, NCSC
Slides
Abstract
Break
10:15 - 10:45
Dynamic seL4 based systems: designing for verifiability
Matthew Brecknell, Kry10
YouTube icon
Slides
Abstract
Gerwin Klein
10:45 - 11:15
Formally Stepping Into The Unverified World
Sandy Frost, Los Alamos National Laboratory
YouTube icon
Slides
Abstract
Break
11:30 - 12:00
Reducing the reliance on verification experts for seL4 proofs
Gerwin Klein, Proofcraft
YouTube icon
Slides
Abstract
Matthew Brecknell
12:00 - 12:30
More multiprocessing on seL4: Are efficient SMP virtual machines possible on verifiable seL4 kernels?
Kent McLeod, Kry10
YouTube icon
Slides
Abstract
Lunch
13:30 - 14:00
System Information Flow Analysis
Ihor Kuz, Kry10
YouTube icon
Slides
Abstract
Robbie VanVossen
14:00 - 14:30
Advancements for Virtualization Support in seL4:CAmkES and seL4cp
Markku Ahvenjärvi, TII
YouTube icon
Slides
Abstract
Break
14:45 - 15:15
The seL4 Device Driver Framework
Lucy Parker, UNSW
YouTube icon
Slides
Abstract
Nick Spinale
15:15 - 15:45
R&D Update from TS
Gernot Heiser, UNSW
YouTube icon
Slides
Abstract
Break
16:00 - 16:15
seL4: Experiences, Improvements and Optimizations
Chris Guikema, DornerWorks
YouTube icon
Slides
Abstract
Axel Heider
16:15 - 16:30
From Zero to a Native xHCl Driver
Josh Felmeden, Capgemini Engineering
YouTube icon
Slides
Abstract
16:30 - 16:45
Crashing For Reliability
Ihor Kuz, Kry10
YouTube icon
Slides
Abstract
16:45 - 17:00
seL4 Foundation update
June Andronick, seL4 Foundation
YouTube icon
Slides
Break
17:00 - 17:15
Gold Sponsor
Building a Platform for Critical Devices in the “Real World”
Boyd Multerer, Kry10
YouTube icon
Slides
Abstract
June Andronick
Networking event: drinks and nibbles 18:00
Day 2 20 September 2023
9:00 - 9:50
Keynote
CantripOS: An OS for Ambient ML Applications
Sam Leffler, Google
YouTube icon
Slides
Abstract
Ihor Kuz
9:50 - 10:00
Announcements
June Andronick, Proofcraft
YouTube icon
Break
10:15 - 10:45
Magnetite: Rust-Based OS Services for seL4
Juliana Furgala, MIT Lincoln Laboratory
YouTube icon
Slides
Abstract
Lucy Parker
10:45 - 11:15
Showcase: Microkernel OS, TPMs, and WASM in Ilo T Environments
Sid Hussmann, Gapfruit
YouTube icon
Slides
Abstract
Break
11:30 - 12:00
Rust support in seL4 userspace: update and roadmap
Nick Spinale, Colias Group
YouTube icon
Slides
Abstract
Kent McLeod
12:00 - 12:30
The seL4 Microkit
Ivan Velickovic, UNSW
YouTube icon
Slides
Abstract
Lunch
13:30 - 14:00
Leveraging Rust for Core Platform
Ben Hamlin, Galois
YouTube icon
Slides
Abstract
Todd Carpenter
14:00 - 14:30
Panel
OS on seL4: so many options!
Gernot Heiser, Sid Hussmann, Kent McLeod, Juliana Furgala, UNSW, Gapfruit, Kry10, MIT Lincoln Laboratory
YouTube icon
Abstract
Break
14:45 - 15:15
seL4 VMM on the RISC-V Rocket Chip
Robbie VanVossen, DornerWorks
YouTube icon
Slides
Abstract
Gernot Heiser
15:15 - 15:45
seL4 on Arm Morello
Martin Atkins, Mission Critical Applications
YouTube icon
Slides
Abstract
Break
16:00 - 16:30
Incremental assurance for a Rust network stack
Michal Podhradsky, Galois
YouTube icon
Slides
Abstract
Gerwin Klein
16:30 - 16:45
Toward a Verified, Minimal IPv6 Network Stack Implementation
Wyeth Greenlaw Rollins, Lewis & Clark College
YouTube icon
Slides
Abstract
16:45 - 17:00
IOMMU (take the ARM SMMUv3 for instance) solution for seL4
Lei Mao, Horizon Robotics
YouTube icon
Slides
Abstract
17:00 - 17:15
Gold Sponsor
OS for Software Defined Vehicle
Qiyan Wang, NIO
YouTube icon
Slides
Abstract
June Andronick
17:15 - 17:30
Gold Sponsor
Secure Systems in Focus: Challenges, Solutions, and Future Directions
Everton de Matos, TII
YouTube icon
Slides
Abstract
Dinner 19:00
Day 3 21 September 2023
9:00 - 9:30
SIG update + Community update/discussion
Yanyan Shen, Matthew Brecknell, Everton de Matos, Kent McLeod, NIO, Kry10, TII, Kry10
YouTube icon
Abstract
Darren Cofer
9:30 - 10:00
seL4 Virtualization (ARMv8 Edge Device) Guest OS Performance & HA Recovery
Lei Mao, Horizon Robotics
Abstract
Break
10:15 - 10:30
Building a Commercial Virtualized Mobile Device with seL4 - Part 2
Jason Sebranek, Cog Systems
YouTube icon
Slides
Abstract
Ihor Kuz
10:30 - 10:45
seL4 on RISC-V: Building a Trusted Execution Environment
Everton de Matos, TII
YouTube icon
Slides
Abstract
10:45 - 11:00
Trustworthy Measurements of a Linux Kernel and Layered Attestation via the seL4
Michael Neises, University of Kansas
YouTube icon
Slides
Abstract
Break
11:30 - 11:45
BoFs teasers
Darren Cofer, Ihor Kuz
Rooms 1 & 2
11:45 - 12:30
BoF
Lunch
Rooms 1 & 2
13:30 - 14:15
BoF
Room 1
14:15 - 14:30
Report from BoFs + Discussion
Darren Cofer, Ihor Kuz
Break
14:45 - 16:30
Training
A quick start to seL4 with the Core Platform
Ivan Velickovic, UNSW