seL4 Summit 2024

The Kry10 operating system supports some dynamic behaviours, including incremental updates to running systems. To ensure that the OS always enforces the access controls specified by device owners, we must verify the privileged OS components that manage system resources across updates. Verification will soon be further complicated by the addition of support for multikernel systems, because the OS will need to coordinate resource management across cores.

Concurrency is therefore fundamental to our approach. There is concurrency between the resource managers on different cores, and also between each resource manager and the apps and kernels in the system. We hope to use the structure of the system to avoid fine-grained reasoning as much as possible. But we want a framework which will allow us to prove that such structural reasoning is sound, rather than forcing us to assume it.

Though our plans might be grand, our first steps must be small. In particular, we need experience with techniques and frameworks for reasoning about concurrency.

In this talk, we present our initial experiments with concurent user-space verification. We use the Iris separation logic framework to build an abstract model of a simple system in which components interact using shared memory and notifications, and we prove a simple correctness property. We explain the limitations of this experiment, and how we plan to address them in our next steps.

At the heart of every modern server platform sits an embedded system called theboard management controller (BMC) that is responsible for the low-levelfunctioning of the platform. Despite their critical nature, they are generallynot built as trustworthy systems. We have embarked on a journey tocyber-retrofit BMC firmware with seL4 as the kernel. In this talk, we present anupdate on our efforts -- generate trustworthy hardware/software I2C drivers. I2C is a low-level protocol used by BMCs to communicate with many peripherals(e.g. the power regulators). Unlike memory-mapped devices with one-to-oneinterfaces with the BMC, multiple I2C devices may share the same bus. Quirks ofone device can influence the whole assemblage. Therefore, to produce a correctdriver for I2C (and other bus-based protocols), we need to consider thespecifications of not only the controller but all devices on the bus.

We present Efeu, a framework that allows us to specify both the host-side driverand the peripherals. The specifications are composed of layers, which enableefficient modeling of different devices (including those with quirks). Theentire system is then model-checked using SPIN to ensure interoperability. Fromthat, Efeu generates trustworthy drivers in software and hardware. The softwareimplementations target seL4, but could also address other operating systems.Furthermore, when I2C communication speed or CPU usage is a concern, Efeu allowsgenerating hybrid hardware/software drivers, where the hardware part can bematerialized on programmable hardware such as Field Programmable Gate Arrays(FPGAs). We evaluated Efeu-generated I2C stacks on a Zynq MPSoC and show thatmodel-checking the whole system and generating the full stack is not onlypractical but that the resulting implementations can saturate the I2C bus andachieve competitive performance with off-the-shelf solutions.

The seL4 Device Driver Framework (sDDF) provides a lightweight library of device drivers and supporting virtualising components which allow clients to securely access and share devices. Each sDDF component is designed to handle one primary concern, and as a result, components have minimal knowledge of the system as a whole and instead communicate only with their direct neighbours. Components are event driven and and require a signal to be scheduled to process incoming data. A signalling protocol is the decision process a component goes through when deciding whether to signal its neighbour.

If a component signals its neighbour unconditionally when data is available, the system progresses without deadlock, however this often results in a large number of unnecessary signals - meaning the receiver was already awake, or had already been signalled but was yet to be scheduled. Designing a signalling protocol that avoids these unnecessary signals, but does not skip any necessary ones can be challenging, since the experimental absence of deadlocks does not necessarily imply deadlock freedom, and if a deadlock is encountered, it can be hard to replicate and understand.

Using formal methods, and in particular model checking, vastly improves the development process of signalling protocols, since the tool can verify for deadlock freedom whilst also producing detailed traces (interleavings of executions) when a deadlock is found. This talk details how the model checker SPIN was used to develop and analyse sDDF signalling protocols, ultimately resulting in a verified protocol that reduces the number of unnecessary signals by 47% when compared to unconditionally signalling.

The development and maintenance of Rust support in seL4 userspace has been an official seL4 Foundation project since last year’s summit. This project’s scope includes libraries for interacting with the seL4 API, higher-level libraries for use in seL4 userspace (e.g. support for asynchronous programming and integration with the seL4 Device Driver Framework), Rust language runtimes for root tasks and Microkit protection domains, modular building blocks for custom seL4 userspace Rust language runtimes, a CapDL system initializer implementation, and an easy-to-use kernel loader. The past year has seen the expansion and refinement of this project’s library offerings, the release of relevant educational materials, and further integration with the rest of the seL4 software ecosystem. In this talk, we will cover progress since last year’s summit, demonstrate how to leverage this work in your own systems, and share our vision and goals for the path ahead.

We introduce Pancake, a new language for verifiable, low-level systems programming, especially device drivers. Pancake features a simple type system that makes it attractive to systems programmers, while at the same time aiming to ease the formal verification of code. Pancake has well-defined semantics which the compiler is proven to preserve, meaning that each generated binary code preserves the semantics of its original program. We have now extended Pancake with the shared memory capability which allows the programs to access device registers without escaping to C.

We present the design of the language and its verified compiler, as well as demonstrating its usability, performance and current limitations through case studies of device drivers and related systems components for an seL4-based operating system.

When a digital system is undergoing cyber attack or is failing in some way, it is often necessary to take action different from its usual operating mode. These alternative modes of operation are called Reserve Modes. 

There are several challenges in implementing reserve modes in systems. The first challenge is developing a mechanism for defining and loading all modes into a system at boot time and enabling alternative modes as necessary. The second challenge is making these changes without affecting or disturbing parts of the system not involved in the reserve modes. The final and hardest challenge is being able to perform such system level changes with assurance that the reserve modes will be enabled as required and operate as expected, without modification.

This presentation introduces Assured Reserve Modes on the seL4-based Kry10 OS. Assured Reserve Modes are a mechanism for providing reserved modes that successfully address the above challenges - implementing reserved mode functionality and providing assurance that they work correctly.  We explain the concept of reserve modes and provide examples of reserve modes and their benefits, present the Assured Reserve Mode design and implementation, and discuss how to provide the assurance that they require.

 

Assured Reserve Modes are a mechanism that we’ve developed for the seL4-based Kry10 OS that allows a system to switch between pre-configured operating modes at runtime in response to security, safety, and other routine operational events. In this presentation we show the operation of assured reserve modes in action.

We present the Kry10 OS design and implementation of assured reserve modes, demonstrating their application to a representaive industrial control system (based on the Fischertechnik Training Factory 4.0).  The system is exposed to security and safety incidents, which it will detect and then switch into appropriate reserve modes in order to mitigate, resolve, or contain the problem.

This presentation is a companion to the Assured Reserve Modes presentation that describes the assured reserve mode model and mechanism itself.

Container solutions have been instrumental throughout cloud computing, influencing how developers build and automate their application deployments. A core benefit behind containers is that they provide a standardised abstraction layer of an application's underlying OS infrastructure. These abstractions help isolate an application's code and system dependencies, whilst conveniently packaging said dependencies into images that can be easily revision controlled and managed in CI/CD pipelines. When applying this technology to embedded systems, containers offer the potential for simplifying application development workflows, whilst also providing a useful CI/CD mechanism for deploying software updates to deployed devices. seL4 is uniquely suited to power a modern generation of embedded devices and using containers brings with it modern software development practices that makes it easier to manage fleets of devices.

Deploying containers on embedded systems is not necessarily new and has been demonstrated across various embedded Linux deployments. At Kry10 we recognise the value of using containers and see the conveniences it can bring to a developers workflow and the capabilities it provides for developing update-able and maintainable systems. We've implemented first-class container support in Kry10 OS that allows developers to define and package native and VM-based applications. In this talk, I'll present the design and implementation behind our seL4-based container support. I'll step through how container builds are used to package and deploy different types of applications on Kry10 OS, starting from simple native applications, and as the needs and runtime requirements of the application grow, moving onto more complex microVM-style applications.

The utilization of seL4, a high-assurance microkernel, in a Trusted Execution Environment (TEE) on RISC-V hardware, presents a robust solution for secure computing. This year, we build upon our foundational work with new insights into the performance impacts and enhancements of our TEE.
We present empirical data on the CPU, memory, and I/O performance impacts of having a seL4 TEE on a PolarFire RISC-V platform and run different TEE services performance measurements. The insights into performance nuances, such as the minimal overhead introduced by the seL4 TEE and its operational efficiency in handling cryptographic tasks, solidify the practical benefits of our architecture. Furthermore, we outline ongoing advancements and future directions in enhancing the seL4-based TEE.

A formally-verified microkernel is a great start, and an OS needs more than a microkernel. Over the past years, we have been building a vehicle operating system and toolsets based on seL4 from scratch. It is very challenging, especially when dependability is the top priority. In this talk, we would like to share our experiences along the journey, with an emphasis on the following topics: (1) POSIX or not, that is not a question. To leverage the existing code base and 3rd party libraries, a layered approach is adopted: The system has a core system call layer and a POSIX layer based on the core layer. System components use the core layer. Applications and 3rd party libraries use the POSIX interfaces. (2) Tooling is especially important for development efficiency and system usability. System status monitoring and comprehensive logging are critical since we rely on them to analyze issues remotely. Additionally, a building and integration tool is specifically designed to manage the building and releasing process of the OS and applications. (3) Resource management needs more thoughts. Seasoned system developers are surprised by another form of resource leakage: capability slot leakage. Access control to resources that are not managed by the kernel directly through capabilities also deserves some discussion. (4) Product-level maturity is paramount. We wish that the major OS components could be verified, but at least for now, realistically, various levels of testing are used to stabilize and mature the new OS.

Since 2021, a small team at Capgemini have been making contributions toward the seL4 infrastructure, assisting developers in getting started with seL4. Previously, building atop CAmkES, we presented a Developer Kit (from zero to "hello world"), a framework to access the U-boot driver suite, and initial efforts in preparing a native xHCI driver (USB 3.0). Now, we present the conclusion of these efforts.
We transition our entire suite of contributions from CAmkES to Microkit. A greater range of USB device classes are now supported. A simple native HDMI driver is introduced. And we leverage sDDF and VMM, in permitting the secure routing of a selected physical USB device into a guest host. While our primary focus has been the Avnet MaaXBoard, many of these contributions would be readily portable to other platforms. More generally, as our focus on seL4 infrastructure reaches a conclusion, we describe our journey with seL4 thus far, summarising our overall contributions and experiences.

In 2017 Cog Systems developed a single domain virtualized device on an HTC One A9 smartphone, and successfully validated it against the National Information Assurance Partnership (NIAP) Protection Profile (PP) for Mobile Device Fundamentals (MDF) and registered the device with the National Security Agency (NSA) as an Approved Component
under its Commercial Solutions for Classified (CSfC) process. In the past few years we have been building the next-gen version of this solution.

At the 2020 seL4 Summit, Cog Systems presented this effort as a case study in applying seL4 to a product commercialization effort. Since then, the project has experienced multiple and varied challenges, and has not yet been completed. At the 2023 Summit we gave a follow-up presentation detailing the progress, setbacks, and lessons learned of the past few years. Now, in the 2024 continuation of the series, Cog Systems will provide an update and share some of
the technical, logistical, and financial challenges we encountered while building a commercial smartphone product with seL4.

Compiling the seL4 kernel itself might be simple, but once more and more of the seL4 ecosystem is involved, transitive dependencies from Python to Haskell complicate things. To tackle this complexity, we added yet another layer on top, a declarative build system that allows to provide all the (transitive-) dependencies from one hand: Nix.
This talk introduces you to the seL4-nix-utils, a collection of Nix expressions to compile but also ease integration and project bring-up with seL4. After a brief introduction to the mechanism behind Nix, we outline the provided Nix expressions and their use-cases. The talk closes with a list of remaining pain-points and a reference to a hands-on you may try ater the talk.