- Devel - lists.sel4.systems

seL4 developer hangout reminder
by Birgit Brecknell 02 Feb '26

02 Feb '26

Hi all A friendly reminder that the seL4 developer hangout is on again this week. Wed 4 Feb, 7: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 <mailto:birgit@sel4.systems> bbrcknl(a)gmail.com <mailto:bbrcknl@gmail.com>

1 0

** Cohesix 0.1.0‑alpha1 — Release Announcement
by Lukas Bower 24 Jan '26

24 Jan '26

Excited to ship the Cohesix 0.1.0‑alpha1 release: a control‑plane OS targeting aarch64, for secure orchestration + telemetry of edge GPU nodes, built on seL4 with a pure‑Rust userspace and a Queen/Worker hive model. This release focuses on repeatable bundles, SwarmUI replays, and CLI workflows: https://github.com/lukeb-aidev/cohesix/blob/main/README.md https://github.com/lukeb-aidev/cohesix/tree/main/releases Best, Lukas Bower

1 0

seL4 developer hangout reminder
by Birgit Brecknell 19 Jan '26

19 Jan '26

Hi all A friendly reminder that the seL4 developer hangout is on again this week. Tue 20 Jan, 21: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 <mailto:birgit@sel4.systems> bbrcknl(a)gmail.com <mailto:bbrcknl@gmail.com>

1 0

issue with elfloader ret instruction while enabling the MMU on armv8-a
by Christian Bruel 15 Jan '26

15 Jan '26

Hello seL4 team, I would like to share an issue found with the port of seL4 and VMs to the STM32MP2 SoC, which features Armv8-A dual Cortex-A35 cores: When activating the secondary core, The RET instruction crashes while executing the arm_enable_mmu(). The exception stack and ESR register show no useful information. Simply replacing the RET instruction with BR X30 resolves the issue. Furthermore, before RET, a check with the AT S1E1R, X30 shows correct memory translation in the PAR_EL1 register, confirming proper MMU setting, which is also supported by the successful BR X30 workaround. Just to be sure I tried to replace the current 1Gb translation table with a finer 4Bb granularity and P:EX U:NX and RO access flags for the Non Secure code execution. Same results. I also set the ASID bits, same result. So back to the current implementation and BR X30 workaround: According to the Arm Architecture Reference Manual [1], the RET instruction behaves identically to BR but provides an additional hint that this is a return from a subroutine. AFAIU, such hints can be related to the branch predictor or the return address stack used for ROP protection, (if the feature is available). In “Requirements for branch predictor maintenance” [2], branch prediction maintenance operations must be performed after enabling or disabling the MMU. However, these operations translate as a NOP if the branch predictor hardware is not architecturally visible. Therefore, the ‘BL/RET’ behavior from different translation regime seems to to be implementation-dependent or dependent on optional architectural features Thus, replacing MMU enable sequence: enable_mmu sctlr_el1 x8 ldp x29,x30,[sp],#16 ret with a trampoline: adr x30,mmu_on ldp x29,x9,[sp],#16 ret mmu_on: enable_mmu sctlr_el1,x8 br x9 is enough to start seL4 with SMP=on NUM_NODES=2 and run a dual core Linux on the CAmkES VM. This is semantically equivalent to the BL X30 workaround, but this is more explicit regarding the MMU translation regime around BL/RET. NB: arm_enable_hyp_mmu() needs the same change as the issue happens equivalently in EL1 or EL2. Thank you very much for your thoughts on this issue. Best Regards Christian References: [1] Arm Architecture Reference Manual (DTI 0487) [2] Arm Architecture Reference Manual ARMv7-A and ARMv7-R edition

2 3

seL4 developer hangout reminder
by Birgit Brecknell 05 Jan '26

05 Jan '26

Hi all A friendly reminder that the seL4 developer hangout is on again this week. Wed 7 Jan, 7: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 <mailto:birgit@sel4.systems> bbrcknl(a)gmail.com <mailto:bbrcknl@gmail.com>

1 0

Re: Announcing release v0.3 of Neptune OS, a Windows NT personality for seL4
by Dr. Chang Liu, PhD. 04 Jan '26

04 Jan '26

In theory if you implement the same interfaces that the NT Executive exposes to client drivers, potentially yes --- the relevant code has around 5K LOCs so it is not that big. --- Dr. Chang Liu, PhD. github.com/cl91/NeptuneOS On Tue, Dec 30, 2025 at 6:11 PM Demi Marie Obenour <demiobenour(a)gmail.com> wrote: > On 12/30/25 04:35, Dr. Chang Liu, PhD. via Devel wrote: > > Additionally, due to the lack of high quality open-source Windows > drivers, > > a big part of the next release will be focused on designing and building > a > > subsystem which allows Linux drivers to run natively (without emulation) > as > > userspace processes on Neptune OS, so stay tuned! > > Is this something that could be reused for other seL4-based OSs? > -- > Sincerely, > Demi Marie Obenour (she/her/hers)

2 1

Announcing release v0.3 of Neptune OS, a Windows NT personality for seL4
by Dr. Chang Liu, PhD. 30 Dec '25

30 Dec '25

Dear List, I am announcing the v0.3 release [1] of Neptune OS, a Windows NT personality built on top of the seL4 microkernel. Neptune OS implements the upper layer of the Windows kernel (the "NT Executive") as a user space process under seL4, providing NT-like interfaces via standard seL4 IPC primitives to device drivers and user programs. These then allow Windows device drivers to be ported to run as user space processes under Neptune OS, with potentially greater degree of isolation and fault recovery than can be achieved under a traditional macro-kernel or hybrid-kernel design. The highlights of the v0.3 release are a bunch of computing industry acronyms: UEFI, ACPI, PCI(E), AHCI, and NVME. We have improved upon the basic NT PnP manager implementation we had in the previous release and ported over the ACPI and PCI(E) drivers from ReactOS, to enable completely dynamic discovery/enumeration, resource assignment, lifetime cycle, and power management of hardware devices. The hope is that this will eventually make Neptune OS suitable as a general purpose OS that must manage an ever-changing device landscape, while still being able to leverage seL4's strong isolation and formal guarantees. Built upon this work, we have ported over what I hope is a reasonably complete portion of the Windows storage device driver stack, consisting of the class drivers (classpnp.sys, disk.sys), the storage port driver (storport.sys), two storage miniport drivers (for AHCI and NVME), and the partition manager (partmgr.sys) and mount-point manager (mountmgr.sys). Among these, the class drivers as well as the AHCI miniport driver are from the official Microsoft sample drivers [3], the NVME miniport driver is from Open Systems Alliance [4], and storport, partmgr, and mountmgr are from ReactOS. These drivers total an over-120K codebase and with the exception of storport where some missing pieces had to be added due to the incompleteness of the ReactOS implementation, are largely unmodified. I hope the non-triviality of these drivers serves as a convincing demonstration that our design is capable of reusing complex, real-world Windows drivers in a microkernel-based OS (which NT had originally hoped to be, allegedly). I have recorded a short video [2] showing the ACPI and AHCI driver stack in action, including device tree enumeration, power management (reboot/poweroff), and basic shell commands. This release also includes a basic disk IO benchmarking tool. Based on some early testing we seem to be able to saturate the AHCI bandwidth without a problem, but NVME seems to be underperforming. This will be part of the work going into the next release. Additionally, due to the lack of high quality open-source Windows drivers, a big part of the next release will be focused on designing and building a subsystem which allows Linux drivers to run natively (without emulation) as userspace processes on Neptune OS, so stay tuned! [1] https://github.com/cl91/NeptuneOS/releases/tag/v0.3.0003 [2] https://www.youtube.com/watch?v=ejNeS7A5qq0 [3] https://github.com/microsoft/Windows-driver-samples/tree/main/storage [4] https://github.com/JoeHsu092015/Windows-NVMe-driver --- Dr. Chang Liu, PhD. github.com/cl91/NeptuneOS

1 0

seL4 developer hangout reminder
by Birgit Brecknell 08 Dec '25

08 Dec '25

Hi all A friendly reminder that the seL4 developer hangout is on again this week. Wed 10 Dec, 7: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 <mailto:birgit@sel4.systems> bbrcknl(a)gmail.com <mailto:bbrcknl@gmail.com>

1 0

next seL4 TSC meeting Dec 3 (Dec 2 in US)
by Gerwin Klein 02 Dec '25

02 Dec '25

The Technical Steering Committee (TSC) of the seL4 Foundation will hold its next public meting on: - Sydney: Wed, 3 Dec, 6pm - Central Europe: Wed, 3 Dec, 8am - US West Coast (LA/SF): Tue, 2 Dec, 11pm See also the seL4 calendar feed available from here: https://sel4.systems/stay-informed.html The meeting is by Zoom, and you can join from here: https://unsw.zoom.us/j/89019527332 Anyone interested can join the meeting and listen to the discussion and request to speak, which will be granted if time permits. Only TSC members can vote. The seL4 code of conduct applies to the meeting [1]. The agenda for the meeting so far is: - action items from last meeting - adopting TSC charter for the new seL4 Foundation organisation - discuss/vote on open RFCs: https://github.com/seL4/rfcs/pulls We are not likely to get through all of the RFCs in this meeting. If you have an RFC open and want to facilitate it moving forward, please leave a comment that summarises the discussion so far so we can pick up there in the meeting. If there are other items that I missed or you think should be on the agenda, please let me know. If we can't get to an item this time, we can still schedule another meeting. Cheers, Gerwin (TSC chair) [1]: https://sel4.systems/Contribute/conduct.html This email and any files transmitted with it may contain confidential information. If you believe you have received this email or any of its contents in error, please notify me immediately by return email and destroy this email. Do not use, disseminate, forward, print or copy any contents of an email received in error.

1 0

New release of seL4, Microkit, CAmkES, capDL and Rust support
by Gerwin Klein 27 Nov '25

27 Nov '25

We’re pleased to announce the release of - seL4 14.0.0: The seL4 microkernel https://docs.sel4.systems/releases/sel4/14.0.0 - Microkit 2.1.0: The seL4 Microkit for building static-architecture systems https://docs.sel4.systems/releases/microkit/2.1.0 - CAmkES 3.11.1: Component Architecture for microkernel-based Embedded Systems https://docs.sel4.systems/releases/camkes/camkes-3.11.1 - capDL 0.4.0: Tools for generating, parsing and loading capability distribution specifications https://docs.sel4.systems/releases/capdl/0.4.0 - rust-sel4 3.0.0: Rust support for seL4 userspace. See the Rust section on the seL4 docsite for more information. https://github.com/seL4/rust-sel4/releases/tag/v3.0.0 seL4 14.0.0 and the corresponding Rust support come with new features and will require updates if you are using the seL4 API directly. Microkit and CAmkES abstract those and should not require any update of user code compared to Microkit 2.0.1 and CAmkES 3.11.1. Enjoy! Gerwin

1 0