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