BEGIN:VCALENDAR
VERSION:2.0
X-WR-CALNAME:sel4summit2026
X-WR-CALDESC:Event Calendar
METHOD:PUBLISH
CALSCALE:GREGORIAN
PRODID:-//Sched.com seL4 Summit 2026//EN
X-WR-TIMEZONE:UTC
BEGIN:VEVENT
DTSTAMP:20260629T203449Z
DTSTART:20260901T150000Z
DTEND:20260902T000000Z
SUMMARY:Registration & Badge Pick-up
DESCRIPTION:\n
CATEGORIES:REGISTRATION / BREAKS / SPECIAL EVENTS
LOCATION:Georgia Ballroom Foyer\, Vancouver\, BC\, Canada
SEQUENCE:0
UID:48bd7459d43e92abf3d009b1fe9054a4
URL:http://sel4summit2026.sched.com/event/48bd7459d43e92abf3d009b1fe9054a4
END:VEVENT
BEGIN:VEVENT
DTSTAMP:20260629T203449Z
DTSTART:20260901T160000Z
DTEND:20260901T161000Z
SUMMARY:Welcome
DESCRIPTION:\n
CATEGORIES:GENERAL SESSION
LOCATION:Georgia Ballroom B\, Vancouver\, BC\, Canada
SEQUENCE:0
UID:a7e5e77c02dcfe441a64192151b59056
URL:http://sel4summit2026.sched.com/event/a7e5e77c02dcfe441a64192151b59056
END:VEVENT
BEGIN:VEVENT
DTSTAMP:20260629T203449Z
DTSTART:20260901T161000Z
DTEND:20260901T170000Z
SUMMARY:Keynote: The Age of Software Understanding - Anjana Rajan\, CEO & Co-Founder\, Atalanta
DESCRIPTION:The emergence of formally verified building blocks across the stack\, from memory-safe languages to verified microkernels like seL4\, represents a hard-won foundation. But it raises a deeper challenge: local correctness does not translate to system reliability. Each component may behave exactly as proven\, while the system as a whole remains unpredictable.\n\nThis talk introduces Software Understanding as a new discipline: the science of formally verifying that software-controlled systems perform correctly across normal\, abnormal\, and hostile conditions\, and making that reasoning legible across the teams responsible for them. As critical infrastructure becomes increasingly autonomous and AI-driven\, the gap between what we build and what we can reason about continues to widen. Closing that gap requires more than proof\; it requires bringing mathematical rigor into the pace and complexity of real-world operations.\n\nDrawing on lessons from national security and mission-critical systems\, this talk examines what it will take to move formal methods from technical scripture to organizational discipline\, and why verified microkernels like seL4 are not the end of the story\, but the beginning.
CATEGORIES:KEYNOTE SESSIONS
LOCATION:Georgia Ballroom B\, Vancouver\, BC\, Canada
SEQUENCE:0
UID:074cab940596d6b802f4b0e2298d199d
URL:http://sel4summit2026.sched.com/event/074cab940596d6b802f4b0e2298d199d
END:VEVENT
BEGIN:VEVENT
DTSTAMP:20260629T203449Z
DTSTART:20260901T170000Z
DTEND:20260901T173000Z
SUMMARY:Break
DESCRIPTION:\n
CATEGORIES:REGISTRATION / BREAKS / SPECIAL EVENTS
LOCATION:Georgia A\, Vancouver\, BC\, Canada
SEQUENCE:0
UID:b62fe5628c90c4da76b27c04422649c9
URL:http://sel4summit2026.sched.com/event/b62fe5628c90c4da76b27c04422649c9
END:VEVENT
BEGIN:VEVENT
DTSTAMP:20260629T203449Z
DTSTART:20260901T173000Z
DTEND:20260901T183000Z
SUMMARY:seL4: What\, Why\, Who and Where? - June Andronick\, Proofcraft and seL4 Foundation
DESCRIPTION:This talk will provide an overview of the seL4 microkernel and its ecosystem\, as an introduction to anyone new to the community and to the seL4 summit\, and as a refresher and update to existing players. The aim is that everyone is set to follow the rest of the event and contribute to discussions.&nbsp\;\nThe talk will cover what seL4 is\, why its formal verification and security properties make it a key platform for high-assurance systems\, who is using and contributing to it across industry\, academia\, and government\, and where it is being applied today. It will provide pointers to who to connect with and where to learn more.\n
CATEGORIES:GENERAL SESSION
LOCATION:Georgia Ballroom B\, Vancouver\, BC\, Canada
SEQUENCE:0
UID:e6bb6504a6ea09ac6ff493d0198deb10
URL:http://sel4summit2026.sched.com/event/e6bb6504a6ea09ac6ff493d0198deb10
END:VEVENT
BEGIN:VEVENT
DTSTAMP:20260629T203449Z
DTSTART:20260901T183000Z
DTEND:20260901T190000Z
SUMMARY:10 Years of seL4 at NCSC - Adam\, NCSC
DESCRIPTION:The UK’s National Cyber Security Centre first started looking at seL4 and its formal security guarantees in 2016. Over the last ten years\, we have worked on numerous projects with the goal of using seL4 to help us in our mission to make the UK the safest place to live and work online. We will talk about our early efforts understanding seL4’s security guarantees and how they map onto our assurance processes for security systems. From those early investigations\, we will talk about how we view emerging technologies and how these considerations led us to invest in the seL4 ecosystem. Focussing on real world deployments of seL4\, we’ll lift the curtain on several projects we’ve been working on over the last few years building products and systems based on seL4.\n\nThe aim for this talk will be to provide insight and feedback on the process of seL4 adoption\, including views from industry on the design and deployment of real world products based on the technology. Finally we will talk about where we think seL4 based components fit in the landscape of secure system design and speculation on what the future might hold for seL4 and the NCSC.\n
CATEGORIES:GENERAL SESSION
LOCATION:Georgia Ballroom B\, Vancouver\, BC\, Canada
SEQUENCE:0
UID:7175c7273262bf4fcbca0847b438128b
URL:http://sel4summit2026.sched.com/event/7175c7273262bf4fcbca0847b438128b
END:VEVENT
BEGIN:VEVENT
DTSTAMP:20260629T203449Z
DTSTART:20260901T190000Z
DTEND:20260901T203000Z
SUMMARY:Lunch
DESCRIPTION:\n
CATEGORIES:REGISTRATION / BREAKS / SPECIAL EVENTS
LOCATION:Georgia A\, Vancouver\, BC\, Canada
SEQUENCE:0
UID:56f9620586c561c81a860743d551d333
URL:http://sel4summit2026.sched.com/event/56f9620586c561c81a860743d551d333
END:VEVENT
BEGIN:VEVENT
DTSTAMP:20260629T203449Z
DTSTART:20260901T203000Z
DTEND:20260901T210000Z
SUMMARY:Talk Title To Be Announced - Alistair Woodman\, Erlang Ecosystem Foundation (EEF)
DESCRIPTION:\n
CATEGORIES:VOICES FROM NEARBY
LOCATION:Georgia Ballroom B\, Vancouver\, BC\, Canada
SEQUENCE:0
UID:c92c718dabcf1b258a81c572d143aa95
URL:http://sel4summit2026.sched.com/event/c92c718dabcf1b258a81c572d143aa95
END:VEVENT
BEGIN:VEVENT
DTSTAMP:20260629T203449Z
DTSTART:20260901T210000Z
DTEND:20260901T213000Z
SUMMARY:Trends in Formal Verification for Real-World Applications and Their Implications for the seL4 Ecosystem - David Hardin\, Collins Aerospace
DESCRIPTION:The formal methods community has made great progress in the past two decades to mature mathematically-precise techniques in order to tackle real-world design and analysis problems. &nbsp\;In areas as diverse as hardware design\, finance\, systems engineering\, software development\, and law\, increasingly the question is not\, “Why would you use formal methods?” but rather “Why wouldn’t you?” &nbsp\;With the assistance of powerful generative artificial intelligence agents\, the barriers to entry for the use of formal methods tools are falling fast -- even mathematicians are now using proof tools. &nbsp\;In this talk\, we will detail a number of leading-edge tools and techniques that are enabling formal methods to be successfully applied in a number of critical real-world domains. &nbsp\;We will also highlight the application of practical formal methods in a number of current government-sponsored Science and Technology initiatives\, such as DARPA's Resilient Software Systems effort. &nbsp\;We will also describe the Software Understanding initiative\, which combines the rigorous practice of constructing (forward understanding) and assessing (reverse understanding) software-controlled systems in order to verify their functionality\, safety\, security\, and reliability. &nbsp\;Finally\, we will reflect on the impact that these advances in real-world formal verification can have on the seL4 ecosystem.
CATEGORIES:VOICES FROM NEARBY
LOCATION:Georgia Ballroom B\, Vancouver\, BC\, Canada
SEQUENCE:0
UID:89d6dbe658a2fc935b1fd1adc08d8bed
URL:http://sel4summit2026.sched.com/event/89d6dbe658a2fc935b1fd1adc08d8bed
END:VEVENT
BEGIN:VEVENT
DTSTAMP:20260629T203449Z
DTSTART:20260901T213000Z
DTEND:20260901T220000Z
SUMMARY:Kry10 OS Software Safety Manual - Ihor Kuz\, Kry10
DESCRIPTION:As a step toward building safety certified systems on the seL4-based Kry10 OS (KOS) we have developed a Software Safety Manual for KOS. This safety manual provides procedures and guidelines for using KOS and its features to develop safety critical systems in such a way that they could be certified.\n\nIn general\, such systems consist of some core functionality (e.g. run a machine) and some safety-related functionality (e.g. stop the machine if a person is too near). The safety-related functionality is “safety critical”\, which means that the systems that implement it should be resistant to failure\, even in the presence of known and unknown hazards. Software safety certification is concerned with providing assurance that the risk of these safety-related systems failing has been reduced to an acceptable level.\n\nIn a KOS system much of that assurance can be gained from the isolation provided by KOS and the underlying\, formally verified\, seL4 microkernel. Additional assurance is gained from KOS features such as process supervision\, process start and restart\, process supervision and monitoring\, process resource management\, etc. Our safety manual walks through the process of creating a safety-related system and then ensuring that the safety functionality is itself safe. The steps for doing this are: 1) develop the core functionality\; 2) develop the safety-related functionality\; 3) protect the safety-related functionality from hazards including: memory corruption\, process corruption\, faulty inputs\, faulty outputs\, etc.\n\nIn this presentation we will discuss and describe this process\, illustrating with concrete examples how it can be applied to real working systems.
CATEGORIES:GENERAL SESSION
LOCATION:Georgia Ballroom B\, Vancouver\, BC\, Canada
SEQUENCE:0
UID:03443a73719c4c6e3ad1d2cc5955bb7c
URL:http://sel4summit2026.sched.com/event/03443a73719c4c6e3ad1d2cc5955bb7c
END:VEVENT
BEGIN:VEVENT
DTSTAMP:20260629T203449Z
DTSTART:20260901T220000Z
DTEND:20260901T223000Z
SUMMARY:Break
DESCRIPTION:\n
CATEGORIES:REGISTRATION / BREAKS / SPECIAL EVENTS
LOCATION:Georgia A\, Vancouver\, BC\, Canada
SEQUENCE:0
UID:8d49b42e35f83174127982ab4aabd8ea
URL:http://sel4summit2026.sched.com/event/8d49b42e35f83174127982ab4aabd8ea
END:VEVENT
BEGIN:VEVENT
DTSTAMP:20260629T203449Z
DTSTART:20260901T223000Z
DTEND:20260901T224500Z
SUMMARY:Navigating the Cyber Resilience Act: Real-World Lessons in Securing Connected Products - Jonathan Marshall\, SafeShark
DESCRIPTION:In an increasingly connected world\, cybersecurity is no longer just a technical feature\, it is a fundamental legal requirement for market access. The EU’s Cyber Resilience Act (CRA) is set to reshape how digital products are designed\, developed\, and maintained by introducing strict mandatory cybersecurity standards and incident reporting obligations for manufacturers. But beyond the dense regulatory text\, what does this actually mean for your business?\n\nDrawing on real-world testing and compliance experience at SafeShark\, this session cuts through the legal jargon to deliver a clear\, actionable overview of the CRA. We will explore the core requirements of the Act\, how it impacts the entire lifecycle of hardware and software products\, and the critical timelines you must meet ahead of the 2027 enforcement deadline. Whether you are a business leader\, product manager\, or developer\, you will leave with a pragmatic understanding of how to navigate these new rules\, avoid costly penalties\, and ensure your connected devices are secure\, compliant\, and ready for the European market.
CATEGORIES:GENERAL SESSION
LOCATION:Georgia Ballroom B\, Vancouver\, BC\, Canada
SEQUENCE:0
UID:e01d43c23e4a426b78bfaf9bda0e7d0b
URL:http://sel4summit2026.sched.com/event/e01d43c23e4a426b78bfaf9bda0e7d0b
END:VEVENT
BEGIN:VEVENT
DTSTAMP:20260629T203449Z
DTSTART:20260901T224500Z
DTEND:20260901T230000Z
SUMMARY:Formal Verification now in European Cyber Resiliency standard for OS - June Andronick\, Proofcraft and seL4 Foundation
DESCRIPTION:In this talk I will report on my contributions to add “Formal Verification” as a requirement to mitigate security risks in the new European Harmonised standards\, in the context of the Cyber Resilience Act (CRA). Namely\, I have submitted 3 contributions to the Operating System harmonised standard\, and all three contributions have now been accepted. The standard is still in the finalisation process\, but so far no changes have been requested on my contributions.\n\nThe Cyber Resilience Act (CRA) is a regulatory framework of the European Union (EU) for hardware and software products that are made available on the EU market. The CRAentered into force in December 2024 and will be fully applicable as of December 2027\, with some provisions starting to apply earlier. During that time\, the EU has commissioned European standardisation bodies (namely CEN\, CENELEC\, and ETSI) to define so-called “harmonised standards” for the CRA. Using a harmonised standard gives a “presumption of conformity”\, meaning any product that follows the standard will be assumed by the authorities to comply with the CRA’s legal requirements.\n\nFor the CRA\, the EU has requested the development of 41 harmonised standards\, split into horizontal standards (which apply across all products) and vertical standards (product-specific). One of the vertical standards being developed is specific to Operating Systems (standard number EN-304-626). Each standard defines a list of requirements\, and proposes a list of mitigations to address these requirements.\n\nBefore my contributions\, Formal Verification did not appear at all in the OS standard (and most other standards). This had 2 major implications. Firstly\, it meant that the standard was not pushing for what is today the demonstrated highest assurance for critical software\, with practical and effective impact. For seL4\, this meant that being formally verified would not differentiate it from other OSes with lower assurance\, when it comes to being compliant with EU regulations. Secondly\, it meant that the effort spent on formal verification would actually be penalised. Indeed\, a formally verified product\, to be compliant\, would still require additional effort to produce lower assurance evidence\, such as being checked for memory errors using a source code analysis tool\, or being implemented in a memory safe language.\n\nMy contributions consist of 3 new mitigations where Formal Verification shall be used to establish: (1) functional correctness\; (2) integrity\; and (3) confidentiality. With these additions to the OS standard\, the CRA will be more in-line with the state-of-the-art approach to cyber resiliency\, and seL4’s unique differentiator can continue to be a key advantage for a more secure software world.
CATEGORIES:GENERAL SESSION
LOCATION:Georgia Ballroom B\, Vancouver\, BC\, Canada
SEQUENCE:0
UID:b0c77f0d2670ce50a1a4fa42e375d185
URL:http://sel4summit2026.sched.com/event/b0c77f0d2670ce50a1a4fa42e375d185
END:VEVENT
BEGIN:VEVENT
DTSTAMP:20260629T203449Z
DTSTART:20260901T230000Z
DTEND:20260902T000000Z
SUMMARY:Panel Session & Speakers To Be Announced
DESCRIPTION:\n
CATEGORIES:GENERAL SESSION
LOCATION:Georgia Ballroom B\, Vancouver\, BC\, Canada
SEQUENCE:0
UID:b29fec3313372eae86d58a6139ed2cf9
URL:http://sel4summit2026.sched.com/event/b29fec3313372eae86d58a6139ed2cf9
END:VEVENT
BEGIN:VEVENT
DTSTAMP:20260629T203449Z
DTSTART:20260902T000000Z
DTEND:20260902T001000Z
SUMMARY:Closing Remarks
DESCRIPTION:\n
CATEGORIES:KEYNOTE SESSIONS
LOCATION:Georgia Ballroom B\, Vancouver\, BC\, Canada
SEQUENCE:0
UID:cfdc3f6a9d5dbea0253510691bd4657a
URL:http://sel4summit2026.sched.com/event/cfdc3f6a9d5dbea0253510691bd4657a
END:VEVENT
BEGIN:VEVENT
DTSTAMP:20260629T203449Z
DTSTART:20260902T013000Z
DTEND:20260902T033000Z
SUMMARY:Attendee Reception
DESCRIPTION:\n
CATEGORIES:REGISTRATION / BREAKS / SPECIAL EVENTS
LOCATION:TBA\, Vancouver\, BC\, Canada
SEQUENCE:0
UID:22c162a997049dba688e1e1288ddc247
URL:http://sel4summit2026.sched.com/event/22c162a997049dba688e1e1288ddc247
END:VEVENT
BEGIN:VEVENT
DTSTAMP:20260629T203449Z
DTSTART:20260902T150000Z
DTEND:20260903T000000Z
SUMMARY:Registration & Badge Pick-up
DESCRIPTION:\n
CATEGORIES:REGISTRATION / BREAKS / SPECIAL EVENTS
LOCATION:Georgia Ballroom Foyer\, Vancouver\, BC\, Canada
SEQUENCE:0
UID:c185289533c8d9bd40e64003ee65580b
URL:http://sel4summit2026.sched.com/event/c185289533c8d9bd40e64003ee65580b
END:VEVENT
BEGIN:VEVENT
DTSTAMP:20260629T203449Z
DTSTART:20260902T160000Z
DTEND:20260902T165000Z
SUMMARY:Keynote: From Proof to Product: Why Formal Methods Is Finally Ready - Martin Dehnel-Wild\, Chief Scientist\, Kry10
DESCRIPTION:For most of its history\, formal methods has been a discipline of proof rather than product: rigorous\, powerful\, and largely confined to academia. That is changing rapidly. I'll argue that FM is finally ready to deliver secure\, resilient systems in the real world\, and that the obstacles left are largely self-inflicted: a history of over-promising\, tools that are painful to use and barely interoperate\, and a habit of staying in the lab rather than supporting customers through real\, evolving deployments.\n\nDrawing on systems we're building today for a wide range of government and commercial partners\, I'll make the case that security is fundamentally an economic argument rather than a quest for perfection: the goal is to make attacking a system so costly that adversaries focus elsewhere. Reaching that at scale depends far less on stronger proofs than on ruthless attention to wider adoption: on meeting real customers in the messy\, changing environments they actually deploy into.\n\nRegardless of your views on AI\, it is rapidly lowering the barrier to entry. I'll show — not just tell — what becomes possible when modern AI is combined with formal tools and seL4. This is a talk for anyone who wants formal methods to matter beyond academia.
CATEGORIES:KEYNOTE SESSIONS
LOCATION:Georgia Ballroom B\, Vancouver\, BC\, Canada
SEQUENCE:0
UID:70551cf319578ff754f6c0f81635b2b5
URL:http://sel4summit2026.sched.com/event/70551cf319578ff754f6c0f81635b2b5
END:VEVENT
BEGIN:VEVENT
DTSTAMP:20260629T203449Z
DTSTART:20260902T165000Z
DTEND:20260902T170000Z
SUMMARY:Announcements - June Andronick\, Proofcraft & seL4 Foundation
DESCRIPTION:\n
CATEGORIES:KEYNOTE SESSIONS
LOCATION:Georgia Ballroom B\, Vancouver\, BC\, Canada
SEQUENCE:0
UID:647715ae72775c1f98a189e3305abd0a
URL:http://sel4summit2026.sched.com/event/647715ae72775c1f98a189e3305abd0a
END:VEVENT
BEGIN:VEVENT
DTSTAMP:20260629T203449Z
DTSTART:20260902T170000Z
DTEND:20260902T173000Z
SUMMARY:Break
DESCRIPTION:\n
CATEGORIES:REGISTRATION / BREAKS / SPECIAL EVENTS
LOCATION:Georgia A\, Vancouver\, BC\, Canada
SEQUENCE:0
UID:cf44c2a9f8d208d6b1282f7eae242317
URL:http://sel4summit2026.sched.com/event/cf44c2a9f8d208d6b1282f7eae242317
END:VEVENT
BEGIN:VEVENT
DTSTAMP:20260629T203449Z
DTSTART:20260902T173000Z
DTEND:20260902T180000Z
SUMMARY:Cyber-Hardened Satellite Software (CHSS) VMM - Robert VanVossen\, Dornerworks
DESCRIPTION:MIT Lincoln Laboratory and the Space Cyber-Resiliency group at Air Force Research Laboratory-Space Vehicles Directorate (AFRL/RV) have created a software platform called Cyber-Hardened Satellite Software (CHSS). “CHSS is a mission-agnostic spaceflight software platform whose functionality was inspired by NASA’s core Flight System but with an emphasis on cyber-resiliency. Most notably\, CHSS offers security without sacrificing performance.”1 CHSS utilizes Magnetite\, which is a secure OS built on top of the seL4 Microkernel. Magnetite and CHSS components are written in Rust\, which provides memory safety and type safety at the OS and application level. This stack provides a safe and secure foundation to create cyber-resilient satellite systems.\n\nAdoption of new technologies\, especially ones such as CHSS which are a paradigm shift in the way things have been done for satellites\, can be quite difficult. AFRL/RV recognized that adoption should be made incremental to have the fastest transition. DornerWorks is working on a Phase II SBIR from SPACEWERX that addresses this in 2 ways:\n\n1. Update VM Composer to target CHSS systems to make system configuration much simpler.\n\n2. Write a VMM in Rust for CHSS to allow a VM to host legacy software which can be incrementally ported to CHSS.\n\nVM Composer is a GUI tool for defining virtualized systems on top of seL4. By adding CHSS awareness to the tool\, the manual steps for system integrators and developers can be significantly reduced. VM Composer is a way to visualize a system and architect security appropriate for mission risk acceptance.\n\nThe VMM provides a way to run the entire legacy code in a sandbox. It can be adapted to communicate with the overall CHSS system and then each app that needs to be cyberhardened can be ported over to CHSS and removed from the VM\, one-by-one. Most importantly\, the developer has a fully functional system at each step\, allowing for incremental launches and deployments as the software is hardened. It also allows for lower criticality software to remain in the VM for deployment.\n\nThis talk will give further background on CHSS\, discuss the progress that has been made in the two major tasks\, and further discuss the iterative porting process of legacy satellite flight software and/or mission software.
CATEGORIES:GENERAL SESSION
LOCATION:Georgia Ballroom B\, Vancouver\, BC\, Canada
SEQUENCE:0
UID:f9827a590cb7f5f2c4055d7a0591495f
URL:http://sel4summit2026.sched.com/event/f9827a590cb7f5f2c4055d7a0591495f
END:VEVENT
BEGIN:VEVENT
DTSTAMP:20260629T203449Z
DTSTART:20260902T180000Z
DTEND:20260902T181500Z
SUMMARY:Throwing seL4 on the Throwbot 3 Robot - Nathan Studer\, Dornerworks
DESCRIPTION:The Throwbot® 3 Robot by ReconRobotics is a ruggedized\, throwable micro-robot designed for rapid and covert reconnaissance in high-risk and dynamic environments. It is used by law enforcement and military personnel for real-time intelligence gathering\, situational awareness\, and remote investigation under control of a remote operator. Their light weight makes them ideal for many forward situations\, but also vulnerable to being commandeered\, carried off\, and dissected.\n\nBuilding on past and current work this talk will explain how seL4 can be used to increase the security posture of the underlying platform\, further harden the control path\, and add additional protections against the exfiltration of sensitive data. Following this overview\, a demonstration of the modified system using seL4 will be given.
CATEGORIES:GENERAL SESSION
LOCATION:Georgia Ballroom B\, Vancouver\, BC\, Canada
SEQUENCE:0
UID:247bd572ad8015ffe0bc3c65d7ac7964
URL:http://sel4summit2026.sched.com/event/247bd572ad8015ffe0bc3c65d7ac7964
END:VEVENT
BEGIN:VEVENT
DTSTAMP:20260629T203449Z
DTSTART:20260902T181500Z
DTEND:20260902T183000Z
SUMMARY:Assured Robotics Embedded Systems and Applications in Ground Vehicles (ARSENAL) - Dave Lide\, Trusted Science and Technology with Additional Speakers To Be Announced
DESCRIPTION:The Robot Operating System (ROS) is widely adopted on various robotic platforms\, including military robotic ground vehicles. However\, it was not designed for performance and determinism requirements or for the safety and security required for the execution of critical missions. The Robotic Technology Kernel (RTK) is a ROS-based autonomy software library for S&T development that provides a set of common robotics capabilities across a variety of Army platforms. This RTK-over-ROS-over-Linux stack possesses the large resource overhead and attack surface manifested by Linux and its software applications such as ROS\; hence an attacker may use a known vulnerability for Ubuntu to gain a footprint on the vehicle\, causing disastrous consequences (e.g.\, crash). Unfortunately\, unmanned ground vehicles\, when running ROS\, fundamentally lack the necessary security\, resilience\, and performance.\n\nTo tackle this challenge\, Trusted ST is developing the Assured Robotics Embedded Systems and Applications in Ground Vehicles (ARSENAL) solution. The ARSENAL effort will result in a modular\, open\, and secure ROS2 stack (newer version of ROS that contains RTK) on military embedded platforms that will have the following capabilities.\n\n- Enables multiple design and configuration options over the seL4 microkernel (as a separation kernel to provide software-level isolation) to support various platform resources and mission requirements (e.g.\, latency\, space\, throughput\, etc.)\, which will significantly improve interoperability and configurability. ARSENAL can support the conventional ROS2 configuration with reduced attack surface (Option 1 with DDS and minimized Linux kernel on seL4)\, and minimized configuration (Option 2\, DDS/ROS2 on seL4) to run mission applications with minimal platform resource requirements.\n- Ports mission essential application modules over simplified DDS/ROS2 (Option 2) by leveraging ROS2/DDS interoperability and analyzing software dependencies\, resource/performance requirements\, and mission needs. The ported robotics application maintains mission critical functionalities (e.g.\, tele-operation) and eliminates non-mission critical functions (e.g.\, visualization) to reduce size and memory/latency overhead while fully leveraging DDS/ROS2 compatibility and supporting cross-platform\, cross-controller capabilities.\n- Provides strong security services and checks\, including memory separation and process isolation\, data flow monitor\, intrusion detection\, and policy enforcement to thwart known and unknown cyber vulnerabilities as applicable and needed in DoD use cases\, including teleoperation\, autonomy\, and swarm.\n- Enables secure inter- and intra-communication by providing cryptographic solutions on top of the open data transport layer (e.g.\, inter-process communication\, or IPC\, and data distribution service\, or DDS). All data exchanges among multiple robotic applications within a platform and between external platforms can be encrypted with TLS to significantly increase the level of data and information protection.\nWe have performed design analyses and made design decisions\; developed a proof-of-concept of running ROS2 in reduced OS (Option 1)\; and developed a proof-of-concept of running native ROS2 with DDS (Option 2). We will further develop and mature the technology\, comprising four main thrusts: (1) completing the integration of DDS and ROS2 on top of seL4\; (2) developing security capabilities\; (3) upgrading software and tooling that includes transition from CAmkES to Microkit\; and (4) performing capability demonstration.\n\nThe ARSENAL solution (1) takes advantage of open-source ROS2 and seL4 for cost-effective development and adoption\, and (2) fully utilizes the deployed ROS2 stack in various UGVs for easy deployment and interoperability. ARSENAL will provide unprecedented\, holistic security and resilience for Army UGVs\, and therefore fundamentally improve the state of the art of the various autonomy stack and capabilities. Due to its open\, modular\, and standard-based design and implementation\, the ARSENAL stack can be deployed on many unmanned systems to protect mission critical assets with minimal configuration changes.\n\nWe will present our seL4 experience and applications to build security and resilience for these unmanned systems in the real world\, and therefore the talk proposal fits the scope of the seL4 Summit.
CATEGORIES:GENERAL SESSION
LOCATION:Georgia Ballroom B\, Vancouver\, BC\, Canada
SEQUENCE:0
UID:a0654cc2b562d4b6ca9e00f69282ee14
URL:http://sel4summit2026.sched.com/event/a0654cc2b562d4b6ca9e00f69282ee14
END:VEVENT
BEGIN:VEVENT
DTSTAMP:20260629T203449Z
DTSTART:20260902T183000Z
DTEND:20260902T184500Z
SUMMARY:Evolving Legacy Systems Towards Strong Spatial and Temporal Isolation with seL4 - Philipp Scholl\, ABB Corporate Research
DESCRIPTION:ABB develops protection and control systems for safety-critical infrastructure in energy and transportation sectors. These systems operate under hard real-time constraints\, require security and safety assurances\, and incorporate legacy software developed over decades by multiple teams across heterogeneous operating systems. Recently\, regulatory requirements like the EU Cyber Resilience Act [1] demand timely and continuous software updates over long system lifetimes. This poses numerous challenges for the platform architecture and certification strategies.\n\nThe presentation reports on experiences gained while evaluating a mixed-criticality platform based on seL4 [2]\, [3]. The focus is on consolidating hard real-time\, safety-critical protection and control functions with non-critical services on shared hardware\, while preserving determinism and isolation. An architectural mechanism is also presented that enables software updates of non-safety-critical components without violating the isolation\, timing\, and trust assumptions of certified functions. This supports regulatory compliance while minimizing recertification effort. Based on this experience\, the presentation discusses lessons learned\, limitations\, and open challenges encountered when implementing seL4 for such real-time\, secured\, and legacy-driven protection and control systems.\n\n[1] Council of the European Union\, “Regulation (EU) 2024/2847.” 2024. Available: https://eur-lex.europa.eu/eli/reg/2024/2847/oj\n\n[2] G. Klein et al.\, “seL4: Formal verification of an OS kernel\,” 2009.\n\n[3] Z. Kocsis\, M. Paturel\, S. Isitha\, T. Weibel\, and G. Heiser\, “The Sel4 Microkit\,” 2023.
CATEGORIES:GENERAL SESSION
LOCATION:Georgia Ballroom B\, Vancouver\, BC\, Canada
SEQUENCE:0
UID:2bf4c3964bb4b3ad04bce879cbf713fc
URL:http://sel4summit2026.sched.com/event/2bf4c3964bb4b3ad04bce879cbf713fc
END:VEVENT
BEGIN:VEVENT
DTSTAMP:20260629T203449Z
DTSTART:20260902T184500Z
DTEND:20260902T190000Z
SUMMARY:tSDX - Reference Architecture for Software Defined X - Nils Brand\, Fraunhofer IESE
DESCRIPTION:The demand for software-defined systems among businesses is growing rapidly. The software-defined paradigm has been known since the 1990s\, originating in the telecommunications industry with software-defined radio. Since around 2021\, innovation in the automotive industry has focused on implementing the software-defined vehicle paradigm. This led to the creation of COVESA\, and in Europe\, automakers and suppliers joined forces in the Eclipse Foundation for SDV. Other industries seeking to accelerate innovation in safety-critical systems—such as manufacturing\, the defense industry\, and aerospace—are now following this model.\n\nMicrokernels are well-suited as a central building block for implementing the Software-Defined Paradigm\, as demonstrated annually at the seL4 Summit and reflected in over 275 million cars equipped with BlackBerry QNX.\n\nTo enable various industries to implement the Software-Defined Paradigm\, Fraunhofer IESE is researching a reference architecture called: tSDX – trustworthy Software Defined X. The “tSDX” research project has been funded by the German Ministry of Research since May 2026 and initially aims to define an instantiable reference architecture with microkernels as its central building block. In a practical\, application-oriented manner\, requirements and architectural drivers from the defense industry\, aviation\, aerospace\, and manufacturing are being gathered with the consortium. The reference architecture is intended to be vendor-neutral (microkernel-independent) and is currently still under development.\n\nThis presentation aims to convey initial insights and interim results. Furthermore\, the presentation seeks to bridge the gap to practical application and present the needs and pain points of industrial applications to the participating microkernel experts.
CATEGORIES:GENERAL SESSION
LOCATION:Georgia Ballroom B\, Vancouver\, BC\, Canada
SEQUENCE:0
UID:f7beafb1b0c96070832076a3b8727f04
URL:http://sel4summit2026.sched.com/event/f7beafb1b0c96070832076a3b8727f04
END:VEVENT
BEGIN:VEVENT
DTSTAMP:20260629T203449Z
DTSTART:20260902T190000Z
DTEND:20260902T203000Z
SUMMARY:Lunchtime Poster Presentations
DESCRIPTION:1.&nbsp\;TCCoE Overview & Update 2026 - Stuart Card\, Critical Technologies\, Inc.&nbsp\;\n\n2.&nbsp\;Binary Verification for seL4 - Nick Spinale\, Colias Group \n\n3.&nbsp\;VM Composer Poster - Robert VanVossem Dornerworks \n\n4.&nbsp\;Updates on Confidential Computing with seL4 - Alexander Weidinger\, Fraunhofer AISEC \n\n5.&nbsp\;Rethinking seL4 Multicore Architecture: SMP vs. Multikernel - Guangtao Zhu & Julia Vassiliki\, UNSW Sydney\n\n\n
CATEGORIES:POSTER SESSIONS
LOCATION:Georgia Ballroom Foyer\, Vancouver\, BC\, Canada
SEQUENCE:0
UID:eaf797097c276cb7b32d6ed536cc08f9
URL:http://sel4summit2026.sched.com/event/eaf797097c276cb7b32d6ed536cc08f9
END:VEVENT
BEGIN:VEVENT
DTSTAMP:20260629T203449Z
DTSTART:20260902T190000Z
DTEND:20260902T203000Z
SUMMARY:Lunch
DESCRIPTION:\n
CATEGORIES:REGISTRATION / BREAKS / SPECIAL EVENTS
LOCATION:Georgia A\, Vancouver\, BC\, Canada
SEQUENCE:0
UID:631dd8ab2dc145ca662891bc501420fe
URL:http://sel4summit2026.sched.com/event/631dd8ab2dc145ca662891bc501420fe
END:VEVENT
BEGIN:VEVENT
DTSTAMP:20260629T203449Z
DTSTART:20260902T203000Z
DTEND:20260902T210000Z
SUMMARY:seL4's Security Proofs - Ryan Barry\, Proofcraft Systems
DESCRIPTION:seL4’s flagship proof is functional correctness\, which states that the C code behaves according to its abstract specification. This talk introduces the next layer in the assurance stack– seL4’s security proofs. We will present an overview of what they are\, how they are structured\, and where they fit into past\, present\, and future work at Proofcraft.\n\nThe CIA triad of properties– confidentiality\, integrity\, and availability– is the foundation of information security\, and the target of seL4’s security proofs. These proofs establish that seL4’s specification\, and by extension its implementation\, prevents an application running on top from: modifying data without authorisation (integrity)\; interfering with another application’s resource access (availability)\; and learning information without authorisation (confidentiality). Together\, the three guarantee isolation between applications in critical systems\, preventing attacks and bugs in non-critical components from propagating to critical ones.\n\nAs part of a broader push towards a full proof stack for seL4 on 64-bit Arm\, we recently extended the security proofs to AArch64. Among other architectural differences\, this introduced two objects that were new to seL4’s security proofs: VCPUs\, which provide virtual CPUs to guest operating systems under a hypervisor\, and FPUs\, which enable perthread floating point operations. Unlike other objects in memory\, the contents of VCPUs and FPUs are loaded into physical registers whose contents may persist between context switches. This introduces new complexity in a security context\, and required novel proof techniques to accommodate them.\n
CATEGORIES:GENERAL SESSION
LOCATION:Georgia Ballroom B\, Vancouver\, BC\, Canada
SEQUENCE:0
UID:ef286466d12ff094116e8d9841be8b79
URL:http://sel4summit2026.sched.com/event/ef286466d12ff094116e8d9841be8b79
END:VEVENT
BEGIN:VEVENT
DTSTAMP:20260629T203449Z
DTSTART:20260902T210000Z
DTEND:20260902T213000Z
SUMMARY:Trustworthy Systems R&D Update - Gernot Heiser\, UNSW Sydney
DESCRIPTION:This talk will give an overview of the (systems) research and development activities at UNSW Sydney’s Trustworthy Systems (TS) group. It will provide the context for the other TS talks that follow\, and will provide details of the activities not covered by separate talks\, including:\n\n- Microkit\, driver framework and LionsOS progress\n- performance analysis of the seL4 SMP kernel vs the multikernel\n- re-establishing seL4’s worst-case execution time (WCET) analysis for the 64-bit MCS kernel on RISC-V\n- establishing sound instruction-latency bounds for WCET analysis\n- work on a clean model for IOMMU support\n- ... and whatever exciting things that happened in the meantime.\nUpdates on verification work will be provided by Miki Tanaka and Rob Sison in their talks.
CATEGORIES:GENERAL SESSION
LOCATION:Georgia Ballroom B\, Vancouver\, BC\, Canada
SEQUENCE:0
UID:6d6797d8d60afa565f668804da534dd4
URL:http://sel4summit2026.sched.com/event/6d6797d8d60afa565f668804da534dd4
END:VEVENT
BEGIN:VEVENT
DTSTAMP:20260629T203449Z
DTSTART:20260902T213000Z
DTEND:20260902T220000Z
SUMMARY:Where are we with Time Protection? Verification and Cross-domain Communication Update - Rob Sison\, UNSW Sydney
DESCRIPTION:This talk will give an update on the past two years’ advances at Trustworthy Systems in (1) our ongoing efforts to verify time protection for seL4\, as well as (2) our implementation in seL4 of new time-protected cross-domain communication mechanisms on RISC-V Cheshire. On the formal verification front\, I will present our results so far\, thanks to a crucial rethink of our approach to verifying a key aspect of time protection for seL4 down to its C implementation\, which has eliminated the main cause of the project’s previously large number of breakages to seL4’s existing correctness proofs. On the OS kernel design and development front\, I will present both legacy and hardware-supported implementation options we evaluated for seL4 to support cross-domain shared memory and notification mechanisms that ensure one-way communications are truly one way\, without permitting any timing channels in either (but most importantly\, the backwards) direction. I will also remark on where we stand and next steps forward to formalise and verify that time protection is enforced by these new mechanisms.
CATEGORIES:GENERAL SESSION
LOCATION:Georgia Ballroom B\, Vancouver\, BC\, Canada
SEQUENCE:0
UID:71af06aaf2453875b59249d70dc8792d
URL:http://sel4summit2026.sched.com/event/71af06aaf2453875b59249d70dc8792d
END:VEVENT
BEGIN:VEVENT
DTSTAMP:20260629T203449Z
DTSTART:20260902T220000Z
DTEND:20260902T223000Z
SUMMARY:Break
DESCRIPTION:\n
CATEGORIES:REGISTRATION / BREAKS / SPECIAL EVENTS
LOCATION:Georgia A\, Vancouver\, BC\, Canada
SEQUENCE:0
UID:4f05f26d5a47671604232d61870dc154
URL:http://sel4summit2026.sched.com/event/4f05f26d5a47671604232d61870dc154
END:VEVENT
BEGIN:VEVENT
DTSTAMP:20260629T203449Z
DTSTART:20260902T223000Z
DTEND:20260902T230000Z
SUMMARY:Pancake Updates - Miki Tanaka\, UNSW
DESCRIPTION:Pancake is a verification-friendly\, imperative low-level language for systems programming\, which the Trustworthy Systems group at UNSW has been working on to produce verified LionsOS components. Since first introduced in 2024 seL4 Summit\, TS continued with Pancake development and Pancake is now mature enough for our systems engineers to take up and port various components originally written in C to Pancake.\n\nIn this talk\, we report on various recent updates on Pancake and its roadmap\, in the broader context of LionsOS. We’ll cover the progress and plans for the general Pancake language extensions and compiler improvements as well as verification of programs written in Pancake\, in particular device drivers\, both via interactive theorem proving and SMT-based tools.\n\nWe’ll highlight the SMT-based approach via Pancake-to-Viper transpiler as a way towards TS’s vision of making verified software the standard for security- and safety-critical systems\, aiming to make software verification more scalable and less expensive.
CATEGORIES:GENERAL SESSION
LOCATION:Georgia Ballroom B\, Vancouver\, BC\, Canada
SEQUENCE:0
UID:81388b163ce3437db214be0c37724196
URL:http://sel4summit2026.sched.com/event/81388b163ce3437db214be0c37724196
END:VEVENT
BEGIN:VEVENT
DTSTAMP:20260629T203449Z
DTSTART:20260902T230000Z
DTEND:20260902T231500Z
SUMMARY:Verifying seL4 device drivers with CN - Michal Podhradsky\, Galois
DESCRIPTION:While sDDF provides a framework for verification of new drivers with the Pancake language\, and driver synthesis\, the vast majority of current systems relies on proprietary hardware\, and existing drivers written in C.\n\nIn our project with DORNERWORKS we were tasked with verifying an ethernet driver for a deployed system. The ethernet device was similar to Intel e100 hardware. Given the relatively new sDDF framework and Pancake language\, and the tight project timeline and budget constraints\, we decided to verify an already existing driver\, with CN verification tool.\n\nCN was developed by The REMS group at University of Cambridge\, and significantly matured during the PROVERS project. CN targets the C language\, and lets users specify properties for the functions.\n\nWe were able to verify both the driver and a device model reverse engineered from the Intel driver datasheet. We had to stub out the seL4 system calls\, including minimal specifications.\n\nWe believe this contribution bridges the gap between legacy drivers\, and the future where drivers are synthesised and guaranteed to be correct.\n
CATEGORIES:GENERAL SESSION
LOCATION:Georgia Ballroom B\, Vancouver\, BC\, Canada
SEQUENCE:0
UID:62751b821f1ad43eb614105a51793878
URL:http://sel4summit2026.sched.com/event/62751b821f1ad43eb614105a51793878
END:VEVENT
BEGIN:VEVENT
DTSTAMP:20260629T203449Z
DTSTART:20260902T231500Z
DTEND:20260902T234500Z
SUMMARY:Formalising Device Protocols for sDDF Driver Verification - Liam Murphy\, UNSW Sydney
DESCRIPTION:Device drivers are a major source of bugs in operating systems\, making them a primary target for formal verification. However\, many of these bugs come from violations of the device’s protocol or faults in the device’s design\, which cannot be prevented without a formal model of the device’s protocol. Such a model would traditionally be derived from the device’s datasheet\, but the accuracy of this is limited\, as datasheets are often incorrect and/or incomplete.\n\nIn this talk\, we discuss how we leverage our open-source RISC-V SoC\, Serengeti\, to extract formally verified specifications from devices’ Verilog implementations\, simultaneously establishing the absence of device faults. We also cover aspects of our application of these specifications to the verification of sDDF device drivers written in Pancake\, with the goal of establishing end-to-end correctness.
CATEGORIES:GENERAL SESSION
LOCATION:Georgia Ballroom B\, Vancouver\, BC\, Canada
SEQUENCE:0
UID:66041aa6c1e8f26269eb365e198535b7
URL:http://sel4summit2026.sched.com/event/66041aa6c1e8f26269eb365e198535b7
END:VEVENT
BEGIN:VEVENT
DTSTAMP:20260629T203449Z
DTSTART:20260902T234500Z
DTEND:20260903T000000Z
SUMMARY:Verification of a UDP Implementation: Challenges and Solutions - Alain Kägi\, Lewis & Clark College
DESCRIPTION:In prior work\, we have verified the correctness of a C implementation of UDPv6 using AutoCorres2\, a tool to facilitate the verification of C programs in Isabelle/HOL. To achieve high performance\, it is common practice for implementations of such network layers to make repeated small mutations to heap state\, using typed pointers with overlapping address ranges. This approach to network implementations presents additional challenges for the verification efforts.\n\nIn this talk\, we describe some of these challenges and present our solutions. First\, rather than showing direct refinement to a high-level specification\, we prove important invariants at the level of the C specification—a monadic representation of the C code generated by AutoCorres2. Second\, we analyze pointer aliasing manually. Third\, we generalize some of our lemmas both to simplify proofs of the UDPv6 implementation but also to use them towards proving properties about other layer implementations. Fourth\, we refactor code where appropriate\, while preserving performance\, to simplify our proofs. Finally\, we describe how we use these invariants to show refinement.
CATEGORIES:GENERAL SESSION
LOCATION:Georgia Ballroom B\, Vancouver\, BC\, Canada
SEQUENCE:0
UID:a56f042d4701531532f437d8b5cda1ae
URL:http://sel4summit2026.sched.com/event/a56f042d4701531532f437d8b5cda1ae
END:VEVENT
BEGIN:VEVENT
DTSTAMP:20260629T203449Z
DTSTART:20260903T000000Z
DTEND:20260903T001000Z
SUMMARY:Closing Remarks
DESCRIPTION:\n
CATEGORIES:KEYNOTE SESSIONS
LOCATION:Georgia Ballroom B\, Vancouver\, BC\, Canada
SEQUENCE:0
UID:ed6219d1e36aaaf574e5aafa48d47682
URL:http://sel4summit2026.sched.com/event/ed6219d1e36aaaf574e5aafa48d47682
END:VEVENT
BEGIN:VEVENT
DTSTAMP:20260629T203449Z
DTSTART:20260903T153000Z
DTEND:20260904T000000Z
SUMMARY:Registration & Badge Pick-up
DESCRIPTION:\n
CATEGORIES:REGISTRATION / BREAKS / SPECIAL EVENTS
LOCATION:Georgia Ballroom Foyer\, Vancouver\, BC\, Canada
SEQUENCE:0
UID:f09930da81e5c7559739e6ee935ad054
URL:http://sel4summit2026.sched.com/event/f09930da81e5c7559739e6ee935ad054
END:VEVENT
BEGIN:VEVENT
DTSTAMP:20260629T203449Z
DTSTART:20260903T160000Z
DTEND:20260903T163000Z
SUMMARY:Ask Me Anything' with the TSC - Speakers To Be Announced
DESCRIPTION:\n
CATEGORIES:KEYNOTE SESSIONS
LOCATION:Georgia Ballroom B\, Vancouver\, BC\, Canada
SEQUENCE:0
UID:eefb9208a55d3ffef035ac5882dabc74
URL:http://sel4summit2026.sched.com/event/eefb9208a55d3ffef035ac5882dabc74
END:VEVENT
BEGIN:VEVENT
DTSTAMP:20260629T203449Z
DTSTART:20260903T163000Z
DTEND:20260903T170000Z
SUMMARY:Simplifying Microkit System Composition with Acacia - Lesley Rossouw\, UNSW Sydney
DESCRIPTION:The seL4 Microkit has a problem: composing systems becomes very difficult when working with modular code or large code bases. The Microkit Acacia tool (formerly SDFgen) solves this problem by offering a higher-level abstraction for generating Microkit system files\, capable of inserting modules with minimal effort. Acacia has been used extensively as a component of LionsOS and the seL4 Device Driver Framework (sDDF)\, simplifying integrating systems with multiple driver subsystems or high-level LionsOS components like filesystems or the firewall. Recently\, Acacia has been re-implemented in Python for greater ease of use.\n\nThis talk will introduce the community to Acacia with a focus on newly added features which simplify build-time configuration and specification of large systems. We will cover the basics\, starting with simply connecting a few programs together\, and then demonstrate how to add subsystems such as sDDF driver stacks. We will conclude with a tutorial demonstrating how to convert freestanding work into a Acacia subsystem for future reuse\, giving an overview of the architecture of the tool.
CATEGORIES:WALKTHROUGH / TUTORIAL
LOCATION:Georgia Ballroom B\, Vancouver\, BC\, Canada
SEQUENCE:0
UID:ddcdd16eb7fbd1921c6cb691ee354e3c
URL:http://sel4summit2026.sched.com/event/ddcdd16eb7fbd1921c6cb691ee354e3c
END:VEVENT
BEGIN:VEVENT
DTSTAMP:20260629T203449Z
DTSTART:20260903T170000Z
DTEND:20260903T173000Z
SUMMARY:Break
DESCRIPTION:\n
CATEGORIES:REGISTRATION / BREAKS / SPECIAL EVENTS
LOCATION:Georgia A\, Vancouver\, BC\, Canada
SEQUENCE:0
UID:a8eecf8a3faa9aafc403000db27f0228
URL:http://sel4summit2026.sched.com/event/a8eecf8a3faa9aafc403000db27f0228
END:VEVENT
BEGIN:VEVENT
DTSTAMP:20260629T203449Z
DTSTART:20260903T173000Z
DTEND:20260903T180000Z
SUMMARY:A Policy-free Boot Process for seL4 - Daniel Schwyn\, Neutrality
DESCRIPTION:In its current form\, the initialization code of the seL4 kernel dictates the policy of how resources are discovered and what capabilities are created at boot time\, making it hard to integrate into existing boot infrastructure. Wepropose to delegate this policy to a pre-boot component and introduce both an interface and mechanisms for pre-boot infrastructure to communicate resources to the kernel and userspace. Not only does this pave the way for booting seL4 in a multikernel configuration where not all the nodes use the same resources\, it also provides a cleaner separation between verified and unverified code.\n\nContrary to the rest of the design of seL4\, the boot code makes several policy decisions. On x86 for example\, the kernel expects to be booted in protected mode. This is the case when loaded with GRUB. All modern server platforms have an EFI pre-boot environment\, which leaves the CPU already in long mode (Intel-speak for 64bit mode). On Arm platforms the physical memory regions are extracted from a device tree at compile time. While device trees are the standard for embedded systems\, Arm server platforms also use EFI\, which provides a memorymapthatisonlyknownatruntime. Thingswillget even morecomplicated with partitioned multikernel configurations\, where the resources of the nodes need to be disjoint\, and the global memory map provided by the firmware does not have enough information for the kernel to create the right capabilities. In such a setting\, there will also be shared frames that userspace components use to communicate between cores. These are resources that the kernel does not touch but should just be passing to userspace. Currently\, the seL4 ecosystem does not have a mechanism to pass resources at addresses that are not statically known to userspace.\n\nOne could of course add support to the kernel for all these cases that currently are not covered. We however argue\, that like any other policy\, a microkernel should not make these decisions but offer a mechanism that is general enough to cover all potential use cases. We therefore propose to remove all code that decides which resources are used by the kernel and what capabilities are created from the initialization of the kernel. Instead\, the kernel should be getting this information from a pre-boot environment that can be tailored to specific use cases. We therefore propose a boot protocol where the kernel expects to be handed a resource map. To cover the case of pre-boot allocated resources that need to be passed to userspace\, we propose to add support for named resources to CapDL. A statically created specification can e.g.\, specify a specific slot in a CSpace to be populated with a capability to such a resource. The rootserver will then get a mapping from these names to CPointers from the kernel and can distribute the capabilities accordingly.\n\nAn additional benefit of this approach is that the clear interface between the verified kernel and the pre-boot interface makes it easier to specify what the state is that the kernel expects to be booted in. By shipping default pre-boot environments that recreate the current initialization code\, the transition to making seL4 an even more versatile tool than it already is\, can even be seamless.
CATEGORIES:GENERAL SESSION
LOCATION:Georgia Ballroom B\, Vancouver\, BC\, Canada
SEQUENCE:0
UID:e54d9e65a748950a152f4485a68a2904
URL:http://sel4summit2026.sched.com/event/e54d9e65a748950a152f4485a68a2904
END:VEVENT
BEGIN:VEVENT
DTSTAMP:20260629T203449Z
DTSTART:20260903T180000Z
DTEND:20260903T183000Z
SUMMARY:Carrels: Secure\, High-performance Microservice on seL4 - Guangtao Zhu\, UNSW Sydney
DESCRIPTION:seL4\, the world’s first formally verified microkernel\, has demonstrated exceptional reliability in security- and safety-critical systems. However\, its use in large-scale\, server-class environments remains underexplored\, especially for dynamic workloads such as microservices.\n\nIn this talk\, we present Carrels\, a secure and high-performance platform for lightweight\, dynamic applications on seL4. Carrels explores whether seL4 can serve as a practical foundation for microservice-style workloads\, which require strong isolation together with dynamic deployment\, destruction\, and migration at runtime.\n\nCarrels is built on LionsOS\, a highly modular\, high-performance seL4-based operating system designed with formal verification in mind. In Carrels\, microservice applications are encapsulated in a prototype container abstraction: a secure isolation domain whose lifecycle can change dynamically. We implement this abstraction using LionsOS modules\, demonstrating how a largely static seL4-based system can be extended into a semi-dynamic platform for dynamic applications.\n\nWe will present the design and implementation of Carrels\, including its security model\, container lifecycle management\, and resource management. We will also share preliminary performance results\, showing that Carrels can support microservice workloads with low overhead while preserving strong isolation guarantees\, including small trusted computing base and fine-grained access control.
CATEGORIES:GENERAL SESSION
LOCATION:Georgia Ballroom B\, Vancouver\, BC\, Canada
SEQUENCE:0
UID:e85e94bd333db2a72e95208cfefbfe9c
URL:http://sel4summit2026.sched.com/event/e85e94bd333db2a72e95208cfefbfe9c
END:VEVENT
BEGIN:VEVENT
DTSTAMP:20260629T203449Z
DTSTART:20260903T183000Z
DTEND:20260903T184500Z
SUMMARY:Single Kernel Multicore seL4 - Scott Brookes\, Riverside Research
DESCRIPTION:Riverside Research presents an seL4 prototype called SKMS: Single Kernel Multicore seL4. SKMS is a proof-of-concept implementation of a previously proposed multicore microkernel architecture [1] for seL4 microkernel on x86. The current POC implements three basic elements of seL4 functionality: memory isolation\, remote system calls\, and remote scheduling. Memory isolation puts usperspace processes into address spaces with no mappings to the seL4 kernel\, remote system calls forward requests from these processes (loaded on other cores) over to the single kernel core\, and remote scheduling allows the kernel scheduler to choose processes for the remote cores. A preliminary design idea for leveraging this architecture in “proving” a version of seL4 that can schedule processes across many cores is presented for community feedback.\n\n[1] Scott Brookes and Stephen Taylor. 2016. Rethinking operating system design: asymmetric multiprocessing for security and performance. In Proceedings of the 2016 New Security Paradigms Workshop (NSPW '16). Association for Computing Machinery\, New York\, NY\, USA\, 68–79. https://doi.org/10.1145/3011883.3011886
CATEGORIES:GENERAL SESSION
LOCATION:Georgia Ballroom B\, Vancouver\, BC\, Canada
SEQUENCE:0
UID:2d2a7d079bcbcd5137dd44e41e6a5b91
URL:http://sel4summit2026.sched.com/event/2d2a7d079bcbcd5137dd44e41e6a5b91
END:VEVENT
BEGIN:VEVENT
DTSTAMP:20260629T203449Z
DTSTART:20260903T184500Z
DTEND:20260903T190000Z
SUMMARY:Booting Windows on an x86-64 seL4-based VMM - Bill Nguyen\, UNSW Sydney
DESCRIPTION:Historically\, open-source Virtual Machine Monitors (VMMs) built on seL4 have focused largely on Linux guest OS support. Booting a closed-source operating system like Windows on a custom x86-64 VMM introduces a unique set of development hurdles.\n\nThis talk details the engineering effort behind LionsOS to achieve a fully functional x86-64 VMMcapable of running modern Windows and desktop Linux distributions. We will explore the technical realities of this architectural leap\, focusing on the distinct challenges encountered when virtualising Windows. Specifically contrasting the predictable boot process of Linux with the strict firmware assumptions and opaqueness of a Windows guest.\n\nBeyond the boot sequence\, we will unpack how we tackled these hurdles\, detailing the low-level virtualisation and driver solutions required to make this work.\n\nThe talk will conclude with a live demonstration of LionsOS successfully booting into a functional Windows desktop environment.
CATEGORIES:GENERAL SESSION
LOCATION:Georgia Ballroom B\, Vancouver\, BC\, Canada
SEQUENCE:0
UID:254cecc4046fe635315e8c1d8306177a
URL:http://sel4summit2026.sched.com/event/254cecc4046fe635315e8c1d8306177a
END:VEVENT
BEGIN:VEVENT
DTSTAMP:20260629T203449Z
DTSTART:20260903T190000Z
DTEND:20260903T203000Z
SUMMARY:Lunch
DESCRIPTION:\n
CATEGORIES:REGISTRATION / BREAKS / SPECIAL EVENTS
LOCATION:Georgia A\, Vancouver\, BC\, Canada
SEQUENCE:0
UID:10186e59ccffe95236a13addb95fbaaa
URL:http://sel4summit2026.sched.com/event/10186e59ccffe95236a13addb95fbaaa
END:VEVENT
BEGIN:VEVENT
DTSTAMP:20260629T203449Z
DTSTART:20260903T193000Z
DTEND:20260903T203000Z
SUMMARY:Lunchtime Poster Presentations
DESCRIPTION:1.&nbsp\;TCCoE Overview & Update 2026 - Stuart Card\, Critical Technologies\, Inc.\n2.&nbsp\;Binary Verification for seL4 - Nick Spinale\, Colias Group\n3.&nbsp\;VM Composer Poster - Robert VanVossem Dornerworks\n4.&nbsp\;Updates on Confidential Computing with seL4 - Alexander Weidinger\, Fraunhofer AISEC\n5. Rethinking seL4 Multicore Architecture: SMP vs. Multikernel -&nbsp\;GuangtaoZhu & Julia Vassiliki\, UNSW Sydney
CATEGORIES:POSTER SESSIONS
LOCATION:Georgia Ballroom Foyer\, Vancouver\, BC\, Canada
SEQUENCE:0
UID:43ae9e38237e9b3673f05302e6ad81d6
URL:http://sel4summit2026.sched.com/event/43ae9e38237e9b3673f05302e6ad81d6
END:VEVENT
BEGIN:VEVENT
DTSTAMP:20260629T203449Z
DTSTART:20260903T203000Z
DTEND:20260903T210000Z
SUMMARY:Rigorous Agentic Systems Engineering for seL4 using HAMR - John Hatcliff\, Kansas State University
DESCRIPTION:The Collins Aerospace INSPECTA project (part of the DARPA PROVERS program) aims to provide a model-based development tool chain for seL4 with integrated formal methods. The High Assurance Modeling and Rapid engineering for embedded systems (HAMR) framework\, whose development is led by researchers at Kansas State University\, is a key part of the INSPECTA tool chain. HAMR supports modelbased development for seL4 via modeling in SysMLv2\, code generation to C and Rust\, and deployment to seL4 using Microkit and CAmKeS. Key themes of HAMR include component-based development\, multiuse formal behavior contracts integrated across models and code that can be used for formal verification\, automated testing\, and run-time monitoring\, and integration with the Collins INSPECTA assurance case framework. On the INSPECTA project\, HAMR is being applied to increase the cyber-resiliency of several autonomy platforms\, including the Collins Aerospace Rapid Edge mission system.\n\nAt the 2025 seL4 summit\, I gave an overview of HAMR framework\, with an emphasis on its new capabilities for SysMLv2 modeling\, Rust code and contract generation\, and integration of the Microkit framework for configuring seL4. That talk focused on specification and verification of individual components using component contracts. In this talk\, I describe two new layers of capabilities that significantly improve the effectiveness and speed at which seL4-based systems can be developed using HAMR.\n\nFirst\, to improve support for reasoning about component integration and system level reasoning\, HAMR model and code generation has been extended to support auto-generation of multiple forms of run-time monitoring including run-time checking of component contracts\, system contracts\, and checking of Mission Time Temporal Logic specifications using R2U2 framework. Several aspects of this work leverage new capabilities for “user-land” static scheduling of HAMR components (Microkit protection domains) recently added by UNSW to Microkit.\n\nSecond\, I give an overview of an emerging agent-based engineering framework for HAMR that supports automated development of HAMR models\, contracts\, component application code\, testing and verification\, assurance\, and reporting tasks. Several INSPECTA teams are collaborating on building out these capabilities. Our team’s contributions have included (a) integration of Model-Context-Protocol (MCP) support for a variety of HAMR modeling\, coding\, contract verification\, and testing capabilities\, (b) specification of HAMR process/workflow steps that agents follow to develop HAMR-based systems on seL4\, (c) agent skills that support workflow steps\, and (d) specification of human/agents interaction points to support design\, property-specification and validation\, and audits. I summarize my views of the benefits of model-based development and seL4 in the context of agentic development of high-assurance systems\, and I describe how KSU contributions are integrating into the broader INSPECTA work on agentdevelopment. I present outcomes of experiments that we have carried out with this framework including the direction and interaction with the system monitoring capabilities listed above as applied to the INSPECTA Open Platform autonomy reference examples.\n\nHAMR is available under an open-source license\, and the project website includes an example repository and collection of videos\, tutorials\, and classroom lecture materials (also suited for workforce training).\n
CATEGORIES:GENERAL SESSION
LOCATION:Georgia Ballroom B\, Vancouver\, BC\, Canada
SEQUENCE:0
UID:bb0646a9b2503a9ef74136cb77c1a3c6
URL:http://sel4summit2026.sched.com/event/bb0646a9b2503a9ef74136cb77c1a3c6
END:VEVENT
BEGIN:VEVENT
DTSTAMP:20260629T203449Z
DTSTART:20260903T210000Z
DTEND:20260903T211500Z
SUMMARY:Accessible Formal Methods – Building on a Strong sel4 Foundation Nick Tudor\, D-RisQ Ltd.
DESCRIPTION:While sel4 provides a sound foundation upon which to build\, it remains the case that applications can be built that are on their own unsound\, insecure and unsafe. The work to develop applications needs rigorous\, accessible tool support in order to more quickly build and deploy assured software systems. For decades\, formal methods have been acknowledged as a very powerful set of techniques with potential to significantly improve the speed and quality of software deployment but usually requiring the use of rare and often expensive skills to deploy effectively.\n\nFor this presentation\, we used an open problem statement by Abrial [1] referred to as the ‘Steam Boiler’. The case study was implemented using a team of professional software engineers and commercially supported tools. The presentation will highlight how the Abrial informal specification was used as the basis for the development of a set of System Requirements using structured English and how formalism can be introduced through software requirements\, design and code and used as the basis for automatic\, independent formal verification. The exploration of desired properties at the requirements level is explored formally. The final aspect discussed is the potential for formal verification of the Executable Object Code exploiting a formalised Instruction Set Architecture in the same graph language used by the sel4 project.\n\nIndeed\, the sel4 graph language is also used\, at least partially\, in automatic verification of source code against design and in design against requirements. The possible claims for certification credit are also discussed. While the example sector is nuclear\, we have used a more accessible and more widely understood software standard from the aerospace sector\, DO-178C [2]\, as amended through use of DO-333 [2]\, the formal methods supplement. A summary of the claims will be provided\, including limitations and how tool qualification using DO-330 [4] can be used to support certification. Finally\, metrics are presented\, including the hours of effort expended on development\, verification and an example is given on how quickly changes can be incorporated showing just how agile the techniques are and the consequent impact on time to market could be.\n\n[1] Abrial\, J-R.: Steam-Boiler Control Specification Problem. In: Abrial\, J-R.\, Borger\, E.\, Langmaack\, H.: (eds.) Formal Methods for Industrial Applications 1996\, LNCS State-of-theArt Survey\, pp. 500–509. Springer\, Heidelberg (1996).\n\n[2] DO-178C: Software Considerations in Airborne Systems and Equipment Certification\, Issue C\, 13th December 2011.\n\n[3] DO-333: Formal Methods Supplement to ED-12C/DO-178C and ED-109A/DO-278A\, 13th December 2011\n\n[4] DO-330: Software Tool Qualification Considerations\, 13th December 2011.
CATEGORIES:GENERAL SESSION
LOCATION:Georgia Ballroom B\, Vancouver\, BC\, Canada
SEQUENCE:0
UID:ee710144be39eefd276c5a17ee9959df
URL:http://sel4summit2026.sched.com/event/ee710144be39eefd276c5a17ee9959df
END:VEVENT
BEGIN:VEVENT
DTSTAMP:20260629T203449Z
DTSTART:20260903T211500Z
DTEND:20260903T213000Z
SUMMARY:Efficient User-level Physical Memory Management on seL4 - Guangtao Zhu\, UNSW Sydney
DESCRIPTION:seL4 gives user-level systems a great deal of control over hardware resources through capability-protected kernel abstractions. This is powerful\, but it also means that performance depends heavily on how user-level resource management is designed.\n\nIn this talk\, we use physical memory management as a case study. We show that the wrong design can make dynamic memory allocation expensive by placing capability-related operations and metadata bookkeeping directly on the allocation critical path.\n\nWe then present a different design: keep the fast path small\, and move capability-heavy functions out of the critical path whenever it can be prepared ahead of time or handled asynchronously. We implement this idea in the seL4 library OS and compare it with baseline designs.\n\nThe results show that efficient dynamic memory management is practical on seL4\, but only if the memory manager is designed to respect the cost structure of capability-based systems.
CATEGORIES:GENERAL SESSION
LOCATION:Georgia Ballroom B\, Vancouver\, BC\, Canada
SEQUENCE:0
UID:8e7dda5535043b1de88de93350aa46f3
URL:http://sel4summit2026.sched.com/event/8e7dda5535043b1de88de93350aa46f3
END:VEVENT
BEGIN:VEVENT
DTSTAMP:20260629T203449Z
DTSTART:20260903T213000Z
DTEND:20260903T214500Z
SUMMARY:Modeling and Performance Analysis of Ethernet on LionsOS - Lesley Rossouw\, UNSW Sydney
DESCRIPTION:Performant networking is critical for many practical computer systems. Since 2022\, the seL4 Device Driver Framework (sDDF) has included an Ethernet driver capable of strong performance without compromising on trustworthiness. Under LionsOS\, the sDDF has been shown to be capable of supporting a variety of intensive use cases such as a firewall and webserver.\n\nIn this talk we will discuss ongoing modelling and analysis of the sDDF ethernet class using discrete-event simulation and practical benchmarks. We will present new observations on the dynamic properties of its radically simple design and explore the theoretical limits of the sDDF design philosophy.
CATEGORIES:GENERAL SESSION
LOCATION:Georgia Ballroom B\, Vancouver\, BC\, Canada
SEQUENCE:0
UID:eeb6d5ba295206d46e82e0a420d02c60
URL:http://sel4summit2026.sched.com/event/eeb6d5ba295206d46e82e0a420d02c60
END:VEVENT
BEGIN:VEVENT
DTSTAMP:20260629T203449Z
DTSTART:20260903T220000Z
DTEND:20260903T224500Z
SUMMARY:BoF Session: Details To Be Announced
DESCRIPTION:\n
CATEGORIES:BOF SESSIONS
LOCATION:Georgia Ballroom B\, Vancouver\, BC\, Canada
SEQUENCE:0
UID:339c5491bb0eae8b43cbfd564884f1ad
URL:http://sel4summit2026.sched.com/event/339c5491bb0eae8b43cbfd564884f1ad
END:VEVENT
BEGIN:VEVENT
DTSTAMP:20260629T203449Z
DTSTART:20260903T224500Z
DTEND:20260903T231500Z
SUMMARY:Break
DESCRIPTION:\n
CATEGORIES:REGISTRATION / BREAKS / SPECIAL EVENTS
LOCATION:Georgia A\, Vancouver\, BC\, Canada
SEQUENCE:0
UID:2b70632c12497ededa6caad4992fd15d
URL:http://sel4summit2026.sched.com/event/2b70632c12497ededa6caad4992fd15d
END:VEVENT
BEGIN:VEVENT
DTSTAMP:20260629T203449Z
DTSTART:20260903T231500Z
DTEND:20260903T234500Z
SUMMARY:BoF Session: Details To Be Announced
DESCRIPTION:\n
CATEGORIES:BOF SESSIONS
LOCATION:Georgia Ballroom B\, Vancouver\, BC\, Canada
SEQUENCE:0
UID:35d4edbd158303db89e1413dc168749b
URL:http://sel4summit2026.sched.com/event/35d4edbd158303db89e1413dc168749b
END:VEVENT
BEGIN:VEVENT
DTSTAMP:20260629T203449Z
DTSTART:20260903T234500Z
DTEND:20260904T000000Z
SUMMARY:BoF Wrap-up
DESCRIPTION:\n
CATEGORIES:BOF SESSIONS
LOCATION:Georgia Ballroom B\, Vancouver\, BC\, Canada
SEQUENCE:0
UID:a41a50cad16adb354f19fae8fa887918
URL:http://sel4summit2026.sched.com/event/a41a50cad16adb354f19fae8fa887918
END:VEVENT
BEGIN:VEVENT
DTSTAMP:20260629T203449Z
DTSTART:20260904T000000Z
DTEND:20260904T001000Z
SUMMARY:Closing Remarks
DESCRIPTION:\n
CATEGORIES:KEYNOTE SESSIONS
LOCATION:Georgia Ballroom B\, Vancouver\, BC\, Canada
SEQUENCE:0
UID:069e21bfd9ca1203cb4f8bb323c94f3b
URL:http://sel4summit2026.sched.com/event/069e21bfd9ca1203cb4f8bb323c94f3b
END:VEVENT
END:VCALENDAR