seL4 summit logo

Call For Presentations for the seL4 Summit 2024

Important Dates:

  • Abstracts due: 22 April 2024
  • Notification of decisions: 7 June 2024
  • Summit: 15-17 October 2024

Overview

The seL4 summit aims at gathering the seL4 community to learn, share, and connect:

  • learn about the seL4 technology, its latest progress, use, successes, challenges, plans;
  • share exciting seL4 development, research, experience, application in the real world;
  • connect with other seL4 developers, users, providers, supporters, potential partners, and enthusiasts.

The seL4 summit covers the complete seL4 ecosystem, consisting of the verified microkernel, as well as all seL4-related technology, tools, infrastructure, products, projects, and people.

The seL4 summit 2024 will be in Sydney, Australia.

Topics

We solicit proposals on any seL4-related topic, in particular in the areas of:

  • seL4 on-going and planned R&D, mature or early stage:
    • seL4 research efforts
    • seL4 development efforts
    • work-in-progress seL4 development
    • student work on seL4
    • new/missing/next-gen kernel mechanisms
    • seL4-related roadmaps: what you plan to work on and when
    • seL4 grand challenges
    • OS frameworks and services
    • seL4 userland with programming language support beyond C
    • High performance systems based on seL4: pushing the boundaries
  • seL4 experience reports
    • experience with deploying seL4 in the field, in commercial/deployed products
    • experience with teaching seL4
    • experience with seL4 in certification schemes and application of industry standards
    • experience with “building a business case for using a verified kernel”
    • experience with porting software from other OSes
  • seL4 and hardware
    • ports to new hardware platforms or architectures
    • multicore systems
    • virtualisation
    • new/proposed hardware features or architectures, which could also enable or broaden the scope of formal reasoning (e.g. about time protection)
    • seL4 in embedded processors on FPGAs, and impact of assured separation
    • IOMMU solutions for various hardware architectures and impact for seL4
  • seL4 and assurance:
    • application-level verification leveraging seL4 proofs
    • correctness, spatial separation, temporal separation, and real-time proofs
    • formalised interface between or composition of kernel-level proofs and user-level proofs
    • verification engineering at scale, scaling verification productivity
    • security/safety impact/assurance/certification for an seL4-based system

Submission

If you would like to propose a talk, please upload an abstract of one page or less for your proposed talk by 22 April 2024 on the submission portal. Abstracts should indicate why the talk fits in the seL4 summit scope. Notifications of accepted presentations will be made by 7 June 2024.

If you'd love to hear about some specific work from other people in the community, we encourage you to reach out to them to incite them to submit a proposal. :-) Alternatively, let us know at summit@sel4.systems.

Open invitation for a 5-minute slot to talk about your seL4 deployment

The community loves to hear about the deployment of seL4. So, if you:

  1. are selling an end-user product that has seL4 embedded within, or
  2. have integrated an seL4-based system/component into a deployed system,

you are welcome to a 5-min slot at the summit to talk about it, regardless of whether you are submitting an abstract for a full presentation! Simply send a short description by email to summit@sel4.systems by 22 April 2024.

Contact

If you have questions, please do not hesitate to contact the seL4 Foundation summit team at: summit@sel4.systems.