seL4 Summit 2024: Full Schedule

09:00 AEDT

Welcome

Tuesday October 15, 2024 09:00 - 09:10 AEDT

Banksia + Bluegum

Tuesday October 15, 2024 09:00 - 09:10 AEDT
Banksia + Bluegum

General Sessions

09:10 AEDT

Industrial Scale Proof Engineering for Critical Trustworthy Applications (INSPECTA)

Tuesday October 15, 2024 09:10 - 10:00 AEDT

Banksia + Bluegum

Formal methods have been successfully deployed at scale in production environments at large internet companies, but barriers remain to their adoption by defense companies developing national security systems. The goal of the INSPECTA project (part of the DARPA PROVERS program which has just started in 2024) is to improve the security of defense and aerospace systems by dramatically improving the usability, flexibility, and accessibility of formal methods-based development and verification tools. We
will leverage memory-safe programming languages (Rust), a provably secure microkernel (seL4), and new formal methods tools and make them accessible to the defense industry workforce. These open source technologies will be integrated into an aerospace CertDevOps workflow automation processes and applied to the development of mission critical systems to demonstrate their usability, practicality, and effectiveness. We will demonstrate the tools and workflow by addressing emerging security requirements for the Air Launched Effects (ALE) mission computing platform. This will include rearchitecting the mission software as a collection of virtual machines running legacy code and selected high-criticality components, producing an architecture model for the system, porting selected software to Rust, building software to run on seL4, and verifying critical safety and security properties. This presentation will provide an overview of the PROVERS program objectives, the INSPECTA workflow to be developed, and the assurance evidence to be produced.

Speakers

Darren Cofer

Fellow, Collins Aerospace

Darren Cofer is a Principal Fellow at Collins Aerospace. He earned his PhD in Electrical and Computer Engineering from The University of Texas at Austin. His area of expertise is developing and applying advanced analysis methods and tools for verification and certification of high-assurance... Read More →

Tuesday October 15, 2024 09:10 - 10:00 AEDT
Banksia + Bluegum

Keynote Sessions

10:00 AEDT

Break

Tuesday October 15, 2024 10:00 - 10:30 AEDT

Bluegum Lobby

Tuesday October 15, 2024 10:00 - 10:30 AEDT
Bluegum Lobby

Activities / Breaks / Special Events

10:30 AEDT

seL4 Verification: Status and Plans

Tuesday October 15, 2024 10:30 - 11:00 AEDT

Banksia + Bluegum

Speakers

Gerwin Klein

Proofcraft

June Andronick

Proofcraft

Corey Lewis

Proofcraft

Michael McInerney

Proofcraft

Rafal Kolanski

Proofcraft

Tuesday October 15, 2024 10:30 - 11:00 AEDT
Banksia + Bluegum

Presentations Sessions

11:00 AEDT

seL4 Multikernel Roadmap and Concurrency Verification

Tuesday October 15, 2024 11:00 - 11:30 AEDT

Banksia + Bluegum

Speakers

Gerwin Klein

Proofcraft

Corey Lewis

Proofcraft

Tuesday October 15, 2024 11:00 - 11:30 AEDT
Banksia + Bluegum

Presentations Sessions

11:30 AEDT

The Neutrality Atoll Hypervisor and the seL4 Multikernel

Tuesday October 15, 2024 11:30 - 12:00 AEDT

Banksia + Bluegum

Speakers

David Cock

Neutrality

Mathieu Mirmont

Neutrality

Stevens Le Blond

Neutrality

Tuesday October 15, 2024 11:30 - 12:00 AEDT
Banksia + Bluegum

Presentations Sessions

12:00 AEDT

Lunch

Tuesday October 15, 2024 12:00 - 13:30 AEDT

Jacaranda Terrace

Tuesday October 15, 2024 12:00 - 13:30 AEDT
Jacaranda Terrace

Activities / Breaks / Special Events

13:30 AEDT

Lions OS: Secure, Fast, Adaptable!

Tuesday October 15, 2024 13:30 - 13:45 AEDT

Banksia + Bluegum

Speakers

Gernot Heiser

Trustworthy Systems, UNSW

Tuesday October 15, 2024 13:30 - 13:45 AEDT
Banksia + Bluegum

Presentations Sessions

13:45 AEDT

In and Around LionsOS

Tuesday October 15, 2024 13:45 - 14:15 AEDT

Banksia + Bluegum

Speakers

Ivan Velickovic

Trustworthy Systems

Tuesday October 15, 2024 13:45 - 14:15 AEDT
Banksia + Bluegum

Presentations Sessions

14:15 AEDT

The Secure Multiserver Operating System Framework

Tuesday October 15, 2024 14:15 - 14:30 AEDT

Banksia + Bluegum

Speakers

Alwin Joshy

Trustworthy Systems

Gernot Heiser

Trustworthy Systems, UNSW

Craig McLaughlin

Trustworthy Systems/UNSW Sydney

Kevin Elphinstone

Trustworthy Systems/UNSW Sydney

Tuesday October 15, 2024 14:15 - 14:30 AEDT
Banksia + Bluegum

Presentations Sessions

14:30 AEDT

Running Certified Operating Systems under the seL4 Hypervisor

Tuesday October 15, 2024 14:30 - 15:00 AEDT

Banksia + Bluegum

Speakers

Chris Guikema

DornerWorks

Tuesday October 15, 2024 14:30 - 15:00 AEDT
Banksia + Bluegum

Presentations Sessions

15:00 AEDT

Break

Tuesday October 15, 2024 15:00 - 15:30 AEDT

Bluegum Lobby

Tuesday October 15, 2024 15:00 - 15:30 AEDT
Bluegum Lobby

Activities / Breaks / Special Events

15:30 AEDT

Securing ROS Systems with seL4

Tuesday October 15, 2024 15:30 - 16:00 AEDT

Banksia + Bluegum

Speakers

Alex Pavey

DornerWorks

Nathan Studer

DornerWorks

Cristian Balas

US Army - Ground Vehicle Robotics

Yale Empie

US Army - Ground Vehicle Robotics

Zach Clark

DornerWorks

Tuesday October 15, 2024 15:30 - 16:00 AEDT
Banksia + Bluegum

Presentations Sessions

16:00 AEDT

Experience Developing Code for the seL4 Environment

Tuesday October 15, 2024 16:00 - 16:15 AEDT

Banksia + Bluegum

Speakers

Alain Kägi

Assistant Professor, Lewis & Clark College

Wyeth Greenlaw Rollins

Student, Lewis & Clark College

Caitlyn Wilde

Student, Lewis & Clark College

I'm a senior at Lewis and Clark College in Oregon studying computer science with a focus in cybersecurity.

Tuesday October 15, 2024 16:00 - 16:15 AEDT
Banksia + Bluegum

Presentations Sessions

16:15 AEDT

Transitioning from CAmkES VMM to MicroKit VMM

Tuesday October 15, 2024 16:15 - 16:30 AEDT

Banksia + Bluegum

Speakers

Leigha VanderKlok

DornerWorks

Tuesday October 15, 2024 16:15 - 16:30 AEDT
Banksia + Bluegum

Presentations Sessions

16:45 AEDT

seL4 on RISC-V:Building Safe and Fast Firmware

Tuesday October 15, 2024 16:45 - 17:00 AEDT

Banksia + Bluegum

Speakers

lei mao

Director, horizon robotics

Tuesday October 15, 2024 16:45 - 17:00 AEDT
Banksia + Bluegum

Presentations Sessions

17:00 AEDT

Networking Event

Tuesday October 15, 2024 17:00 - 18:30 AEDT

TBA

Tuesday October 15, 2024 17:00 - 18:30 AEDT
TBA

Activities / Breaks / Special Events

09:00 AEDT

Panel Discussion

Wednesday October 16, 2024 09:00 - 09:50 AEDT

Banksia + Bluegum

Wednesday October 16, 2024 09:00 - 09:50 AEDT
Banksia + Bluegum

Panel Discussions & Birds of a Feather

09:50 AEDT

sel4 Foundation Update

Wednesday October 16, 2024 09:50 - 10:00 AEDT

Banksia + Bluegum

Wednesday October 16, 2024 09:50 - 10:00 AEDT
Banksia + Bluegum

General Sessions

10:00 AEDT

Break

Wednesday October 16, 2024 10:00 - 10:30 AEDT

Bluegum Lobby

Wednesday October 16, 2024 10:00 - 10:30 AEDT
Bluegum Lobby

Activities / Breaks / Special Events

10:30 AEDT

First Steps Towards Verification of User-Space Systems

Wednesday October 16, 2024 10:30 - 11:00 AEDT

Banksia + Bluegum

Speakers

Matthew Brecknell

Verification Engineer, Kry10

Matthew is a formal verification practitioner. He has made significant contributions to the seL4 verification story, and is a member of the seL4 Foundation Technical Steering Committee. At Kry10, Matthew is developing the next generation of high-assurance remotely-managed seL4-based... Read More →

Wednesday October 16, 2024 10:30 - 11:00 AEDT
Banksia + Bluegum

Presentations Sessions

11:00 AEDT

Generating Trustworthy Hardware/Software I2C Drivers for Board Management Controllers

Wednesday October 16, 2024 11:00 - 11:30 AEDT

Banksia + Bluegum

Speakers

Daniel Schwyn

PhD Student, ETH Zurich

Timothy Roscoe

Professor, ETH Zurich

Zikai Liu

ETH Zurich

Wednesday October 16, 2024 11:00 - 11:30 AEDT
Banksia + Bluegum

Presentations Sessions

11:30 AEDT

Using Model Checking to Develop and Verify Inter-Component Signalling Protocols

Wednesday October 16, 2024 11:30 - 11:45 AEDT

Banksia + Bluegum

Speakers

Courtney Darville

UNSW

Wednesday October 16, 2024 11:30 - 11:45 AEDT
Banksia + Bluegum

Presentations Sessions

11:45 AEDT

Rust Support in seL4 Userspace: Overview and Update

Wednesday October 16, 2024 11:45 - 12:00 AEDT

Banksia + Bluegum

Speakers

Nick Spinale

Colias Group LLC

Wednesday October 16, 2024 11:45 - 12:00 AEDT
Banksia + Bluegum

Presentations Sessions

12:00 AEDT

Pancake: A Language for Verified Systems Programming

Wednesday October 16, 2024 12:00 - 12:15 AEDT

Banksia + Bluegum

Speakers

Miki Tanaka

UNSW Sydney

Gernot Heiser

Trustworthy Systems, UNSW

Johannes Åman Pohjola

UNSW Sydney

Wednesday October 16, 2024 12:00 - 12:15 AEDT
Banksia + Bluegum

Presentations Sessions

12:15 AEDT

Lunch

Wednesday October 16, 2024 12:15 - 13:45 AEDT

Jacaranda Terrace

Wednesday October 16, 2024 12:15 - 13:45 AEDT
Jacaranda Terrace

Activities / Breaks / Special Events

13:45 AEDT

Assured Reserve Modes

Wednesday October 16, 2024 13:45 - 14:15 AEDT

Banksia + Bluegum

Speakers

Ihor Kuz

Principal Engineer, Kry10

Dr Ihor Kuz is an operating system engineer at Kry10, helping develop the Kry10 OS and Platform. Ihor has previous experience leading the team developing the seL4 microkernel, and has been involved with seL4 for as long as it’s been around. Ihor is a member of the seL4 Foundation's... Read More →

Lance Joneckis

Idaho National Laboratory

Wednesday October 16, 2024 13:45 - 14:15 AEDT
Banksia + Bluegum

Presentations Sessions

14:15 AEDT

Assured Reserve Modes in Action

Wednesday October 16, 2024 14:15 - 14:30 AEDT

Banksia + Bluegum

Speakers

Ihor Kuz

Principal Engineer, Kry10

Lance Joneckis

Idaho National Laboratory

Wednesday October 16, 2024 14:15 - 14:30 AEDT
Banksia + Bluegum

Presentations Sessions

14:30 AEDT

Supporting Container Applications on an seL4-based OS (Kry10 OS)

Wednesday October 16, 2024 14:30 - 14:45 AEDT

Banksia + Bluegum

Speakers

Alison Felizzi

Kry10

Wednesday October 16, 2024 14:30 - 14:45 AEDT
Banksia + Bluegum

Presentations Sessions

14:45 AEDT

Exploring an seL4-based Trusted Execution Environment in a RISC-V Platform

Wednesday October 16, 2024 14:45 - 15:00 AEDT

Banksia + Bluegum

Speakers

Everton de Matos

Technology Innovation Institute

Wednesday October 16, 2024 14:45 - 15:00 AEDT
Banksia + Bluegum

Presentations Sessions

15:00 AEDT

Break

Wednesday October 16, 2024 15:00 - 15:30 AEDT

Bluegum Lobby

Wednesday October 16, 2024 15:00 - 15:30 AEDT
Bluegum Lobby

Activities / Breaks / Special Events

15:30 AEDT

Bridging Academia and Industry

Wednesday October 16, 2024 15:30 - 16:00 AEDT

Banksia + Bluegum

Speakers

Yanyan Shen

NIO

Dhammika Elkaduwe

NIO

Wednesday October 16, 2024 15:30 - 16:00 AEDT
Banksia + Bluegum

Presentations Sessions

16:00 AEDT

seL4 Infrastructure: USB and Beyond

Wednesday October 16, 2024 16:00 - 16:30 AEDT

Banksia + Bluegum

Speakers

Bill Ellis

Software Engineer, Capgemini

Wednesday October 16, 2024 16:00 - 16:30 AEDT
Banksia + Bluegum

Presentations Sessions

16:30 AEDT

Building a Commercial Virtualized Mobile Device with seL4 – Part 3

Wednesday October 16, 2024 16:30 - 16:45 AEDT

Banksia + Bluegum

Speakers

Jason Sebranek

Cog Systems Inc

Wednesday October 16, 2024 16:30 - 16:45 AEDT
Banksia + Bluegum

Presentations Sessions

16:45 AEDT

Doing Nix for seL4: Towards more Infrastructure-as-Code

Wednesday October 16, 2024 16:45 - 17:00 AEDT

Banksia + Bluegum

Speakers

Wanja Zaeske

Deutsches Zentrum für Luft- und Raumfahrt (DLR)

Wednesday October 16, 2024 16:45 - 17:00 AEDT
Banksia + Bluegum

Presentations Sessions

18:00 AEDT

Dinner

Wednesday October 16, 2024 18:00 - 20:00 AEDT

TBA

Wednesday October 16, 2024 18:00 - 20:00 AEDT
TBA

Activities / Breaks / Special Events

09:00 AEDT

seL4 in Software-Defined Vehicles: Vision, Roadmap, and Impact at NIO

Thursday October 17, 2024 09:00 - 09:50 AEDT

Banksia + Bluegum

The automotive industry is rapidly evolving, with software-defined vehicles (SDVs) at the forefront of this transformation. At NIO, we are leveraging the seL4 microkernel to redefine vehicle architecture, ensuring robust safety, reliability, and performance. This presentation will explore the vision behind integrating seL4 into our SDV platform. We will share the journey of delivering the seL4-based SkyOS-M within the ONVO vehicle on our latest NT3 platform, highlight the significant impact this integration has had on our vehicle design and functionality, and outline our future roadmap beyond the current launch.

Speakers