seL4 summit logo

seL4 Summit 2024

Sydney, Australia

15-17 October 2024

Program

All times are local time in Sydney, Australia (GMT+11).

Social activities

Weekend of Oct 12 & 13, 2024: Potential bush walking led by Gernot Heiser (contact him if interested).

Mon Oct 14, 2024: Informal Social Activities will be organised by local Sydney-siders. Stay tuned.

Summit

Day 1 15 October 2024
9:00 - 9:10 Announcements Welcome
9:10 - 10:00 Keynote Industrial Scale Proof Engineering for Critical Trustworthy Applications (INSPECTA)
Darren Cofer, Collins Aerospace
Break
10:30 - 11:00 Talk seL4 Verification: Status and Plans
Gerwin Klein, June Andronick, Rafal Kolanski, Gerwin Klein, Corey Lewis, Michael McInerney, Proofcraft
11:00 - 11:30 Talk seL4 multikernel roadmap and concurrency verification
Gerwin Klein, Corey Lewis, Proofcraft
11:30 - 12:00 Talk The Neutrality Atoll Hypervisor and the seL4 Multikernel
David Cock, Mathieu Mirmont, Stevens Le Blond, Neutrality
Lunch
13:30 - 13:45 Talk Lions OS: Secure, fast, adaptable!
Gernot Heiser, UNSW Sydney
13:45 - 14:15 Talk In and Around LionsOS
Ivan Velickovic, UNSW Sydney
14:15 - 14:30 Talk The Secure Multiserver Operating System Framework
Alwin Joshy, Kevin Elphinstone, Gernot Heiser, Craig McLaughlin, UNSW Sydney
14:30 - 15:00 Talk Running Certified Operating Systems under the seL4 Hypervisor
Chris Guikema, DornerWorks
Break
15:30 - 16:00 Talk Securing ROS Systems with seL4
Nathan Studer, Alex Pavey, Zach Clark, DornerWorks, Dariusz Mikulski, Cristian Balas, Yale Empie, US Army - Ground Vehicle Robotics
16:00 - 16:15 Talk Experience Developing Code for the seL4 Environment
Caitlyn Wilde, Wyeth Greenlaw Rollins, Alain Kägi, Lewis & Clark College
16:15 - 16:30 Talk Transitioning from CAmkES VMM to MicroKit VMM
Leigha VanderKlok, DornerWorks
16:30 - 16:45 Talk seL4 on RISC-V:building safe and fast firmware
Lei Mao, Horizon Robotics
Networking event: drinks and nibbles
Day 2 16 October 2024
9:00 - 9:50 Panel
9:50 - 10:00 seL4 Foundation update
Break
10:30 - 11:00 Talk First steps towards verification of user-space systems
Matthew Brecknell, Kry10
11:00 - 11:30 Talk Generating Trustworthy Software/Hardware I2C Drivers
Daniel Schwyn, Zikai Liu, Timothy Roscoe, ETH Zurich
11:30 - 11:45 Talk Using Model Checking to Develop and Verify Inter-Component Signalling Protocols
Courtney Darville, UNSW Sydney
11:45 - 12:00 Talk Rust Support in seL4 Userspace: Overview and Update
Nick Spinale, Colias Group, LLC
12:00 - 12:15 Talk Pancake: a language for verified systems programming
Miki Tanaka, Johannes Åman Pohjola, Gernot Heiser UNSW Sydney
Lunch
13:45 - 14:15 Talk Assured Reserve Modes
Ihor Kuz, Kry10, Lance Joneckis, Idaho National Laboratory
14:15 - 14:30 Talk Assured Reserve Modes in Action
Ihor Kuz, Kry10, Lance Joneckis, Idaho National Laboratory
14:30 - 14:45 Talk Supporting container applications on Kry10 OS
Alison Felizzi, Kry10
14:45 - 15:00 Talk Exploring an seL4-based Trusted Execution Environment in a RISC-V Platform
Everton de Matos, TII
Break
15:30 - 16:00 Talk Bridging Academia and Industry
Yanyan Shen, Dhammika Elkaduwe, NIO
16:00 - 16:30 Talk Journeys with seL4
Bill Ellis, James Nevell, Stephen Williams, Josh Felmeden, Daniel Storer, Tom Harvey, Capgemini
16:30 - 16:45 Talk Building a Commercial Virtualized Mobile Device with seL4 – Part 3
Jason Sebranek, Cog Systems, Inc.
16:45 - 17:00 Talk Setting up Nix for Cross Compilation
Wanja Zaeske, Deutsches Zentrum für Luft- und Raumfahrt (DLR)
Dinner
Day 3 17 October 2024
9:00 - 9:50 Keynote seL4 in Software-Defined Vehicles: Vision, Roadmap, and Impact at NIO
Ning Qu, NIO
9:50 - 10:00 Announcements
Break
10:30 - 11:00 Talk seL4 CHERI/Morello port
Hesham Almatary, Capabilities Limited
11:00 - 11:15 Talk Hardware Support for Time Protection
Nils Wistoff, ETH Zurich, Gernot Heiser, UNSW Sydney, Luca Benini, ETH Zurich & University of Bologna
11:15 - 11:45 Talk Two new frontiers for seL4's refinement proofs: Time protection and Microkit-based OS service verification
Robert Sison, UNSW Sydney
11:45 - 12:15 Talk seL4 as a CPU Driver for an OS for Real Computers
Roman Meier, Zikai Liu, Ben Fiedler, Timothy Roscoe, ETH Zurich
Lunch
13:30 - 13:45 Plenary Discussion, BoF Teasers
14:00 - 15:00 Plenary BoFs
Break
15:30 - 16:30 Plenary BoFs
16:30 - 16:45 Plenary Report from BoFs + Discussion
16:45 - 17:00 Concluding remarks
Day 4 18 October 2024 Training day @UNSW (TBC) 
Training Using Lions OS
Ivan Velickovic, UNSW Sydney
Training Rust Support in seL4 Userspace
Nick Spinale, Colias Group, LLC