seL4 summit logo

seL4 Summit 2024

Sydney, Australia

15-17 October 2024

Program

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

See the Schedule on LF Events.

Social activities

A number of informal social activities are being organised by local Sydney-siders. Check out the list and contact the organisers to register your interest.

Summit

Day 1 15 October 2024
Session chair
9:00 - 9:10 Announcements Welcome Ihor Kuz
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
Matthew Brecknell
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
Everton de Matos
13:45 - 14:15 Talk In and Around Lions OS
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
Gernot Heiser
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 Update seL4 Foundation Update
June Andronick, seL4 Foundation
16:45 - 17:00 Gold sponsor Real world needs and applications of seL4
Boyd Multerer, Kry10
Cocktail reception @ Verandah Public 18:00
Day 2 16 October 2024
Session chair
9:00 - 10:00 Panel
Nick Spinale
Break
10:30 - 11:00 Talk First steps towards verification of user-space systems
Matthew Brecknell, Kry10
Gerwin Klein
11:00 - 11:30 Talk Generating Trustworthy Hardware/Software I2C Drivers for Board Management Controllers
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
Robbie VanVossen
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
June Andronick
16:00 - 16:30 Talk seL4 Infrastructure: USB and Beyond
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 Doing Nix for seL4: Towards more Infrastructure-as-Code
Wanja Zaeske, Deutsches Zentrum für Luft- und Raumfahrt (DLR)
Dinner @ The Butler 18:00
Day 3 17 October 2024
Session chair
9:00 - 9:50 Keynote seL4 in Software-Defined Vehicles: Vision, Roadmap, and Impact at NIO
Ning Qu, NIO
Ihor Kuz
9:50 - 10:00 Announcements
Break
10:30 - 11:00 Talk Enhancing seL4’s C/C++ userspace memory safety using CHERI
Hesham Almatary, Capabilities Limited
Lucy Parker
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 Verification Status of Time Protection and Microkit-based OS Services
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 Ihor Kuz/Nick Spinale
14:00 - 15:00 Plenary BoFs
Break
15:30 - 16:30 Plenary BoFs Ihor Kuz/Nick Spinale
16:30 - 16:45 Plenary Report from BoFs + Discussion
16:45 - 17:00 Concluding remarks
Day 4 18 October 2024 Training day @ UNSW 
10:00 - 12:30 Training Using LionsOS
Ivan Velickovic, UNSW Sydney
14:00 - 16:30 Training Using Rust in seL4 Userspace
Nick Spinale, Colias Group, LLC