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, 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 | Enhancing seL4’s C/C++ userspace memory safety using CHERI Hesham Almatary, Capabilities Limited |
|
|
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 | seL4 Anniversary Panel Session
Moderated by Nick Spinale, Colias Group, LLC |
|
|
Nick Spinale |
| Break | |||||
| 10:30 - 11:00 | Talk | First steps towards verification of user-space systems Matthew Brecknell, Kry10 |
|
|
Darren Cofer |
| 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 | Announcements June Andronick, seL4 Foundation |
|
||
| Break | |||||
| 10:30 - 11: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 |
|
|
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 | |||