- Devel - lists.sel4.systems

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

Are there any users of 32bit seL4/x86 left?
by Gerwin Klein 25 Aug '26

25 Aug '26

Before I write up a proper RFC for this, a poll: Is anybody still using the 32-bit x86 support of seL4? Given that Microkit only supports x64 and even most Linux distributions have removed support for 32 bit x86, my impression is that this port is now mostly unused. Since it is a maintenance burden, it would make sense to phase out support for it in seL4 so there is more time available to concentrate on newer hardware. If you don’t want to reply publicly for some reason, it’s fine to email me privately. No matter the outcome, there will be an official RFC with the usual comment period before anything is decided. Cheers, Gerwin

1 0

seL4 security proofs now complete on AArch64
by June Andronick 24 Aug '26

24 Aug '26

The verification of seL4 on the 64-bit Arm architecture has reached another milestone. After completing the proofs of functional correctness and integrity, Proofcraft has now established the proof that seL4 enforces confidentiality on AArch64, providing a formal mathematical proof that the kernel prevents an application running on top of seL4 from learning information without authorisation. This milestone completes the formal proof that the seL4 implementation code on AArch64 enforces security isolation of the applications running on top (under the assumptions listed here [0]). This isolation prevents attacks on non-critical applications from propagating to critical applications and compromising them. https://proofcraft.systems/news-2026/#2026-08-21 [0] https://sel4.systems/Verification/assumptions.html June

1 0

seL4 developer hangout reminder
by Birgit Brecknell 17 Aug '26

17 Aug '26

Hi all A friendly reminder that the seL4 developer hangout is on again this week. Wed 19 Aug, 8:00 UTC 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

seL4 developer hangout reminder
by Birgit Brecknell 03 Aug '26

03 Aug '26

Hi all A friendly reminder that the seL4 developer hangout is on again this week. Tue 4 Aug, 22:00 UTC 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

seL4 Day Party!
by Gernot Heiser 24 Jul '26

24 Jul '26

Trustworthy Systems will be celebrating seL4 Day with a little party, starting 13:00 Sydney time, at the TS digs on Level 3 of the CSE Building (K17) on UNSW’s Kensington campus. Any seL4 developers in town are welcome to attend! Gernot

1 0