1 - 3 September | Vancouver, Canada BC View More Details & Registration The schedule is subject to change, so please check back before the event for the most up-to-date information.
Please note that all session times are listed below in Pacific Daylight Time (PDT), UTC-7.
Sign up or log in to add sessions to your schedule and sync them to your phone or calendar.
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.
This 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.
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.
Contrary 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.
One 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.
An 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.
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.
In 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.
Carrels 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.
We 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.
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.
[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
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.
This 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.
Beyond the boot sequence, we will unpack how we tackled these hurdles, detailing the low-level virtualisation and driver solutions required to make this work.
The talk will conclude with a live demonstration of LionsOS successfully booting into a functional Windows desktop environment.
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.
At 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.
First, 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.
Second, 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.
HAMR 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).
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.
For 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.
Indeed, 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.
[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).
[2] DO-178C: Software Considerations in Airborne Systems and Equipment Certification, Issue C, 13th December 2011.
[3] DO-333: Formal Methods Supplement to ED-12C/DO-178C and ED-109A/DO-278A, 13th December 2011
[4] DO-330: Software Tool Qualification Considerations, 13th December 2011.
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.
In 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.
We 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.
The 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.
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.
In 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.
