-
-
-
-
-
- seL4 Summit 2023
-
-
- Minneapolis, USA
-
-
- 19 - 21 September 2023
-
-
-
-
- Abstracts
-
-
-
-
- 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.
-
-
-
See this talk in the program
-
-
-
-
- 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.
-
-
-
-
-
See this talk in the program
-
-
-
-
-
-
- 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.
-
-
-
-
-
See this talk in the program
-
-
-
-
-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.
-
-
-
-
-
See this talk in the program
-
-
-
-
-
-
- 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.
-
-
-
-
-
See this talk in the program
-
-
-
-
-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.
-
-
-
-
-
See this talk in the program
-
-
-
-
-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.
-
-
-
-
-
See this talk in the program
-
-
-
-
-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.
-
-
-
-
-
See this talk in the program
-
-
-
-
-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.
-
-
-
-
-
See this talk in the program
-
-
-
-
-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.
-
-
-
-
-
See this talk in the program
-
-
-
-
-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.
-
-
-
-
-
See this talk in the program
-
-
-
-
-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.
-
-
-
-
-
See this talk in the program
-
-
-
-
-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.
-
-
-
-
-
See this talk in the program
-
-
-
-
- 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
-
-
-
-
-
See this talk in the program
-
-
-
-
-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.
-
-
-
-
-
See this talk in the program
-
-
-
-
-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.
-
-
-
-
-
See this talk in the program
-
-
-
-
- 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.
-
-
-
-
-
See this talk in the program
-
-
-
-
- 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.
-
-
-
-
See this talk in the program
-
-
-
-
- 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.
-
-
-
-
-
See this talk in the program
-
-
-
-
- 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.
-
-
-
-
-
See this talk in the program
-
-
-
-
- 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.
-
-
-
-
-
See this talk in the program
-
-
-
-
-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
-
-
-
-
-
See this talk in the program
-
-
-
-
- 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.
-
-
-
-
-
See this talk in the program
-
-
-
-
- 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.
-
-
-
-
-
See this talk in the program
-
-
-
-
- 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.
-
-
-
-
-
See this talk in the program
-
-
-
-
-
-
- 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.
-
-
-
See this talk in the program
-
-
-
-
- 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.
-
-
-
-
-
See this talk in the program
-
-
-
-
- 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.
-
-
-
-
-
See this talk in the program
-
-
-
-
- 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.
-
-
-
-
-
See this talk in the program
-
-
-
-
- 
- Being a kernel means it is the piece
- of software that runs at the heart of any software system and
- controls all accesses to resources. It provides fine-grained
- access control through 
- 
- 
- 
- 
- 
- 
- 
- 
- 
- 
- 
- 
- 
- 
- 
- 
- 
- 
- 
- 
- 
- 
- 
- 
- 
- 
- 
- 
- 
- 
- 
- 
- 
- 
- 
- 
- 
- 
- 
- 
- 
- 
- 
- 
- 
- 
- 
- 
- 
- 
- 
- 
- 
- 
- 
- 
- 
- 
- 
- 
- 
- 
- 
- 
- 
- 
- 
- 
- 
- 
- 
- 
- 
- 
- 
- 
-
-
- 
- 
- 
- The seL4 Foundation thanks Ghost for its
- generous contribution. Ghost's commitment strengthens the seL4
- Foundation's mission to continue advancing the ecosystem, the code
- base, and the verification efforts of seL4, the world's most
- advanced and highly assured operating-system kernel.
-
- 
- 
-
- On 29th July 2009, the original functional correctness proof of seL4 was
- completed, a widely-recognised research breakthrough and the first big
- milestone in seL4's history. We obviously had a party then, and have since
- celebrated its anniversary, calling it, tongue-in-cheek, “International Proof
- Day”.
-
- 
- 
- 
- 
- 
- 
- 
- 
- 
- 
- 
-
- 
- 
- 
- 
- 
- 
- 
- 
- 
- 
- 
- 
- 
- 
- 
- 
- 
- Darren Cofer is a Principal Fellow at Collins Aerospace. He
- earned his PhD in Electrical and Computer Engineering from The University of
- Texas at Austin. His area of expertise is developing and applying advanced
- analysis methods and tools for verification and certification of
- high-integrity systems. His background includes work with formal methods for
- system and software analysis, the design of real-time embedded systems for
- safety-critical applications, and the development of nuclear propulsion
- systems in the U.S. Navy. Dr. Cofer has served as principal investigator on
- many government-sponsored research programs, developing and using formal
- methods for verification of safety and security properties. He served on
- RTCA committee SC-205 developing new certification guidance for airborne
- software (DO-178C) and was one of the developers of the Formal Methods
- Supplement (DO-333). He is currently a member of SAE committee G-34
- developing certification guidance for the use of machine learning
- technologies onboard aircraft.
- 
- Ning Qu is a veteran in the autonomous driving industry and
- a seasoned technical leader with extensive experience in operating systems,
- high-performance runtime frameworks, and hardware-software co-design.
- Currently, Ning serves as the Senior Director of the SkyOS team at NIO,
- where he spearheads the development of SkyOS—a comprehensive suite of
- platform software (including hypervisor, operating systems, and middleware)
- for Software Defined Vehicles, showcased at NIO IN 2023. Before joining NIO,
- Ning managed Waymo's ML Runtime team, playing a pivotal role in SF
- Rider-only driverless launch on the Jaguar EV. At Baidu, he built the Apollo
- OS from the ground up, establishing the foundation for the Apollo project.
- Notably, he architected and developed Cyber RT and led Baidu's fully
- driverless launch in 2020. Ning holds a B.S. and Ph.D. from Peking
- University and has served as a researcher at CMU.
- 
-
- 
-
-