seL4 Summit 2022 Abstracts

I will provide an overview of the seL4-related research activities of the Trustworthy Systems group at UNSW, and how they relate to each other and the overall seL4 vision. Some of these activities will be covered in more detail in the afternoon session (seL4 Core Platform and seL4 Device Driver Framework), so I will mostly provide context for them and focus on the activities that will not be discussed further. These include:

I will also attempt to provide some context for various pull requests against the kernel originating from TS.

Verification makes seL4 unique. With increasing adoption, seL4 is evolving to support more platforms, architectures, configurations, and features, meaning its formal proofs must evolve as well. Proofcraft is committed to keep this evolution alive. In this talk, we will present the status of the seL4 verification roadmap.

seL4’s extensive formal verification comprises formal proofs of a number of properties for various hardware architectures: AArch32, Intel x64 and RISC-V (64-bit). These properties include:

The verification matrix of architectures, properties, configurations and seL4 features is ever evolving. AArch32 still has the most complete proof stack, but RISC-V is catching up. Intel x64 and AArch32 with hypervisor extensions have verified functional correctness. The current roadmap includes completion of the seL4 MCS configuration (support for mixed-criticality systems), functional correctness of seL4 on AArch64, and progress on multicore seL4 verification.

Kry10 is building a cost-effective platform for connected devices, with extreme security and reliability. We choose to build on seL4 because its capability model gives us the mechanisms, and its verification gives us the confidence that we need. But how do we understand what the verification says about how we should use seL4's mechanisms to build secure systems?

From the functional correctness and invariant proofs, we know that the implementation has no behaviours that aren't permitted by the specification, and that the specification is internally consistent. But the specification still contains considerable detail. When viewed from the perspective of a user outside the kernel, it can be hard for a mere mortal to infer the security properties of a particular system design.

In this presentation, we will look at the seL4 integrity theorems, which give us an abstract way to understand the authorities that components in a system have over each other. We'll see how to construct abstract authority graphs, called policies, and how they relate to individual system states through policy refinement. Policy refinement is a purely static view of the system state, which is appropriate for system initialisation, but we're also interested in how the system evolves from its initial state. So we define integrity as the system state changes that we want to allow for a given policy, and prove that actual state changes are bounded by that definition. Note that integrity does not tell us whether the new state is governed by the same policy, so a separate proof, called authority confinement, shows that state changes preserve the policy refinement.

Both theorems are subject to some well-formedness assumptions about the policy. These assumptions are important for system designers who want the benefit of the theorems, because they act as constraints on their system designs. So we'll examine these conditions in detail, and consider what they mean for static systems such as those produced by the CAmkES tool and the capDL loader. We'll also look at more dynamic systems, where we'll see that with careful design, the theorems can still provide some benefit.

The seL4CP is a very lightweight OS environment for seL4 that’s presently being developed by Breakaway in collaboration with TS. Compared to CAmkES, seL4CP abstractions map more directly on seL4 primitives, and it dissociates app development from the kernel build system, allowing easier integration into the developer’s preferred development environment. The seL4CP was originally presented as a concept at the 2020 seL4 Summit. It now has an implementation that is already used in products. The talk will provide a refresher on the seL4CP’s concepts and will the discuss recent/on-going work, which falls into two broad categories:

a) Verification: this has itself two thrusts:

b) Adding dynamic features to seL4CP. This is a multi-step process, of making apps restartable to supporting empty app slots that can load arbitrary apps at run time

Both categories are work in progress, with prototypes of partial functionality available at time of writing, significant progress is expected by the time of the Summit.

Here we present a framework for high-performance I/O on seL4 that enables formal reasoning, eventual verification and demonstrates performance competitive with Linux in a networking focused system. Unlike monolithic kernels, the seL4 microkernel prescribes device drivers to run as user level programs. This has the advantage that a driver’s special privileges are reduced to just the ability to access the control registers of the device it drives, thus significantly reducing the system’s trusted computing base. However, the extra context switches involved in such a system can degrade performance. The seL4 Device Driver Framework (sDDF) aims to provide interfaces and protocols for writing and porting device drivers to run as seL4 user-level programs. It assumes a simple and general device model, and presents an asynchronous transport layer as a means of communication to other components in the system. It currently supports network devices to run at near wire speed.

Verified multicore seL4 seem too far away? Think again, this talk presents a simple multikernel approach to achieve this goal that is attainable using the verified unicore kernel we already have. While this solution does not provide all the benefits of a single system image it allows us to build static systems on a verified seL4 using multiple cores today. This talk will detail how to construct such a system, the work involved and examples of how it can be used.

The traits of seL4 makes it an appealing hypervisor platform. Today hypervisors are increasingly used to build complex security- and safety critical systems. Good and stable abstractions are required to build upon, and that in turn needs a vivid community of developers and maintainers. Having access to stable and high quality drivers can help building such a community, and is one step towards having seL4 on par feature-wise with the other hypervisors. At TII we explored if QEMU could be used as a VirtIO backend for seL4. The QEMU would bring the tried and tested VirtIO backend, and already thriving ecosystem to work with. Having VirtIO backend running in a Linux VMs user space has its benefits, but also comes with an overhead cost. This talk walks through our journey with having a QEMU within a Linux VM on top of seL4 to provide paravirtualized devices to the other VMs. We share how we went about getting the QEMU working with seL4 along with the benchmarks, the learnings and the pain points. We share where we are at the moment, and our plans for the future.

The talk gives an overview about what works more or less out of the box for ARM and RISC-V and what advances configuration and debug options can be used. Then we will look at the limitations of the various emulated machines and some pitfalls. Finally we will explain some of the modifications we have done to the QEMU sources, so it provides some otherwise missing features.

Our work has been aimed towards easing the overheads for new users to adopt seL4. To support this, we have developed a relatively quick and easy method for providing a high level of driver coverage for an i.MX8MQ-based board (Avnet MaaXBoard). The approach implements a framework to support the U-Boot Driver Model, a standard model employed by U-Boot for defining and interfacing to device drivers. With that framework implemented, the drivers already available in U-Boot (which comprise a very large set) can be made available within seL4 with either limited or zero code changes to the driver itself.

Our approach has so far been used to port several drivers from U-Boot including USB3.0, Ethernet, MMC, GPIO, I2C, SPI.

This approach is not optimised for performance or verifiability and is unlikely to be used for drivers where this is paramount. However, our approach is intended to be complementary to such use cases, with significantly less handcrafting of bespoke drivers, helping to lower the bar for entry into seL4 development.

Microarchitectural timing channels enable information transfer between security domains that are supposed to be isolated, bypassing the operating system's security boundaries. They result from shared microarchitectural state that depends on execution in one security domain and impacts timing in another. Since modern ISAs do not specify timing behaviour, they are insufficient to address these channels.

In this talk, we present fence.t, a novel RISC-V instruction that clears the processor's microarchitectural state and thus any timing dependence on execution history. We show how this instruction was implemented in an open-source RISC-V core and integrated into an experimental version of seL4 with time protection. Furthermore, we will address the challenges of fence.t and its future roadmap.

The Kry10 Secure Platform is a new seL4-based platform that brings security and reliability to industrial connected devices. The platform is based on a philosophy of "Trust but Isolate" - build trusted software to the best quality, but isolate it so that if problems do occur, they cannot spread to the rest of the system.

"Trust but isolate" requires: strict spatial and temporal isolation for OS processes, modular system design that benefits from and takes advantage of isolation to contain any errors, and the ability for application and OS software to be restarted and updated without causing downtime for the rest of the system.

The foundation of the Kry10 Secure Platform is Kry10 OS (KOS), an OS based on the guaranteed isolation provided by the seL4 microkernel. KOS builds on top of seL4, providing a dynamic runtime environment that allows for a flexible and updateable system architecture. KOS integrates an Elixir-based application environment bringing the resilience and concurrency benefits of the BEAM to connected devices. KOS also enables fine-grained and efficient system updates, so that updates can be performed on specific application or system components without affecting other running components, thus virtually eliminating the need for scheduled downtime. Finally, KOS provides a high quality development environment with API and tools that are designed to be consistent, understandable, and usable.

In this presentation we will introduce the Kry10 Secure Platform with its Trust but Isolate philosophy, and then show how the Kry10 Operating System implements this philosophy to achieve a secure and robust platform for industrial connected devices.

When building secure and robust systems, the general strategy is to "prevent, contain, and recover". Ideally we prevent problems (like errors and vulnerabilities) from occurring in the first place, contain the effects of any problems that do occur, and recover from those problems by repairing any damage and ensuring the problems do not happen again in the future.

SeL4 provides excellent spatial and temporal isolation mechanisms to help contain any potential problems, but it does not address prevention and recovery - gaps left for user-level software running on top of the kernel. The BEAM virtual machine and its Erlang and Elixir programming environments provide one of the best opportunities to fill these gaps. Developing code based on the BEAM and its programming environments prevents many errors from occurring, leading to robust user-level components. The BEAM also provides strong fault-recovery mechanisms based on its supervision trees and a "crash and restart" philosophy coupled with dynamic code (re)loading. This, combined with seL4's strong isolation, leads to systems that can realise the full "prevent, contain, and recover" strategy.

In this presentation we will demonstrate what can be achieved by combining seL4 and the BEAM. We will also describe our experience with building BEAM-based systems on seL4, including porting the BEAM to run on seL4, integrating the BEAM with seL4 inter-process communication mechanisms and other C-based components, and creating a powerful Elixir-based development environment for seL4 systems.

Most modern computing platforms are so complex that they need a separate embedded system to manage them. These systems are referred to as (Base-)Board Management Controllers or BMCs. BMCs handle power and clock distribution and sequencing, firmware for other components on the board, and usually offer remote management capabilities (e.g. console access and firmware updates). This makes them the root of trust in such systems.

Although BMCs have absolute power over modern computing platforms they are not engineered in the rigorous way that warrants the implicit trust that we put in them. In our talk we will present ongoing work on declarative power and clock management and our broader vision of a trustworthy BMC software stack with, at its heart, seL4 as a separation kernel. Not only will a trustworthy BMC stack improve safety and security of modern computing platforms but, with the right tools for generating code from declarative models, it has the potential to shorten bringup times for new platforms.

The Rust programming language and ecosystem offer memory safety and developer productivity even at lower levels of the software stack. There are numerous efforts within the seL4 community towards laying groundwork for an accessible development story for Rust in the seL4 userspace. This talk explores the technical considerations related to Rust in the seL4 userspace, surveys the accomplishments and directions of these efforts, and then calls for the participation of interested parties in the ongoing design and implementation of Rust support in the upstream seL4 software ecosystem.

We are investigating the question of whether the field of software verification has matured enough to allow a small group of researchers at two undergraduate institutions to prove correctness properties of network protocols implemented in operating system distributions, in general, and IoT devices, in particular. As a proof of concept, we are designing a networked temperature sensor, to monitor incubators, built on top of the seL4 microkernel and seL4® core platform. In this talk, we will share our early experience building and proving some properties about such a system. In particular, we will describe our efforts developing our own UDP networking stack, testing IPv6-based protocols, proving properties about reassembly of network fragments, and finding possible inconsistencies in specifications published by the Internet Engineering Task Force.

Formal methods tools that provide mathematical proof of system properties have improved dramatically in their power and capabilities. As part of DARPA's Cyber Assured Systems Engineering (CASE) program, our team has developed a model-based systems engineering environment called BriefCASE that integrates formal methods at all levels of system design, including the ability to build systems targeting seL4. We will present an overview of the CASE project and the capabilities of the BriefCASE tools. We will also describe an application of the BriefCASE tools and workflow to the mission computing system in a military helicopter.

Remote attestation is a process where one digital system gathers and provides evidence of its state and/or identity to an external system. The external system appraises the attestation evidence to make judgments over the attesting system. For this process to be successful, the appraiser must find the attestation evidence to be convincingly trustworthy. Remote attestation is difficult to make trustworthy due to the appraiser’s limited access to the attestation target. In contrast to local attestation, the appraising system is unable to directly observe and oversee the attestation target. In this work, we present a system architecture design and prototype implementation that we claim enables trustworthy remote attestation.

This architecture defines a layered system consisting of seL4 and a Linux virtual machine contained therein. Existing Linux systems may easily be run within the virtual machine, and augmented by coordinated attestation components running both at the Linux and seL4 level. We argue that this layered design offers both the flexibility to accommodate existing systems as wells as rigorous and trustworthy attestation capabilities.

Even though seL4 promises that our resources are isolated, how can we know those resources are enough to fuel our applications? FerrOS is an approach to answering that question by using Rust's type system to layer resource management abstractions on top of seL4 primitives. This talk covers the productivity advantages of teaching a compiler to check that the right kinds of capabilities are in the right places, the tradeoffs between rigid and fluid modes of development, and the branching future paths for Rust with seL4.

A few important criteria have to be satisfied for a piece of software system before becoming ASIL-D certified, two of those are MISRA coding standard and Code Coverage.

First, MISRA is an important coding standard for automotive industry. Making seL4 source code MISRA compliant is a key point to boost the adoption of seL4 in automotive industry. In this talk, we’ll present a joint work from us and our partners, how to make seL4 code MISRA compliant, who has chosen seL4 as the fundamental kernel for their OS product. We’ll discuss typical implementation issues which don’t follow MISRA guidance, the fixes and impacts on proofs.

Second, Code Coverage has been an important metric to measure the code quality in automotive industry. Although seL4 is a formally proven, Code Coverage is still important for two reasons. One is Code Coverage can work orthogonally with formal proof to assure the code quality. The other is Code Coverage rate is key metric in many certifications. We’d like to share our work regarding measure seL4 kernel code coverage. We will present the measuring results and ways we have tried to improve code coverage rate.

We are very fortunate to welcome four leaders at major funding agencies to participate in a session Funding agencies: priorities and vision. They will each give their views on the priorities and vision of their agency in terms of high-assurance systems.

DARPA

William “Brad” Martin

The Defense Advanced Research Projects Agency (DARPA), established in 1958, is an agency within the Department of Defense (DOD) responsible for catalyzing the development of technologies that maintain and advance the capabilities and technical superiority of the U.S. military.

William Martin currently serves as a program manager in the Information Innovation Office at DARPA. He joined DARPA from the National Security Agency (NSA), where he served in a variety of roles, most recently as acting technical director and cybersecurity subject matter expert of the Laboratory for Advanced Cybersecurity Research. His research interests include formal methods, domain-specific languages, system analysis, and trustworthy artificial intelligence.

NCSC

Paul Waller

NCSC is the UK national technical authority for cyber security. Part of the UK government, we provide expert leadership and guidance to help make the UK the safest place to live and work online.

Paul has worked in cryptography and hardware security since graduating with a degree in mathematics in 2001. He has represented the NCSC and its predecessor organisation in various standards bodies, including the Trusted Computing Group, Global Platform and FIDO. His current role allows him to spend time with academic and industry partners learning what the future holds for security technology, and also to help user communities take advantage of new features. Outside of work Paul likes to cycle up small hills in summer, and ski down bigger ones in winter.

Cyberagentur

Sebastian Jester

The Agentur für Innovation in der Cybersicherheit (Cyberagentur) funds high-risk research and development projects with a high disruptive potential in the field of cybersecurity. The Cyberagentur’s goal is to advance internal and external security and technological sovereignty. It was created in 2020 by the German Federal Government and is funded by the Federal Ministry of Defence and the Federal Ministry of the Interior and Home Affairs.

Sebastian Jester is Head of Secure Hardware and Supply Chains at the Agentur für Innovation in der Cybersicherheit, which he joined in June 2022. Previously, he was at Germany’s Federal Ministry of Education and Research, latterly responsible for microelectronics R&D policy at the national and EU level. He holds a doctorate in astronomy from the University of Heidelberg and a Master of Physics from the University of Oxford.

TII

Dr. Shreekant (Ticky) Thakkar

Technology Innovation Institute (TII) is pioneering global research institute that focuses on applied research and a new-age technology capabilities. The institute has seven initial dedicated research centers in Secure Systems, Quantum, Autonomous Robotics, Cryptography, Advanced Materials, Digital Security and Directed Energy.

TII advances research rapidly through a defined research roadmap, approved research funding and state-of-the-art-facilities. By working with an exceptional talent, universities, research institutions and industry partners from all over the world, the institute connects an intellectual community and contributes to building an R&D ecosystem in Abu Dhabi and the UAE. The institute pursues the development of breakthrough technologies that have practical use-cases and global impact. Technology Innovation Institute also reinforces Abu Dhabi and the UAE’s status as hub for innovation and contributes to the broader development of the knowledge-based economy.

Dr Shreekant (Ticky) Thakkar is Chief Research Officer at the Secure Systems Research Centre at the Technology Innovation Institute (TII), a cutting-edge UAE-based scientific research Centre and Adjunct Research Professor at Khalifa University. In this role, he is responsible for carrying out advanced research that is driving end-to-end security and resilience in cyber physical and autonomous systems of systems (swarm of drones). These includes secure technologies in silicon, edge and mobile and cloud platforms working with open-source ecosystems (Dronecode, RISC-V, Linux, Apache, ROS) and research institutions across USA, Europe, and UAE.

Gernot will start the day by providing background on seL4 and its philosophy. Specifically he will talk about the principles that drive seL4’s design and abstractions. Given the low-level nature of seL4’s abstractions and mechanisms, and the deliberate policy-freedom, it is not always clear what constitutes “proper use”. Gernot will highlight some of the do’s and don’ts that developers should keep in mind to produce good designs. He will link this back to earlier presentations on user-level frameworks and how they support proper use.

seL4 is commonly referred to as "the most verified microkernel". While this statement is true, the notion of being “verified” requires careful handling to ensure appropriate expectations and valid claims. seL4’s verification is its key differentiator. Inappropriate claims will damage its reputation and could have serious consequences in real systems.

Not all seL4 configurations and features are verified, and not all “verified” configurations are verified to the same degree. While we should celebrate and promote the high-assurance that seL4 and seL4-based systems provide, it is important to ensure understanding of what exactly is proved, as well as the conditions under which the proofs hold and what they imply in practice. Such precision is also important and necessary to allow a suitable comparison with other alternative solutions.

In this talk we will give a brief overview of what seL4 verification claims can be made and what they mean, and which claims should not be made.

The seL4 foundation manages a collection of over 55 repositories in the seL4 GitHub organisation.

This talk gives an overview of the Continuous Integration (CI) setup for this collection, how the repositories are kept consistent with each other, and how we can tell after a change whether things are still working or not.

The centre of this collection is the seL4 kernel repository itself. Its test suite includes running the formal verification of the kernel, as well as static compilation checks for all supported hardware platforms, simulation runs for all architectures, automated tests on hardware for most of the supported platforms, running benchmarks, documentation builds, etc. Both, formal verification and runtime tests are necessary – formal verification is good at showing the absence of bad behaviours, tests are good at showing the presence of good behaviours. They are also useful for validating assumptions of the formal verification. Test runs leave behind log files and build artefacts such as compiled kernel binaries or sel4tests binaries that can be simulated or run on hardware. Successful test runs automatically record the constellation of repositories that were involved in that successful run, so developers can easily trace and access known working combinations. The talk will also give an overview on how you can contribute tests, how you can help to improve the CI infrastructure, and how you can run most of these tests locally yourself.

The lifeblood of open-source projects are the contributors, developers, and maintainers that work to keep the projects up to date, add new features, and squash bugs. However, there can be quite a few roadblocks that prevent or slow down upstreaming of code. This will be an account of the seL4 mainlining experiences of DornerWorks. This talk will encompass our successes, difficulties, possible improvements, and some open questions. This will be a short talk with a lot of time for open discussion. The goal is to spark a conversation that will lead to even greater collaboration than is seen today.

Using seL4 in complex production environments brings new challenges often quite different from research-oriented environments. At a high level, there are gaps in the seL4 stack, specifically the VMM, userspace, and tooling, which complicate matters for integrators attempting to meet real-world customer use cases. Not all business opportunities require a solution using a VM architecture, but those that do quickly become complex and would benefit enormously from an established standard or reference baseline. The lack of a robust and consistent VMM for seL4 has created a highly fractured environment. Most integrators have their own specialized customer use cases, and they have found that the quickest path is to use a forked and modified VMM. This practice may have short-term benefits to that integrator. Still, it does not allow the community to benefit from commonality and guarantees that the fork will get old and out of sync with the mainline.

This talk proposes to establish a driving philosophy to design a baseline VMM rather than prescribe a specific system architecture. We intend to discuss the possible missing features of the existing seL4 VMM concerning standardization, more so than a prescription for the right way to do it. Indeed, this will entail recommending high-level architecture patterns but cannot lock an adopter into specific implementations. Each adopting integrator will inevitably start from the new standard and refine the implementation for their use case. The effort here is to close the gap between the current VMM baseline and the point of necessary deviation.

While seL4 is an amazing technology, it is difficult to develop and build applications from scratch. Even when using virtualization, the development process for OS applications is a long loop of write, build, deploy, test, fix, build, deploy, test, etc. One way to improve on this is to borrow from the server world and support containers in VMs running on seL4. This improves embedded DevOps by allowing developers to test various container applications together on their host target, thereby reducing the number of required deployments. We will be discussing what work we have already done in this space as well as some thoughts on where to take it in the future. This will be a short talk followed by open discussion to explore issues and interests.

Since the winter term 2020, the practical course "seL4 & TRENTOS" offers students at the TUM an introduction into the fundamental aspects of TRENTOS, a novel secure embedded operating system developed by HENSOLDT Cyber, which is built on top of the seL4 microkernel and the CAmkES framework. The course starts with a respective theory phase, in which students get to know the basic building blocks of both kernel and user space. Afterwards, the course participants work within teams on an individual practical project. They hereby apply a TRENTOS-based setup, running on top of the the Raspberry Pi platform, to a selected real-world use case (e.g. originating from the domains automotive or industrial automation). Besides providing a general course overview, this talk shall therefore demonstrate respective course results and serve as a starting point for follow-up discussions.

A secure kernel is more and more attractive these days and seL4 is one of the strongest microkernels around. However, the seL4 ecosystem is still maturing and may not be a drop-in replacement for practical applications in real-world systems. With the strictest security needs, it is probably best to use just the microkernel with user-space applications. However, there are many stacks, libraries, and drivers lacking to meet the needs of most systems. Virtualization and the user-space VMM provide an answer to this. For developers new to the seL4 ecosystem, it is difficult to configure the software to meet system requirements. The traditional approach is to start with a known working configuration and tweak it until it fits the specific application. The latest approach is to use DornerWorks’ VM Composer, a graphical, drag-and-drop interface which allows one to easily configure their seL4-based, virtualized systems without needing to modify any CMake, CAmkES, python, or C files. This short, teaser talk will introduce the features and platforms that are supported in VM Composer.

The seL4 Foundation is home to the ecosystem of software, developers and adopters for safety- and security-critical systems based on seL4. It was formed in April 2020 as a neutral and community-based organisation that ensures long-term, independent support for seL4 and its ecosystem, and fosters strong community participation and ownership in the ecosystem. It raises funds for continuing and accelerating development, facilitates interoperability, standardisation and sharing of cost for the benefit of all. Its aim is to ensure that seL4 is not only the world’s best secure operating-system technology, but is readily deployable and supported by a diverse and stable ecosystem of services and products.

In this talk I will give an brief update on the Foundation's successes in increased contributions, increased support, and increased membership, as well as the vision to keep supporting a thriving seL4 ecosystem.