seL4 Summit 2024

Formal methods have been successfully deployed at scale in production environments at large internet companies, but barriers remain to their adoption by defense companies developing national security systems. The goal of the INSPECTA project (part of the DARPA PROVERS program which has just started in 2024) is to improve the security of defense and aerospace systems by dramatically improving the usability, flexibility, and accessibility of formal methods-based development and verification tools. We will leverage memory-safe programming languages (Rust), a provably secure microkernel (seL4), and new formal methods tools and make them accessible to the defense industry workforce. These open source technologies will be integrated into an aerospace CertDevOps workflow automation processes and applied to the development of mission critical systems to demonstrate their usability, practicality, and effectiveness. We will demonstrate the tools and workflow by addressing emerging security requirements for the Air Launched Effects (ALE) mission computing platform. This will include rearchitecting the mission software as a collection of virtual machines running legacy code and selected high-criticality components, producing an architecture model for the system, porting selected software to Rust, building software to run on seL4, and verifying critical safety and security properties. This presentation will provide an overview of the PROVERS program objectives, the INSPECTA workflow to be developed, and the assurance evidence to be produced.

In this talk we will give an overview of Proofcraft's recent milestones, as well as ongoing and future plans for the formal verification of seL4 to support more platforms, architectures, configurations, and features.

In particular, we will report on the completion of the functional correctness proof of seL4 on AArch64. AArch64 is now on par with Arm 32-bit, RISC-V 64-bit and Intel x86 64-bit with respect to functional correctness, the strongest assurance that can be given about the correctness of software. Functional correctness is also the cornerstone of even stronger overall assurance, such as the security properties of integrity and confidentiality, which are next inseL4's AArch64 verification roadmap.

We will further report on where the verification of the seL4 extensions for mixed-criticality systems (MCS) is at, and share our plans for DARPA's PROVERS program where, as part of the INSPECTA team, we are aiming at increasing verification automation and scope while reducing the reliance on formal methods experts.

In this talk we will present Proofcraft's roadmap for producing a verified static
multikernel configuration of seL4, allowing the use of multiple CPU cores with
one kernel per core. In this roadmap, we are planning to increase formal
assurance incrementally, providing a tractable path to multicore verification
with early usable results for the seL4 community.

Formally proving correctness on a multicore platform requires the ability to
model fully concurrent execution, and then prove that any interactions either
do not occur or are safe. This requires a new formal model of execution,
supporting concurrency reasoning.

We will report on our progress in building such a framework, with the aim to
maximise the reuse of existing proofs. We will also present how starting with a
static multikernel design is the fastest path to providing the community with an
seL4 kernel that allows utilisation of multiple processor cores, opening the
path to building multicore seL4-based systems that come with a formal proof of
correctness.

Neutrality(1) is building the Atoll hypervisor as a high-assurance platform for the secure multitenant virtualisation of workloads which are likely targets of well-resourced attackers. Atoll will use seL4 configured as a multikernel to provide verified isolation between multi-vCPU VMs on datacenter-class hardware containing hundreds of CPU cores, terabytes of main memory, and 100GbE-class self-virtualising (SR-IOV) NICs. This project places seL4 on a wholly new playing field, with orders-of-magnitude increases in hardware performance and the associated scaling challenges, while retaining the full verified assurance of the seL4/ARM stack. In particular, Atoll will provide fully-verified Integrity and Confidentiality between customer VMs, while efficiently handling commercial-scale workloads.

In this talk, we will give an overview of Atoll’s design, and explain how it addresses the challenges unique to this application domain. In particular we will motivate the choice of the multikernel as the ultimate design rather than as a
stepping stone on the way to a verified SMP kernel, the benefits and challenges that arise from this choice, and other details of likely interest to others building multi-processor systems on seL4. In particular we will discuss the implications
for verification, including on our own verification plan, and where we expect to coordinate with and contribute to the overall seL4 proof roadmap.

(1) https://neutrality.ch/

Lions OS is a new, seL4-based, open-source operating systems aimed at the embedded/IoT/cyberphysical space. Based on the Microkit, Lions OS features a static system architecture, i.e. all (potential) components and their (maximum) connectivity are known at system build time. Lions OS is characterised by a highly modular design, driven by the principles of strong separation of concerns and strict adherence to the KISS principle – keep it simple, stupid! The “radical simplicity” design, when done right, enables excellent performance despite the many context switches resulting from the fine-grained modularity. Critically, this modularity, coupled with keeping each module as simple as possible, should enable formal verification of Lions OS.

Taking the KISS principle to the extreme, Lions OS radically departs from the idea of universal policies, adaptable to many different use cases, that characterise most existing OSes. In contrast, Lions OS keeps all policies minimal and specific to the particular use case; it achieves use-case diversity by isolating each policy in an individual module that can be easily rewritten/replaced when a different policy is required.

In the talk I will explain the principles of Lions OS and its design, looking at concrete examples. I will present performance data that show that the approach can work and provide an overview of our current work on verification. This will be complemented by Ivan Velickovic’s talk covering Lions OS from a developer’s point of view, and Rob Sison’s and Courtney Darville’s talks on verifying Lions OS.

LionsOS is a new Operating Systems developed at Trustworthy Systems aimed at embedded, IoT, and cyberphysical systems. LionsOS is based on the seL4 Microkit and is desgined to formally verifiable, performant, and adaptable to a
wide class of use-cases.

Gernot's talk will discuss the principles and design of LionsOS, while this talk will be focused on aspects of LionsOS from a developer's perspective.

We will dive into what it is like to use LionsOS by showcasing the tooling and surrounding infrastructure that has been created for developing a LionsOS-based system. This will cover topics such as I/O, virtualisation, debugging, profiling,
as well as how to put all these pieces together.

Several frameworks, such as CAmkES and the seL4 Microkit, have been built on top of seL4 to enable the development of performant and provably secure operating systems. Most of these have static architectures and use system descriptions that define a complete system including all components and the resources they can access. The system specification is then passed to tools like CapDL, which generate the described system with the correct capability distribution. An important attribute of frameworks like CAmkES and Microkit is that they do not allow this initial distribution to evolve, preventing the runtime transmission of capabilities within an initialized system. This makes them well-suited for static analysis and verification, but comes with the caveat that some behaviours become more difficult or even impossible to represent. In particular, static frameworks are unsuitable for dynamic systems that adhere to complex security policies, especially ones that depend on runtime behaviour, or require functionality such as the ability to create new, sandboxed components, or temporarily transfer privileges between components at runtime.

The Secure Multiserver Operating System (SMOS) project aims to create a secure, dynamic OS framework on top of seL4. Our goal is to enable the development of systems as dynamic as mainstream operating systems like Linux, that allow you to, for example, download and run arbitrary executables, while leveraging the security properties of seL4 to ensure that a global security policy is always correctly upheld. This talk will focus on the key principles behind the design of SMOS, the progress we have made on its implementation, and an overview of some of the challenges we have encountered, both in development and in correctly enforcing a variety of arbitrary, often complex security policies at runtime.

Upstream hypervisor support has expanded in recent years to support additional configurations on x86, ARM, and RISC-V. Every upstream example simply runs Linux, which is an excellent use case for highly functional, general purpose computing platforms, however there are other guest Operating Systems that solve different use cases. Running seL4 in Hypervisor mode allows for the untrusted code in Linux to be sandboxed and isolated from trusted components in the system. What if the guest Operating System was fully trusted? Deos is a DO-178C DAL A certified RTOS for Avionics Applications, an area seL4 has struggled to break into. DornerWorks expanded seL4 Hypervisor support to run Deos under the CAmkES VM. This presentation will overview the changes that needed to be made to support a certifiable RTOS guest, how a Hypervisor effects the safety certification considerations of Deos, and the next steps needed to create a certifiable system with seL4. 

ROS (Robotic Operating System), a modular componentized architecture for robot applications, has made it possible to quickly develop and deploy systems utilizing autonomous or human guided robots.  Focusing on ease of use and portability, ROS has enabled a community of developers to create autonomy solutions that were previously restricted to well-funded companies.  However, ROS depends on many services included in a full Linux distribution to function properly.  Beyond the Operating System itself, these distributions contain many unvetted software packages, which when used in high assurance environments, such as factory automation, could present an unacceptable amount of overhead and potential vulnerabilities.

Even in less critical environments, a compromised robot could surreptitiously spy on an end user or subtly/overtly cause harm to the environment in which it operates.  While securing such systems with seL4 seems like an obvious solution, the lack of support for common software APIs and middleware presents a significant hurdle. Once this is overcome wider adoption of seL4 and more resilient robotic systems would be enabled.  This presentation will show how the cyber-retrofit approach is being used to enable secure autonomous operation of an x86 based ground vehicle, how this approach is being extended to enable native seL4 ROS applications, and the barriers to further system hardening.

We have developed a minimal networking stack (Ethernet, IP, UDP, and ICMP) with the overarching goal of proving that it implements its specification correctly. We target our implementation for the embedded market and therefore we have chosen to develop our solution around the seL4 Microkit and the seL4 Device Driver Framework.
In this talk, we report on our experience developing, testing, and characterizing the performance of our implementation using the seL4 ecosystem. We have containerized our development environment to simplify building our application and to support users with differing platforms. In addition to relying on automated theorem prover assistants and model checkers, we have written many unit and integration tests to help write correct software. Using a network benchmark, we show that our solution exhibits competitive, if not superior, performance characteristics both in terms of average behavior and variance.

This talk presents an experience report on migrating seL4-based systems from the CAmkES VMM to the Microkit VMM. Microkit is a simple framework and SDK created to enable more efficient designs and lower the barrier to entry to seL4.  The presentation will compare and contrast MicroKit with CAmkES and highlight a few reasons to start using Microkit.  In addition, it will examine how MicroKit can make learning and developing seL4-based systems easier and breakdown roadblocks encountered by new users when porting to a new platform. Finally, we will present our gap analysis between the two VMMs and highlight what still needs to be addressed so users can start developing real-world products. 

In this talk, June Andronick, CEO of the seL4 Foundation, will give a brief overview of the latest updates and future plans for the seL4 Foundation.

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.