September 2026 - Devel - lists.sel4.systems

Announcing Neptune OS v0.4, now running Linux kernel drivers in userspace on seL4
by Dr. Chang Liu, PhD. 21 Sep '26

21 Sep '26

Dear list, I am announcing release v0.4 of Neptune OS [0], a general purpose Windows NT-like operating system built on top of seL4. The main feature of this release is a new driver subsystem that allows unmodified (or at most minimally modified) Linux kernel drivers to run as native userspace processes on seL4. By 'native' I mean that these are just regular, unprivileged user processes: there is no virtual machine or any kind of virtualization technology involved, at all. These drivers communicate with the rest of the system via the standard NT driver APIs and appear to the OS as regular, native NT drivers without the need of any special handling. Therefore, I believe with some effort our approach can be adapted to work on other NT-like OSes, including ReactOS and Windows itself, and potentially (with some greater effort) to other seL4-based OSes as well. Before we get into the technical details, here [1,2] are two videos demonstrating Linux kernel GPU (AMDGPU, i915, virtio_gpu) and Ethernet (e1000e) drivers running as native user processes on Neptune OS. We show that these GPU drivers can successfully POST the GPU cards and perform mode setting and framebuffer mapping, and that we can have a basic networking stack capable of packet TX/RX via the Ethernet driver. I hope these examples demonstrate the validity of our approach as the drivers involved here are massive, highly nontrivial beasts (especially in the case of AMDGPU) that drive complex, modern hardware, and their correct function, even for seemingly simple things like mode setting (which is actually not so simple in modern graphics cards), depends on the correct behavior of memory management, timers, workqueues, IRQs, RCU, and many other Linux kernel subsystems. With the exception of i915 (which needs some patching due to its use of the wbinvd instruction), the drivers involved are otherwise completely unmodified. Now some technical details. One of the defining features of the NT architecture is its support for multiple userspace programming interfaces, including Win32 and POSIX, via the so-called Environment Subsystems. These environment subsystems sit on top of the NT Executive and essentially "translate" the APIs spoken by, say a Win32 application, to the native NT API exposed by the Executive. Since Neptune OS has moved the NT Executive to userspace on seL4 and every NT driver now runs as unprivileged user processes, the idea of a userspace Linux driver subsystem becomes a natural extension to these environment subsystems. To the rest of the NT OS, the Linux driver subsystem is simply a regular NT driver (sitting under drivers/lib/lnxdrv in the source tree) that speaks the standard NT driver API (exposed by the Executive) and participates in the usual IO request packet flow. It somehow "magically" translates the NT driver API into the Linux kernel API so that a Linux device driver, say amdgpu or i915, responds to IO requests just like any other native NT driver does. Of course, it would be completely impractical to actually implement a compatibility layer that translates the NT driver API to the Linux kernel API, as the latter is not only highly complex, but also very much unstable. The solution to this problem is inspired by the approaches taken by UML (usermode Linux) and the lkl (Linux-kernel-as-a-library) project. The idea is to add a new architecture port to the Linux kernel (under arch/ntos in the Linux source tree). This architecture port defines how the Linux kernel requests hardware resources, such as memory and IRQ, by calling the host NT OS (eg. request_irq will eventually be routed to IoConnectInterrupt, an NT driver API call). Additionally, a new config switch CONFIG_KERNEL is added to the main arch-independent part of the Linux kernel, which gates the schedulers and other core kernel components behind it. When built without CONFIG_KERNEL, the resulting kernel binary is stripped of what makes Linux an independent OS kernel and becomes essentially a runtime library for kernel driver modules. When loaded by the aforementioned NT driver (lnxdrv.sys), this Linux kernel binary is supplied with an "import table" which the Linux side can call, and returns an "export table" for the NT side to call. The import table defines the interface with which the Linux side can request resources from the NT side (eg. allocating memory or scheduling an IO work item), and the export table defines the services that the Linux side provides to the NT side (eg. responding to a READ IO request). Some thunking magic needs to happen for the PE and ELF images to be able to call each other, but it all turns out to work pretty well (this is similar to the PE+ELF split used in modern WINE). Communication between the NT side and the Linux side is done entirely via these import and export tables. This way we shield the NT side from the complex, volatile Linux kernel API and maintain a clean separation between the two sides. Additionally, this design allows us the flexibility to potentially extend our work to other non-NT OSes, including other seL4-based OSes: another OS just needs to implement the same interface in these import/export tables to reuse our work. One further benefit is that we are part of the Linux kernel source tree, so updating to a newer Linux kernel is just a git rebase away (as I have done during the development cycle), as the changes to the arch-independent kernel is very minimal (I'm not sure if upstream Linux is ever going to accept this into the mainline tree, but one can hope). Anyway, if you have read this far, I hope you do find this work interesting. I believe with the introduction of the Linux driver subsystem, there would be a real chance that Neptune OS could become something useful beyond a hobby operating system. I am therefore actively looking for funding to continue the work on Neptune OS, so if you are interested, please do let me know. [0] https://github.com/cl91/NeptuneOS [1] https://youtu.be/BJIrUZIGgBc [2] https://youtu.be/YTdqeGk54to --- Dr. Chang Liu, PhD. github.com/cl91/NeptuneOS

2 3

QSOE: QNX-inspired OS with dual-kernel architecture (custom kernel & seL4)
by Yuri Zaporozhets 18 Sep '26

18 Sep '26

Hi! This is my project which I recently announced: https://qsoe.net Interestingly, when working in the shell (mksh-derived), the subjective "feeling" is that QSOE/N (with Skimmer) is ~10 times faster than /L :) . Launching e.g. "time ls" command confirms this: 0.1s for QSOE/L (with seL4) vs. 0.01s for QSOE/N. The work continues. Now I'm working on a video controller support for my SiFive Unmatched; then, when the _real_ text-mode console is there, I'll return to active QSOE developments. -- Regards, Yuri

1 1

The videos and slides of the seL4 Summit 2026 are available online
by Birgit Brecknell 16 Sep '26

16 Sep '26

The videos and slides of the seL4 Summit 2026 are available online Videos of the seL4 Summit 2026 [0] are now available on the seL4 YouTube channel [1]! Links, slides, and posters can be found on the summit Program [2] and Abstracts [3] pages. Thanks to all the speakers for making the seL4 Summit 2026 a great success [5]! [0] https://sel4.systems/Summit/2026/ [1] https://www.youtube.com/playlist?list=PLd7rrADYxxQQ [2] https://sel4.systems/Summit/2026/program.html [3] https://sel4.systems/Summit/2026/abstracts2026.html [4] https://sel4.systems/Summit/2026/#gallery -- Birgit Brecknell seL4 Foundation Project Coordinator Sydney, Australia Mon 9-5 Wed 2-5 Fri 9-5 birgit(a)sel4.systems bbrcknl(a)gmail.com

1 0

Cohesix 1.0.0-beta — AArch64 SMP+MCS, isolated Rust drivers, and Pi 4 images
by Lukas Bower 14 Sep '26

14 Sep '26

Hi all, Following my initial announcement in January, I’m pleased to announce Cohesix 1.0.0-beta. Cohesix is an Apache-2.0 research operating system for edge GPU orchestration, built on seL4 with pure Rust no_std target userspace. It combines capability-based resource control with a Plan 9-inspired namespace for commands, telemetry, and policy. GPU execution stays on the host; Cohesix coordinates authority, leases, and task lifecycles. This is a substantial architectural change from 0.9.0. Several parts may be of particular interest to this list. - AArch64 SMP+MCS on seL4 16.0.0 The QEMU and Pi 4 profiles use four cores, with explicit scheduling contexts for control, fault handling, supervision, drivers, and Worker executors. The NineDoor namespace service and executable Workers are passive children served through scheduling-context donation and Call/Reply. The aim is to make execution budgets and the authority to consume them inspectable alongside the capability topology. - Isolated drivers with explicit cooperation between runtimes Pi drivers execute in separate CSpaces/VSpaces, with HAL admitting their device resources. Generated links use bounded, pointer-free request/completion records, shared buffers, and notifications. For example, CYW43 owns Wi-Fi firmware and protocol state while a separate SDIO runtime owns the physical bus. On Ethernet, an explicit post-DHCP handoff connects the GENET driver directly to the isolated TCP/console service, removing root from the steady packet path. - Manifest-driven system construction The coh-rtc compiler validates the selected profile and generates resource inventories, scheduling parameters, runtime descriptors, and policy tables. Device ownership, shared-memory links, and queue bounds are declared together, giving contributors a concrete contract for adding or reviewing a runtime. - Passive Worker populations with bounded execution Both target profiles configure 256 Worker instances across heartbeat, GPU-lease, and model-lifecycle roles, served by two active executor lanes. Each instance retains its own capability and lifecycle identity, including generation checks across replacement. This separates the number of represented control-plane tasks from the number of active scheduling contexts. - Trying the release There are prebuilt bundles for Apple Silicon macOS and Linux AArch64, including their matching QEMU guests and host tools, plus a complete Raspberry Pi 4 SD image. No GPU is needed to explore the OS in QEMU. Downloads: https://github.com/lukeb-aidev/cohesix/tree/main/releases Release notes: https://github.com/lukeb-aidev/cohesix/blob/main/releases/RELEASE_NOTES-1.0… Quickstart: https://github.com/lukeb-aidev/cohesix/blob/main/docs/QUICKSTART.md Architecture: https://github.com/lukeb-aidev/cohesix/blob/main/docs/ARCHITECTURE.md Driver contracts: https://github.com/lukeb-aidev/cohesix/blob/main/docs/DRIVERS.md I’d particularly welcome feedback on the passive-service donation model, driver-link ownership, and the boundary between generated policy and runtime enforcement. Code review, hardware observations, and comparisons with other seL4 system designs would all be valuable. This remains a research beta. No formal verification of Cohesix or its selected SMP+MCS configuration is claimed. The release notes document qualification limits, including outstanding fault/wake evidence, an unrepeated full burn-in, and the absence of fresh runtime qualification for the published builds. Best, Lukas Bower

1 0

seL4 developer hangout reminders
by Birgit Brecknell 14 Sep '26

14 Sep '26

Hi all A friendly reminder that the seL4 developer hangout is on again in the coming weeks. (I'll be on leave 21 Sep - 6 Oct, so won't send reminders during this time). - Wed 16 Sep, 8:00 UTC - Tue 29 Sep, 10pm For your local date and time please see https://sel4.systems /stay-informed.html#calendar Zoom link: https://unsw.zoom.us/j/82640784431 -- Birgit Brecknell seL4 Foundation Project Coordinator Sydney, Australia Mon 9-5 Wed 2-5 Fri 9-5 birgit(a)sel4.systems bbrcknl(a)gmail.com

1 0

BCM2711 (Raspberry Pi 4B) support in libsel4vm — is this wanted?
by shankaradi1511＠gmail.com 09 Sep '26

09 Sep '26

Hi, The kernel supports and formally verifies bcm2711, but libsel4vm doesn't build for it: gicv2.h has no GIC_PADDR branch, and libsel4vmmplatsupport has no plat_include/bcm2711. I have a small patch (2 lines in gicv2.h, 2 new headers) that I've been using to run VMs on a Raspberry Pi 4B, single-core and 4-core SMP. GIC_PADDR is 0xff840000 — the ARM view of the GIC-400; the rpi4 DTS gives the VideoCore view, and the ARM addresses come from the kernel's generated devices_gen.h. The same value appears in tiiuae's rpi4 branch, derived independently. Before opening a PR I wanted to ask about direction. I see #83 proposes reading these addresses from the device tree, and #58 (GICv3 emulation) has cleanup PRs held back pending it. Is adding another per-platform #elif still acceptable, or would you rather this waited? Two caveats: there's no upstream VM application for this board, so nothing in CI would exercise it; and the vpci.h values are taken from tiiuae's branch — my guests are bare-metal and exercise no PCI path, so I haven't verified them. Happy to rework or drop it. git show bcm2711-platform-support commit ef8f6257ef17a457df075154e81353e6b1eeb39a (HEAD -> bcm2711-platform-support) Author: Shankaraditya N S <shankaradi1511(a)gmail.com> Date: Tue Sep 8 20:21:58 2026 +0530 libsel4vm/libsel4vmmplatsupport: add BCM2711 (Raspberry Pi 4B) support Signed-off-by: Shankaraditya N S <shankaradi1511(a)gmail.com> diff --git a/libsel4vm/src/arch/arm/vgic/gicv2.h b/libsel4vm/src/arch/arm/vgic/gicv2.h index c801b88..aa3c831 100644 --- a/libsel4vm/src/arch/arm/vgic/gicv2.h +++ b/libsel4vm/src/arch/arm/vgic/gicv2.h @@ -24,6 +24,8 @@ #define GIC_PADDR 0xc4300000 #elif defined(CONFIG_PLAT_ZYNQMP) #define GIC_PADDR 0xf9000000 +#elif defined(CONFIG_PLAT_BCM2711) +#define GIC_PADDR 0xff840000 #elif defined(CONFIG_PLAT_STM32MP2) #define GIC_PADDR 0x4ac00000 #else diff --git a/libsel4vmmplatsupport/plat_include/bcm2711/sel4vmmplatsupport/plat/guest_vcpu_util.h b/libsel4vmmplatsupport/plat_include/bcm2711/sel4vmmplatsupport/plat/guest_vcpu_util.h new file mode 100644 index 0000000..4ad9935 --- /dev/null +++ b/libsel4vmmplatsupport/plat_include/bcm2711/sel4vmmplatsupport/plat/guest_vcpu_util.h @@ -0,0 +1,9 @@ +/* + * Copyright 2026, Shankaraditya N S + * + * SPDX-License-Identifier: BSD-2-Clause + */ + +#pragma once + +#define PLAT_CPU_COMPAT "arm,cortex-a72" diff --git a/libsel4vmmplatsupport/plat_include/bcm2711/sel4vmmplatsupport/plat/vpci.h b/libsel4vmmplatsupport/plat_include/bcm2711/sel4vmmplatsupport/plat/vpci.h new file mode 100644 index 0000000..07acc59 --- /dev/null +++ b/libsel4vmmplatsupport/plat_include/bcm2711/sel4vmmplatsupport/plat/vpci.h @@ -0,0 +1,23 @@ +/* + * Copyright 2022, Technology Innovation Institute + * + * SPDX-License-Identifier: BSD-2-Clause + */ + +#pragma once + +/* PCI host bridge configuration space */ +#define PCI_CFG_REGION_ADDR 0x100000000ULL +/* PCI host bridge IO space */ +#define PCI_IO_REGION_ADDR 0x101000000ULL +/* Size of PCI configuration space */ +#define PCI_CFG_REGION_SIZE 0x1000000 +/* Size of PCI IO space */ +#define PCI_IO_REGION_SIZE 0x10000 +/* PCI memory space */ +#define PCI_MEM_REGION_ADDR 0x60000000ULL +/* PCI memory space size */ +#define PCI_MEM_REGION_SIZE 0x60000000 + +/* FDT IRQ controller address cells definition */ +#define GIC_ADDRESS_CELLS 0x1 (END)

2 1