seL4 Summit 2023

Scoping assurance activities with seL4

Keynote

Presented by Gage B, NCSC

In both the safety and security industries, high levels of product assurance are sought to mitigate the risk of product failure. Often this means that software developers need to demonstrate that all functions do what they are supposed to do, the product does not do anything it is not supposed to do, and that the product is free from all known bugs and vulnerabilities.

Whilst none of these requirements have trivial solutions, testing does a reasonable job of checking the correctness of functions. Similarly, taking advantage of tooling (such as static analysis, dynamic analysis), tracking the discovery of bugs and vulnerabilities, and having a refined software patching process helps to mitigate the presence of bugs and vulnerabilities. However, it is much less obvious how one can gain confidence that the software has no unintended functionality without checking the entire software implementation. Even then, the scope of what you need to check is potentially unbounded (we’re looking for the unknown unknowns after all), issues will still be missed, and the resource requirements are high.

In this talk, I will describe how basing a software product on seL4 facilitates the scoping of this no unintended functionality problem, and in turn, reduces the amount of effort required when it comes to demonstrating assurance of a security product. By walking through an example, we’ll observe the assurance benefits of component isolation, data flow control, how seL4 helps to direct where we should focus our assurance efforts, and any caveats we should be aware of.

Accepting that the assurance effort should be commensurate with the criticality of the security product, my hope is that this presentation provides a sliding scale of seL4 features we should seek to take advantage of, be it for articulating an assurance case, or conducting an independent assessment.

Dynamic seL4 based systems: designing for verifiability

Talk

Presented by Matthew Brecknell, Kry10

The current state of the art in seL4-based system design is to statically partition system resources into unprivileged components. Components may synchronise and communicate with each other, but otherwise only have rights to their own resources. For such static systems, the seL4 security theorems guarantee that seL4 correctly enforces access controls, and does not allow any component to gain new rights. The main benefit of this approach is that it automatically gives strong guarantees about component isolation, without further verification effort, and these can be used to support arguments about fault tolerance and security.

However, some things are not possible in static systems. For Kry10, over-the-air software and configuration updates are important. Updates should minimise disruption to the system, and may therefore need to co-ordinate with running components. For example, a server may gain new clients, and an allocation of extra memory it can use to serve them.

Support for dynamic features like updates adds significant complexity. Dynamic systems must include some privileged components that retain authority to resources used by other components, so isolation guarantees are no longer free. Privileged components should be verified, so we need a way to reason about user-level components, and their interactions with each other and the kernel.

This talk will report on our initial work on this challenge. We'll discuss our approach to system design, which uses a strict hierarchy of control to ensure that supervisors have complete oversight of their subsystems, and can enforce protocols for resource delegation and revocation. We'll look at our work-in-progress supervisor API design, whose distinguishing feature is the ability to apply complex configuration updates with all-or-nothing semantics. And finally, we'll speculate on how we might eventually back this up with formal guarantees.

Formally Stepping Into The Unverified World

Talk

Presented by Sandy Frost, Los Alamos National Laboratory

With the rise in high profile attacks against safety and security critical systems, formal methods are being considered as a defensive option across many domains, such as with critical infrastructure, since they can prove that software behaves exactly according to specification, therefore minimizing software vulnerabilities. Unfortunately, there has been slow adoption of this technology due to technical (e.g., performance limitation of verification tools) and non-technical (e.g., unfamiliarity with concepts, difficult to implement) reasons. We propose an analysis of the interface between formally (checking software against specifications) and non-formally verified components, to better understand the impacts to system robustness. This work has the potential to be transformational by enabling wider adoption of this defensive measure.

We are analyzing system interaction impacts between components that are formally verified and those that are not using a e.g., seL4-provided channel with approved access control. The seL4 microkernel, which is the minimal core of an operating system provides strong isolation. To allow communication between components, seL4 must enable fine-grained access control, which is an explicitly enabled communication channel for a desired operation.

This talk is relevant to the seL4 scope because it covers an seL4 experience report relevant to developing capabilities toward “building a business case for using a verified kernel”. In order to use a verified kernel, especially with critical components, it is important to know its potential limitations and special considerations, therefore exploring the kernel’s interactions with components that might not be verified is paramount.

Reducing the reliance on verification experts for seL4 proofs

Talk

Presented by Gerwin Klein, Proofcraft

The seL4 microkernel is the world’s most highly assured OS kernel. Keeping this claim true is hard work. The formal verification journey of the seL4 microkernel is nearing two decades, and still has a busy roadmap for the years ahead. It started as a research project aiming for a highly challenging problem with the potential of significant impact. Today, the seL4 proofs represent more than a million lines of formal proofs that have been continuously maintained over a system that has evolved considerably, with significant new features being added in response to increased interest and adoption from numerous sectors.

This unique maintenance of a formally verified, evolving software system is one of the largest examples in the emerging discipline of proof engineering: the art of systematic treatment, management and estimation of large-scale proofs. Proofcraft is constantly developing and refining proof engineering techniques to manage what is probably the world’s largest continually maintained formal proof artefact.

Importantly, and perhaps paradoxically, proof engineering aims at reducing the reliance on verification experts, in this case through techniques improving the genericity and automation of the seL4 proofs. In this talk we will present the challenges one encounters while maintaining such a large proof base, along with some of Proofcraft’s existing and planned techniques to make seL4 proofs more agile and friendly to change, more robust against predictable change, and less dependent on experts for updates.

For instance, the current seL4 invariant proofs are split into a generic architecture- independent part and an architecture-dependent part. This allows significantly speed up in development of proofs for new features, as well as reduction of the proof update bur- den on code changes. We plan to improve this architecture split and apply it to other large proof artefacts in seL4. Another example is our plan to almost completely automate the verification of platform ports within existing verified architectures of the seL4 kernel. Currently, porting seL4 to a new platform involves determining which architecture the platform runs on, for instance Arm v7, Intel x64, or RISC-V 64, determining which devices are included, at which memory addresses they reside, etc. These lead to configuration parameters for the kernel and the definition of a set of constants. Instead of requiring the involvement of experts, we can develop proof automation that shows these interface relationships are satisfied by a concrete platform configuration, greatly reducing the verification overhead of porting to a new platform.

More multiprocessing on seL4: Are efficient SMP virtual machines possible on verifiable seL4 kernels?

Talk

Presented by Kent McLeod, Kry10

Multicore systems with verified seL4 is just around the corner with multikernels - kernel state is isolated on each core and avoid kernel-mode concurrency for easier verification. Does this mean that it's not possible to support multicore at user level? Let's find out by investigating whether it's possible to efficiently support virtualizing SMP virtual machines with small core counts using our multikernel mechanisms.

This talk will detail how to construct such a system, the work involved and examples of how it can be used.

System Information Flow Analysis

Talk

Presented by Ihor Kuz, Kry10

Most seL4 systems are multi-server systems - consisting of numerous user-level components that communicate amongst each other. These systems often rely on isolation and restricted communication between components to provide assurance about security and safety properties while minimising the trust put into individual components. For such assurance it is usually necessary to analyse the information and control flow in the systems in order to get an understanding of the isolation (or protection) domains and how the system could behave at runtime. This is something that we are interested in doing for the seL4-based Kry10 OS as well.

There has been past work looking at analysing static seL4-based systems for various information flow properties, but Kry10 OS is a more dynamic system. This presentation will discuss the problem space of analysing information and control flow in multi-server systems and present options and solutions (both formal and informal) for doing this for static and dynamic seL4-based systems. We will also discuss how such analyses contribute to overall system assurance cases and how they relate to kernel and user-level component proofs.

Advancements for Virtualization Support in seL4:CAmkES and seL4cp

Talk

Presented by Markku Ahvenjärvi, TII

Virtualization enables multiple virtual machines (VMs) to operate on a single physical machine, each with its own operating system, applications, and data, while sharing the underlying physical resources of the host machine. seL4 is a microkernel-based operating system that provides a high-assurance, secure, and efficient platform for the deployment of critical systems. It can be utilized as a hypervisor, providing a minimal and scalable infrastructure for virtualized environments, making it well-suited for use in embedded and real-time systems and high-assurance security-critical systems that require virtualization.

Our previous talk at the seL4 Summit 2022 presented our architecture on VirtIO-based Virtualization with seL4 Hypervisor and QEMU. We demonstrated how our approach provides VirtIO standard support to devices on top of the seL4 hypervisor using QEMU to provide the VirtIO device backends for the guest VMs. Our approach offered support for practically all VirtIO-device backends with a minimal amount of source code, providing accelerated graphics and proper file system support.

In this talk at the seL4 Summit 2023, we will show the evolution of our architecture compared to the one presented last year, as well as current efforts that we have been working on regarding virtualization support. We aim to discuss the adaptation and integration of our "VirtIO backend" implementation work from the CAmkES environment to the seL4 Core Platform (seL4cp). We will emphasize how the underlying concepts and principles are orthogonal to the choice between CAmkES and seL4cp, demonstrating the seamless transition of key elements such as CAmkES dataports to seL4cp shared memory regions. Our objective is to showcase the versatility and applicability of this virtualization approach, highlighting its value for rapid prototyping in both CAmkES and seL4cp environments. By presenting our work in this manner, we aim to encourage the adoption of this robust virtualization solution, empowering developers to efficiently prototype and deploy secure embedded systems, irrespective of their chosen platform.

Our approach provides a flexible and scalable solution for critical systems, addressing the limitations of existing solutions while building on the foundation of our previous work. Our talk will provide an overview of the implementation details, performance improvements, and future directions for the technology, highlighting the benefits of using the seL4 hypervisor for virtualized environments.

The seL4 Device Driver Framework

Talk

Presented by Lucy Parker, UNSW

A lack of a good approach to I/O is one of the primary barriers to uptake for seL4. Unfortunately, there’s a distinct lack of guidance, along with too many poor performing solutions that don’t make good use of seL4. We believe a thoughtful design can, and should, demonstrate performance competitive with Linux. We present such a design in the seL4 Device Driver framework (sDDF). Its simple design prioritises a strong separation of concerns by using multiple isolated components, each with a single task in the pipeline, that communicate via a low-overhead, asynchronous transport layer. It’s presently focused on networking systems, and comparison against Linux already shows that simplicity wins. This talk will revisit the design of the sDDF, and discuss ongoing work to further evaluate and optimise the framework for device sharing.

R&D Update from TS

Talk

Presented by Gernot Heiser, UNSW

I will given an overview of seL4-related research and development at Trustworthy Systems.

At the core of our present work is the design and implementation of a new OS personality for IoT/embedded/cyberphysical systems that is based on the KISS principle – keep it simple, stupid! We take simplicity to the extreme, with fine-grained modularity driven by strict separation of concerns, resulting in extremely simple modules, most just comprising a few hundred lines of code. This is possible by abandoning the 1980's model of an OS, implemented by almost all contemporary OS designs, that strives to provide general (and thus inherently complex) policies. Our approach is the opposite: extremely use-case-specific policies, that are simple to implement, and trivial to replace. Our experience with networking (see the preceding talk by Lucy) shows that this approach is not only feasible, it can also be highly performant.

Highly aligned to the above is our work on the use of push-button verification of OS components. We have demonstrated that we can verify the implementation of the seL4 Core Platform this way: Once a suitable specification is created, the SMT solver provides the proof without further manual action. We have furthermore created an automated translation-validation toolchain, using a similar apporach as for the binary verification of seL4, that proves the correctness of a mapping of the seL4CP system specification (SDF) to the CapDL formalism that describes low-level access rights in an seL4 system (and that can produce a verified system initialiser).

Our experience with verifying seL4CP makes us confident that we can verify (at least) core components of our new KISS-based OS using the same push-button approach. This creates the exciting prospect that in the near future we will have an OS that is not only easy to use, yet high performant, but also at least partially verified.

Our third major activity is Pancake, our new systems language aimed at easing verification of OS components, especially device drivers. Pancake has a verified compiler, meaning that correctness proofs can be based on the semantics of Pancake rather than dealing with the complexities of C. We have already used Pancake to implement some components of the networking system, although significant work remains to be done.

I will finally give an update on our work on verified Time Protection, the principled prevention of microarchitectural timing channels, as wel as the SMOS project, which is designing a fully dynamic, general-purpose OS that can be proved to enforce a security policy.

seL4: Experiences, Improvements and Optimizations

Talk

Presented by Chris Guikema, DornerWorks

Sandboxing legacy code provides a low barrier approach for developers to start implementing systems in the seL4 ecosystem. However, these legacy applications often need to communicate with each other to function properly. seL4 provides a means of communication between virtual machines via a software implementation of an ethernet device called virtio-net, which currently suffers from performance and stability problems. These performance and stability issues present a barrier to adoption of seL4 for multiple markets. DornerWorks will present an overview of the seL4 virtio-net implementation, the challenges using it, how DornerWorks improved it in the mainline, and performance benchmarks which include our IP solution to increase performance by a factor of 40.

From Zero to a Native xHCl Driver

Talk

Presented by Josh Felmeden, Capgemini Engineering

At the 2022 seL4 summit, our colleagues presented a framework allowing u-boot drivers to be used in seL4. This submission presents follow on work, with the goal of improving seL4 USB support. Specifically, by writing a native xHCI driver and stack for use in seL4.

We use the Avnet MaaXBoard as our development board although our intention is to make the driver easily portable to other platforms. Our approach has been to port an existing xHCI USB stack from the NetBSD operating system into the Microkit framework, changing as little code as possible.

We also present an experience report detailing our development with seL4 as a team who had no prior experience with it.

Crashing For Reliability

Talk

Presented by Ihor Kuz, Kry10

A reliable OS needs to make sure that it, and the software that runs on it, keeps running and is always available.

Ideally software would never fail, so reliability would be easy. But even if your software is perfect, there are always hardware problems, or problems when interacting with other software. Also software isn’t perfect (even if it’s formally verified) so we have to deal with inevitable failure.

One approach to dealing with failure is to let software crash, but monitor it and restart it when it does crash. This allows the system to control (and importantly - recover from) the failures. Erlang OTP-based systems take this approach, and it has worked extremely well for building highly reliable long-running systems.

We’ve applied this “let it crash” approach in the sel4-based Kry10 OS. In this presentation we will dive into our use of this approach, describe the challenges of applying it in Kry10 OS (such as resource recovery, dependency managements, re-initialisation of resources, etc), explain why seL4 provides all the right features for applying this approach at the system level, and give examples of how it helps to achieve reliability.

Building a Platform for Critical Devices in the “Real World”

Gold Sponsor Talk

Presented by Boyd Multerer, Kry10

Boyd Multerer, Founder and CEO of Kry10 will talk about the role of seL4 as a one of the critical ingredients for addressing the “real world” requirements and high level of assurance required by their critical systems. Boyd will talk about the importance of the continued innovation around seL4 and the additional platform services platform work Kry10 is doing to need to deliver addition of seL4 and the new work underway as a key ingredient to any broader platform for critical systems and the importance of new investments done and the critical role that seL4 plays as Boyd will emphasize role of seL4 and the Kry10 Platform. Hear about the design principles of the KRy10 Platform Kry10 Platform that caters to the real-world demands of critical systems. Don't miss this opportunity to learn about the exciting advancements in seL4 and the Kry10 Platform and its potential to support the real-world challenges faced by critical systems.

CantripOS: An OS for Ambient ML Applications

Keynote

Presented by Sam Leffler, Google

CantripOS is an open source operating system purpose-built to run ML workloads for embedded systems. It is being developed as part of Google’s project Sparrow, whose charter is to build a low-power embedded platform for ML applications with a focus on security and privacy. CantripOS is built in the Rust programming language1, runs under the seL4 microkernel2, and uses a modified CAmkES framework3. This allows CantripOS to run dynamically loaded applications in a controlled sandbox, while still retaining the benefits of a statically designed system. This paper describes the system design, modifications made to seL4 and CAmkES, and future directions. All the work described here is publicly available on GitHub4.

Magnetite: Rust-Based OS Services for seL4

Talk

Presented by Juliana Furgala, MIT Lincoln Laboratory

What if the isolation that seL4 provides could be applied at a fine-grained level to individual processes? Frequently seL4 is used as a hypervisor but at MIT Lincoln Laboratory, we explored the potential of seL4 as a foundational block in a new security-focused operating system. Magnetite is a suite of performant, secure-by-design, real-time OS services built upon the formally-verified microkernel seL4 and written in Rust, a memory-safe language. Magnetite offers a feature-rich API for both legacy C and new Rust applications to engage with its variety of resource types, which extend seL4’s capability-based system to provide common OS services. Magnetite is built upon the Principle of Least Privilege (PoLP) to limit trust and time of trust, and also adheres to strong isolation properties with self-contained processes and system services, and isolated domains known as silos.

Showcase: Microkernel OS, TPMs, and WASM in Ilo T Environments

Talk

Presented by Sid Hussmann, Gapfruit

This talk will demonstrate how Gapfruit OS [0], an operating system built with the Genode Framework [1], can be deployed for edge computing in industrial IoT environments. Genode is an operating system framework that supports seL4.

When it comes to systems engineering, we live in exciting times. On the one hand, we have projects, such as seL4 and Genode, that push the boundaries for a solid computing foundation from the bottom up. On the other hand, Zero-Trust principles move the industry to combine public-key infrastructures with TPM-backed device identities. Third, we can witness a trend from the cloud natives that tries to free us from much of the complex legacy code bases on the application layer with new runtimes such as WebAssembly/WASI.

I present Gapfruit's journey of deploying WASM code to a microkernel OS with capability-based security. I will explain how we chose the Genode Framework for our products and how we utilize it to port libraries such as tpm2-tss [2] and WasmEdge [3].

I will then showcase a live demo demonstrating the zero-touch provisioning capabilities of an IoT gateway running Gapfruit OS. The demo will show how the device boots and connects to its digital twin on Azure [4] with TPM-backed credentials and how the desired-state configuration of its digital twin triggers the deployment of a WebAssembly application with WasmEdge to the device.

[0] https://gapfruit.com

[1] https://github.com/genodelabs/genode

[2] https://github.com/tpm2-software/tpm2-tss

[3] https://github.com/WasmEdge/WasmEdge

[4] https://azure.microsoft.com/en-us/products/iot-hub

Rust support in seL4 userspace: update and roadmap

Talk

Presented by Nick Spinale, Colias Group

The Rust programming language and ecosystem provide memory safety and enhance developer productivity even at lower levels of the software stack. This talk outlines our efforts, funded by the seL4 Foundation, to apply Rust to seL4 userspace and facilitate its use in the seL4 software ecosystem. This talk will cover new bodies of Rust code related to libsel4, the seL4 Core Platform, and CapDL; information about how to integrate, extend, and contribute to this work; and our vision and roadmap moving forward.

The seL4 Microkit

Talk

Presented by Ivan Velickovic, UNSW

The seL4 Microkit is an operating system framework on top of seL4 that aims to provide minimal abstractions to make it easier to build statically structured systems on seL4, while still leveraging the kernel’s benefits of security and performance. Since the 2022 seL4 Summit, seL4CP has become more mature and is seeing wider use. At Trustworthy Systems, seL4CP is the basis of much of our work, including the seL4 Device Driver Framework and other OS services such as a virtual machine monitor. The goal of this talk is to give you an understanding of seL4CP and surrounding developments by covering three topics:

• An introduction to seL4CP and its concepts, and how they map onto seL4 primitives.
• How the seL4CP has progressed over the past year and how it can now be used to create more complex systems.
• An update on the verification story of seL4CP, which includes the functional correctness of the seL4CP library and runtime code as well as the verified mapping from seL4CP system description to CapDL.

Leveraging Rust for Core Platform

Talk

Presented by Ben Hamlin, Galois

A natural way to perform hardware abstraction in SeL4 is to create a dedicated driver component. Writing such hardware driver components in SeL4 Core Platform for Rust is currently a manual process. Assuming a Rust library to perform register manipulation, etc. already exists (say, as an implementation of embedded-hal traits), it is still necessary to:

1. Design an RPC protocol that clients will use to access the hardware driver;

2. Implement the driver-side protocol;

3. Implement the client-side protocol, adapting any libraries already written to interface with the hardware drivers to use this RPC protocol instead.

This talk describes a way to use traits from HAL crates, such as embedded-hal to make the code implementing these protocols easily reusable. As an added benefit our approach allows code reuse in two more ways: Existing implementations of HAL traits for specific hardware can be turned into dedicated Core Platform components with a minimum of additional boilerplate; and hardware-agnostic libraries written on top of embedded-hal traits can be used in client components without writing adapters. This approach is suitable for interactions with a networking stack (smoltcp) and other devices such as UART, and can be extended to other peripherals (timers, SPI, I2C). Our approach should make running Core Platform on various devices more straightforward.

We will present conclusions and examples developed as part of this work.

OS on seL4: so many options!

Panel

Gernot Heiser, Leader, Trustworthy Systems at UNSW Sydney

Chairman, seL4 Foundation

Sid Hussmann, CTO, Gapfruit

In my first job as an industrial automation engineer, I loved how disciplines came together: Electronics, mechanics, programming, and robotics - like Lego, using building blocks to create something new.

After my studies in Electrical Engineering and Computer Science, I worked for three years in research of HW/SW co-design for IoT systems. Since 2011, I have been in the defense security industry, first as a firmware engineer and later as a lead systems architect.

I was responsible for a framework for various security products: 100G link encryption, VPN, VoIP, and secure radio communication. I was also part of a team that developed a secure notebook for governmental agencies, including a new operating system for highly classified information.

In 2018 I co-founded Gapfruit to bring academic security research to real-world products.

I still love to create.

Kent McLeod, KOS engineering lead, Kry10

Kent is an operating-systems engineer specialized in formally verifiable trustworthy systems using seL4. His interests include systems engineering and how using different operating system architectures can help construct trustworthy applications.

His work at Kry10 is focused on designing and developing the new Kry10 secure platform which includes a new device operating system, KOS, that leverages seL4 and the BEAM to make it easier to build and maintain embedded software that still needs to be secure and robust even if it’s connected to the internet. He previously worked at the Trustworthy Systems Research Group where he helped oversee the technical development of seL4 as an OS engineer. He is currently a member of the seL4 Foundation’s technical steering committee.

Juliana Furgala, Cybersecurity Researcher, MIT Lincoln Laboratory

Juliana Furgala is an associate technical staff member in the Secure Resilient Systems and Technology Group. Currently she is researching secure and recoverable satellite systems. Interested in the pursuit of technology built with security in mind, she aims to develop lasting technology that can stand the test of adversaries, not just the test of time. Her recently published research focuses on the needs of embedded and real-time systems, specifically related to operating system development.

To lower the barrier of entry into STEM fields, she is involved in a variety of academic and outreach efforts. One such activity was founding LL EduCATE, a volunteer group that develops accessible, hands-on courses to introduce middle and high school students to the possibilities of STEM. The first course, an Introduction to Engineering Concepts was created for both independent student study and collaborations with educators.

Juliana received her BS degree in computer science in 2019 from Tufts University. She is currently pursuing an MS degree in cybersecurity at Georgia Institute of Technology.

Moderator

Todd Carpenter, Principal Scientist, Galois, Inc

Todd's research is focused on tools and techniques to develop safe, secure, real-time, and dependable systems built on solid foundations. He has designed and specified system architectures, hardware, and software, and has developed tools, standards, and processes for enhancing design flows.

Galois develops technology to guarantee the trustworthiness of systems where failure is unacceptable. We apply cutting edge computer science and mathematics to advance the state of the art in software and hardware trustworthiness.

seL4 VMM on the RISC-V Rocket Chip

Talk

Presented by Robbie VanVossen, DornerWorks

The royalty-free, open-source RISC-V is an ideal ISA for the high-assurance seL4 microkernel since the formal proof requires definitive understanding of its underlying architecture. DornerWorks’ use-case generally utilizes virtualization with seL4 to provide a secure platform which allows for cyber-retrofit, rapid deployment, and cyber resilience. Virtualization is an area where RISC-V is immature. The hypervisor (H) extension has been ratified, but there are still no commercially available silicon processors that support the extension. The Rocket Chip is a soft-core RISC-V implementation which can be instantiated on an FPGA and is essentially equivalent to a real silicon processor. DornerWorks bridged the gap between the seL4 VMM running on QEMU and running on actual silicon by getting a seL4 VMM running, for the first time, on a Rocket Chip instantiation which has the hypervisor extensions implemented. This presentation will provide an overview of the Rocket Chip, the RISC-V H extension, the effort that went into getting the seL4 VMM to run on Rocket Chip, and thoughts on the next steps for seL4 virtualization on RISC-V platforms.

seL4 on Arm Morello

Talk

Presented by Martin Atkins, Mission Critical Applications

seL4 has a formally-proven kernel, but the safe and secure operation of a system built on seL4 depends on the correct operation of the user-level tasks that implement the system policies, services, and device drivers needed by the application, as well as on the correct operation of the application tasks. Running an seL4 system on a processor with CHERI extensions brings the extra assurance of the capability architecture to these user-level tasks, and thus increases the assurance of the overall application.

Our project builds on initial work done at Arm Research to port the seL4 kernel to the Arm Morello CHERI processor. The project aims to support a mixture of user-level tasks compiled as Hybrid code (that is, where capabilities are explicitly defined in the source code), and PureCap code (that is, where all pointers are dereferenced as capabilities). The seL4 user-level libraries must be ported to support these compilation options. SeL4 virtual machines will also be extended to support capability-aware operating systems, such as CheriBSD4, Morello Android5, and Morello Linux6.

This paper will report on the progress of the project, and discuss the requirements and design options for the communication of CHERI capabilities between seL4 tasks, and the implications this has on the seL4 IPC mechanisms.

Incremental assurance for a Rust network stack

Talk

Presented by Michal Podhradsky, Galois

Despite the fact that numerous components and subsystems have been developed on top of or with seL4 over the past few years, sponsored mainly by DoD SBIR grants, seL4 does not have a high-assurance network stack. In earlier work on the HACMS project, Galois integrated an off-the-shelf TCP stack into a seL4 platform. Many other organizations have done something similar, either by shiming in existing low-assurance network code that has poor provenance and no rigorous assurance, or by using the Linux environment to provide networking features. To the best of our knowledge, there is currently no high assurance network stack readily available for embedded systems.

To mitigate this gap, we started with an existing and widely used Rust network stack smoltcp and are providing an incremental assurance, that is by no means complete, but provides a path towards a high assurance stack in the future.

This summer, we used Prognosis framework, offering automated closed-box learning and analysis of models of network protocol implementations, for model based veritication of TCP protocol in smoltcp, and Kani Rust verifier to verify TCP protocol logic and packet format correctness via symbolic execution. We have found protocol violations or misimplementations in the library, and have been working with the smoltcp developers to mitigate these violations. Furthermore, we integrated Continuous Verification suite with the smoltcp library, to automatically validate the code after each commit.

IOMMU (take the ARM SMMUv3 for instance) solution for seL4

Talk

Presented by Lei Mao, Horizon Robotics

The IOMMU Stage-2 only scheme (the view of IOMMU Stage-2 is as same as the MMU's) is simple, and seems good at most of time, but in order to go further for a more unrestricted and finely controlled Stage-1, we can apply the classic virtio scheme for IOMMU. The only extra important thing that needs to be done in virtio-smmu backend is managing relationships between messages in virtqueue and IOMMU or VSpace capabilities.

But what if we use a different page table granularity for SMMU than for MMU? As we know, the IO-mapping request from Guest OS could be as small as one normal page, but seL4 doesn't allow reusing huge or large frames in the same region at the same time. If we already distribute the region into one huge or several large frames, meanwhile, we can not re-segment it into small pages for IO-mapping. Even if leaving capability control aside, we have to use the scheme of Stage1 plus Stage2, and realize Stage1 construction for IO page table which is redundant already exists in VM's OS.

Now we have the complete Components'&VMs' IOMMU SID/CB capability management, derivation, and configuration. And most importantly, a proven IOMMU nested sw approach which has the advantages of both performance, flexibility and reliability, with few restrictions, with minimal effort and minimum changes using existing capability systems.

By hosting the installation/uninstallation of the Stage-1 context root, bring multiple benefits:

1. Not only has finely controlled Stage-1, but also rarely relies on VMM with little restriction and much more flexibility, such as,

• This design can be applied with all modes of SMMU.
• The Linux native SMMU driver keeps all of the original direct operations，so no need to use QEMU or VIRTIO-IOMMU backend driver.

2. We can separate out Guest OS internal IO page management, and keep them the same as the native IOMMU drivers.

3. Not only can native drivers be highly reused, but also the performance is almost the same as without virtualization

Toward a Verified, Minimal IPv6 Network Stack Implementation

Talk

Presented by Wyeth Greenlaw Rollins, Lewis & Clark College

We are completing the implementation of a minimal, pure IPv6 network stack optimized to run on IoT endpoints connected to a network through a Layer 2 Ethernet interface. This implementation supports only the minimal set of protocols (IEEE 802.3, ICMP, IP, and UDP) to provide efficient UDP-based communication between an IoT endpoint and any other host.

We believe our implementation will provide high performance and reliability through a strict application of separation of concerns and elimination of all unnecessary data copies while keeping the codebase amenable to verification.

In this talk, we report on our progress implementing and verifying this networking stack.

OS for Software Defined Vehicle

Gold Sponsor Talk

Presented by Qiyan Wang, NIO

This talk provides a brief introduction of NIO – a global smart EV company, and discusses how automotive industry evolves towards software defined vehicle, and how OS could play a key role in this transition, and shares what NIO’s vision and progress of building a vehicle OS using seL4.

Secure Systems in Focus: Challenges, Solutions, and Future Directions

Gold Sponsor Talk

Presented by Everton de Matos, TII

In today's digital age, when cyber threats are everywhere, the importance of building robust and secure systems cannot be overstated. This presentation dives deep into the initiatives undertaken by the Secure Systems Research Center (SSRC). We'll shed light on our collaborations, projects, and the novel solutions we've pioneered to tackle pressing cyber challenges. The SSRC is a pillar among the ten research centers that comprise the Technology Innovation Institute (TII). Situated in Abu Dhabi, TII aims to lead the way in tech research, focusing on critical areas in the digital world today. In this presentation, we will discuss our latest work and how tools like the seL4 microkernel help make our systems even more secure. By the end of this session, attendees will gain a panoramic view of SSRC's achievements over the past year. We'll also offer a glimpse into the future, outlining our strategic plans and emphasizing SSRC's commitment to pushing the barriers of tech security.

SIG update, Community Update and Discussion

Update and discussion

This session will include a community update from Kent McLeod, Kry10, and SIG updates from Matt Brecknell, Kry10, Yanyan Shen, NIO, and Everton DeMatos, TII. There will also be opportunity for discussion.

Kent McLeod, KOS engineering lead, Kry10

Kent is an operating-systems engineer specialized in formally verifiable trustworthy systems using seL4. His interests include systems engineering and how using different operating system architectures can help construct trustworthy applications.

His work at Kry10 is focused on designing and developing the new Kry10 secure platform which includes a new device operating system, KOS, that leverages seL4 and the BEAM to make it easier to build and maintain embedded software that still needs to be secure and robust even if it’s connected to the internet.

He previously worked at the Trustworthy Systems Research Group where he helped oversee the technical development of seL4 as an OS engineer. He is currently a member of the seL4 Foundation’s technical steering committee.

Matthew Brecknell, Verification Engineer, Kry10

Matthew is a formal verification practitioner. He has made significant contributions to the seL4 verification story, and is a member of the seL4 Foundation Technical Steering Committee. At Kry10, Matthew is developing the next generation of high-assurance remotely-managed seL4-based devices.

Everton de Matos, TII

Everton de Matos serves as Lead Security Research Engineer at the Technology Innovation Institute (TII) within the Secure Systems Research Center (SSRC). He earned his Ph.D. in Computer Science from the Pontifical Catholic University of Rio Grande do Sul (PUCRS). During his doctoral studies, he was honored with a Fulbright scholarship, allowing him to further his research at the University of Southern California (USC). Presently, Everton's focus lies in security for embedded systems, specifically within the context of the seL4 Microkernel. He boasts numerous contributions to significant conferences and journals. His primary areas of interest encompass embedded systems security, the Internet of Things, virtualization, and context-aware security.

seL4 Virtualization (ARMv8 Edge Device) Guest OS Performance & HA Recovery

Talk

Presented by Lei Mao, Horizon Robotics

Virtualization technology was widely used in X86 Cloud Server. There are various mature finetunes work was done for GuestOS Performance and High Availability Recovery.

In comparison, Virtualization in ARM Edge device(ARMv8 AACH64) was not so widely used. And its HW IP device usage model was very different from the Cloud scenario. The performance and HA is a challenge here.

In our advance research project, we explored some ways to improve that, e.g.

1) Support sel4 kernel fastpath virtual interrupt(for SPI/PPI/SGI/LPI) to shorten the long interrupt process route.

With this, Linux 5.10 GuestOS(cyclictest) average schedule latency will be reduced from 30us- >7us, close to RAW Linux 5.10 which was 5us

Note: Most++ COST ARMv8 SoC only have GICv3 interrupt controller IP, GOS interrupt direct inject was only supported in GICv4.

2) Support Virtual Machine Monitor (VMM) with vCPU symmetric multiprocessing (SMP) extension to speedup co-current helper services to GuestOS VMExits.

3) Support Virtual Machine Monitor (VMM) with HA Recovery extension to make Linux GuestOS recovery to working mode less than 1000 ms while crashing.

Note: Linux GOS basic system can recover less in 500ms, Linux GOS with an actual complex application may recover less in 1000 ms.

Building a Commercial Virtualized Mobile Device with seL4 – Part 2

Talk

Presented by Jason Sebranek, Cog Systems

Cog Systems, Inc. specializes in developing secure solutions leveraging virtualization on connected mobile devices. Cog Systems has developed a Virtualized Mobile Device (VMD) architecture and has placed the seL4 microkernel and Virtual Machine Manager (VMM) at its heart. Thus, the VMD is built on a Type-1 hypervisor which manages physical device hardware and acts as a very small Trusted Computing Base (TCB).

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 Virtual Private Network (VPN). This allowed Cog Systems to register the device with the National Security Agency (NSA) as an Approved Component under its Commercial Solutions for Classified (CSfC) process. Cog Systems is currently leveraging our VMD to develop a next-gen commercial virtualized smartphone - again planned for NIAP evaluation, CSfC inclusion, and commercial availability to the US government.

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. Cog Systems feels there is value in giving a follow-up presentation to discuss the progress, setbacks, and lessons learned in the past few years.

seL4 on RISC-V: Building a Trusted Execution Environment

Talk

Presented by Everton de Matos, TII

The use of Trusted Execution Environments (TEEs) is becoming increasingly common in the design of secure systems. TEEs provide a secure execution environment for sensitive applications and data, ensuring that they are protected from attacks and unauthorized access. TEEs are typically implemented as a separate execution environment within a system, with their own hardware and software resources that are isolated from the rest of the system. The trend towards the use of TEEs is driven by the increasing sophistication of cyber-attacks and the need for more robust security solutions. As such, the use of TEEs is becoming increasingly important in the design of secure systems, and technologies such as seL4 and RISC-V are playing a key role in their development.

In this talk, we will present our efforts on using seL4 on RISC-V to build a TEE service. We will discuss the challenges we faced during the development process and the solutions we implemented to address them. Additionally, we will provide an in-depth overview of our TEE architecture by discussing its features and demonstrating its functionality through real-world use cases. Our experimentation tests with the PolarFire Icicle kit have played a crucial role in enhancing our understanding of the platform and refining our implementation. Furthermore, we will discuss our ongoing efforts to improve and expand upon the TEE service and its potential applications, as well as outline our future research and development directions in this domain.

Trustworthy Measurements of a Linux Kernel and Layered Attestation via the seL4

Talk

Presented by Michael Neises, University of Kansas

This application-in-development leverages the seL4 proofs to provide assurance for the trustworthy and remote attestation of a Linux VM. By focusing on a Linux VM running on an ODROID XU4 platform, this work demonstrates the potential of seL4-based remote attestation across different hardware architectures and platforms.

The principles of remote attestation demand that the mechanisms of attestation are trustworthy. The seL4 guarantees properties of confidentiality and integrity, and these can be jointly understood as the seL4 enforcing the isolation of processes. This isolation allows the use of virtual machine introspection without fear of the virtual machine escape exploits to which previous software solutions are vulnerable. Here, the tools that introspect are trusted to measure a target because they are isolated from that target.

This attestation is layered in order to confine the adversary, and the layering is implemented at the architectural level using CAmkES. The adversary is confined to either corrupt the attestation tools or to rapidly corrupt and restore the target, bypassing the attestation tools. The seL4 permits an argument for the infeasibility of these strategies. However, the principles of remote attestation also demand that comprehensive information be generated over the target. Without a comprehensive measurement of the Linux environment, the adversary gains the option of hiding their corruption.

In support of a comprehensive measurement suite, an introspection library was implemented for a narrow range of Linux kernels. The library required a pathway for using arbitrary kernel modules in an arbitrary version of Linux, but the range of applicable kernels is narrow due to changes in how Linux manages its memory. The library facilitated the measurements of kernel modules, kernel and user processes, and kernel read-only data. Much more is required for a comprehensive measurement.

The principles also demand fresh information and constrained disclosure, which are simple matters of cryptography. Finally, the principles demand semantic explicitness, and this is largely considered in adjacent work that implements the Copland attestation language in CakeML extracted from Coq theorems. That work is integrated into this system. A way to use the latest versions of CakeML in seL4 threads independent from HOL4 was required.

It remains to implement a more comprehensive suite of measurements for the Linux kernel and the target program, and to demonstrate layered attestation on the bare metal of the ODROID XU4. If the measurements suffice to detect corruption, the appraiser will learn of this. Possible future work includes implementing this work for a wider range of Linux kernels and hardware platforms or formalizing a composition of seL4 kernel-level proofs and proofs over the attestation tools.