Dear PC of the seL4 Summit 2023! We are thrilled that you accepted the invitation! Please find below [0] our awesome team, from various parts of the seL4 ecosystem. To get started, we have 2 small tasks for you: 1- Website: we aim to announce the PC next week, so please check, by Friday 10 Feb, that you are fine with your name/affiliation/link as below [0]. If we don't hear back from you, we'll assume it's all good and we'll go ahead with the announcement. For the people that were on the PC last year, we'll use the same picture as last year. If you prefer a different one, please send it to Birg and I by Friday as well. 2- Themes/topics for the Call for Presentations: we suggest we keep the same topics as last year [1], as they are still good and relevant. But your thoughts/suggestions are welcome. Please send them by Tuesday 14 Feb. If we don't hear back from you, we'll assume you're fine with reusing the same topics and we'll aim to publish the CfP around Wednesday 15th Feb. Your next task (hopefully next week) will be to help advertise for the CfP, encourage submissions, nudge specific people you'd like to hear about etc. Remember: we aim to maximise the take away value. So you should think of it as: what would an ideal seL4 summit look like for you? What is the cool seL4 work that you heard about and would love to hear more about? The Call For Presentation is lightweight and informal. The aim is to attract the work we want to hear about or want the community to hear about. I’m just adding a 3rd tiny task: 0- if you don’t need to reply to 1 and 2 above because you happen to be fine with the default, can you please still send Birg and I an “ACK” email so we know we got the mailing list right? :) If you have any questions, let us know. Thanks again, Birg, June, Darren & Ihor [0] PC of the seL4 Summit 2023: - Darren Cofer (Raytheon), co-chair, http://loonwerks.com/people/darren-cofer.html - Ihor Kuz (Kry10), co-chair, http://www.ikuz.org/ - Perry Alexander (U of Kansas), https://perry.alexander.name - June Andronick (Proofcraft), https://proofcraft.systems/#june - Todd Carpenter (Adventium Labs), https://www.adventiumlabs.com/team-member/todd-carpenter - Martin D2 (NCSC), https://www.ncsc.gov.uk - Alison Felizzi (Kry10) - Axel Heider (Hensoldt Cyber), https://www.linkedin.com/in/axelheider/ - Gernot Heiser (UNSW), https://trustworthy.systems/people/?cn=Gernot+Heiser - Lucy Parker (UNSW), https://trustworthy.systems/people/?cn=Lucy+Parker - Nick Spinale (Colias Group), https://nickspinale.com - Robbie VanVossen (Dornerworks), https://www.linkedin.com/in/robbie-vanvossen-gr/ [1] Themes for the seL4 summit’22 CfP: - 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