seL4 Summit 2022
Munich, Germany (hybrid)
10-13 Oct 2022
Program
All times are local time in Munich, Germany (UTC+2).
| Day 1 10 October 2022 | |||||
|---|---|---|---|---|---|
| Session chair | |||||
| 9:00 - 9:10 | Announcements | Welcome |  |
 |
Darren Cofer & June Andronick |
| 9:10 - 10:00 | Keynote | State of seL4-related research Gernot Heiser, UNSW |
|
|
Darren Cofer |
| Break | |||||
| 10:15 - 10:45 | Talk | seL4 verification roadmap Rafal Kolanski, Gerwin Klein & June Andronick, Proofcraft |
|
|
Nick Spinale |
| 10:45 - 11:15 | Talk | Explaining the seL4 integrity theorems Matt Brecknell, Kry10 |
|
|
|
| 11:15 - 11:45 | Discussion | AMA (Ask Me Anything) with the Foundation TSC | |
Darren Cofer | |
| Break | |||||
| 12:45 - 13:15 | Talk | The seL4 Core
Platform (seL4CP) Zoltan Kocsis, UNSW |
|
|
Robbie VanVossen |
| 13:15 - 13:45 | Talk | The seL4 Device Driver Framework (sDDF) Lucy Parker, UNSW |
|
|
|
| 13:45 - 14:30 | Talk & Discussion | Multiprocessing on seL4 with verified kernels Kent McLeod, Kry10 |
|
|
|
| Break | |||||
| 15:00 - 15:30 | Talk | Using QEMU to extend seL4 VirtIO support Hannu Lyytinen & Markku Ahvenjärvi, TII |
|
|
Ihor Kuz |
| 15:30 - 16:00 | Talk | QEMU as prototyping platform for seL4 systems Axel Heider, HENSOLDT Cyber |
|
|
|
| 16:00 - 16:30 | Talk | Porting U-Boot drivers to seL4 Mark Jenkinson & Stephen Williams, Capgemini |
|
|
|
| 16:30 - 17:00 | Talk | fence.t: hardware support for preventing microarchitectural timing channels Nils Wistoff, ETH |
|
|
|
| Traditional Bavarian Dinner 19:00 - 22:30 | |||||
| Day 2 11 October 2022 | |||||
| Session chair | |||||
| 9:00 - 9:50 | Keynote | Kry10 Secure Platform Boyd Multerer, Kry10 |
|
|
June Andronick |
| 9:50 - 10:00 | Announcements | Foundation announcements | |
|
June Andronick & Darren Cofer |
| Break | |||||
| 10:15 - 10:45 | Talk | seL4 and BEAM: a match made in Erlang Ihor Kuz, Kry10 |
|
|
Gerwin Klein |
| 10:45 - 11:15 | Talk | Trustworthy board management controllers Daniel Schwyn, Ben Fiedler, Michael Giardino, David Cock & Timothy Roscoe, ETH |
|
|
|
| 11:15 - 11:45 | Talk & Discussion | Rust support in seL4 userspace: present and future Nick Spinale |
|
|
|
| Break | |||||
| 12:45 - 13:15 | Talk | Early experiences proving the correctness of a network stack implementation Alain Kägi, Aubrey Birdwell, Caitlyn Wilde, Jens Mache & Richard Weiss, Lewis & Clark College |
|
|
Rafal Kolanski |
| 13:15 - 13:45 | Talk | CASE overview: Cyber Assured Systems Engineering Darren Cofer, Collins Aerospace |
|
|
|
| 13:45 - 14:15 | Talk | A verified architecture for trustworthy remote attestation Grant Jurgensen, The University of Kansas |
|
||
| Break | |||||
| 14:45 - 15:05 | Experience report | FerrOS: Rust-y unikernels on seL4 w/ compile-time assurances Zack Pierce, Auxon |
|
|
Kent McLeod |
| 15:05 - 15:25 | Experience report | Make seL4 an ASIL-D certified system Yuning Liang, Xcalibyte |
|
|
|
| 15:25 - 15:45 | Experience report | seL4 Summit and TCCOE - an overview
Renato Levy, Jason Li & Ray Richards, TCCOE |
|
|
|
| 15:45 - 17:00 | Panel & Discussion | Funding agencies: priorities and vision
William “Brad” Martin, DARPA Paul Waller, NCSC Sebastian Jester, Cyberagentur Dr. Shreekant (Ticky) Thakkar, TII |
|
|
Gernot Heiser |
| Day 3 12 October 2022 | |||||
| Session chair | |||||
| 9:00 - 9:45 | Plenary | Overview: seL4 principles, abstractions and use Gernot Heiser, seL4 Foundation |
|
|
Matt Brecknell |
| 9:45 - 10:00 | Plenary | Overview: what's verified, what's not, and what does it mean? June Andronick, seL4 Foundation |
|
|
|
| 10:00 - 10:45 | Plenary | The seL4 GitHub test suite Gerwin Klein, Proofcraft |
|
|
|
| Break | |||||
| 11:00 - 11:15 | Announcements | Discussion teaser and suggestions for Birds of a Feather | Anna Lyons | ||
| 11:15 - 12:00 | Room 1: Talk & Discussion |
seL4 mainlining: experiences, challenges, and solutions Robbie VanVossen & Chris Guikema, DornerWorks |
|
|
Anna Lyons |
| Room 2: BoF |
Birds of a Feather on a topic to be suggested | ||||
| Break | |||||
| 12:45 - 13:30 | Room 1: Talk & Discussion |
seL4 microkernel for virtualization use-cases “The importance of a standard VMM” Everton de Matos & Jason Sebranek, TII+Cog |
|
|
Room 1: Axel Heider Room 2: self-organised |
| Room 2: BoF |
Birds of a Feather on a topic to be suggested | ||||
| 13:30 - 14:15 | Room 1: Talk & Discussion |
Improving embedded DevOps with seL4 VMM Robbie VanVossen, DornerWorks |
|
|
|
| Room 2: BoF |
Birds of a Feather on a topic to be suggested | ||||
| 14:15 - 15:00 | Room 1: Talk & Discussion |
Experience teaching seL4 Sebastian Eckl, HENSOLDT Cyber |
|
|
|
| Room 2: BoF |
Birds of a Feather on a topic to be suggested | ||||
| Break | |||||
| 15:15 - 16:00 | Plenary | BoFs report back | Gernot Heiser | ||
| 16:00 - 16:15 | Announcements | Bootcamp overview | Gernot Heiser | ||
| 16:15 - 16:30 | Teaser | DornerWorks’ VM Composer Robbie VanVossen, DornerWorks |
|
|
Gernot Heiser |
| 16:30 - 16:45 | Plenary | seL4 Foundation: overview, update and vision June Andronick, seL4 Foundation |
|
|
|
| 16:45 - 17:00 | Announcements | Concluding remarks | |
Darren Cofer, June Andronick & Gernot Heiser |
|
| Day 4 (Bootcamp, on-site participants only) 13 October 2022 | |||||
| 9:00 - 10:00 | Bootcamp | seL4: from zero to hello world Ihor Kuz, Kry10 |
Axel Heider | ||
| Break | |||||
| 10:15 - 10:45 | Bootcamp | CAmkES Sebastian Eckl, HENSOLDT Cyber |
Axel Heider | ||
| 10:45 - 12:00 | Bootcamp | TRENTOS Sebastian Eckl, HENSOLDT Cyber |
Axel Heider | ||
| Break | |||||
| 13:00 - 14:30 | Bootcamp | The seL4 Core Platform (seL4CP) Ivan Velickovic & Peter Chubb, UNSW |
Axel Heider | ||
| 14:30 - 15:15 | Bootcamp | DornerWorks’ VM Composer: the easy button for virtualized seL4-based systems Chris Guikema & Robbie VanVossen, Dornerworks |
Axel Heider | ||
| Break | |||||
| 15:30 - 17:00 | Bootcamp | BriefCASE tutorial Isaac Amundson & Darren Cofer, Collins Aerospace |
Axel Heider | ||
| 17:00 - 17:05 | Plenary | Concluding remarks | June Andronick & Darren Cofer |
||
Acknowledgement:
Slide icons create by Syahrul Hidayatullah - Flaticon