- Devel - lists.sel4.systems

seL4 developer hangout reminder
by Birgit Brecknell 15 Mar '26

15 Mar '26

Hi all A friendly reminder that the seL4 developer hangout is on again this week. Tue 17 Mar, 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

seL4 developer hangout reminder
by Birgit Brecknell 01 Mar '26

01 Mar '26

Hi all A friendly reminder that the seL4 developer hangout is on again this week. Wed 4 Mar, 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

seL4 developer hangout reminder
by Birgit Brecknell 15 Feb '26

15 Feb '26

Hi all A friendly reminder that the seL4 developer hangout is on again this week. Tue 17 Feb, 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 11 Feb '26

11 Feb '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 4

seL4 developer hangout reminder
by Birgit Brecknell 01 Feb '26

01 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 18 Jan '26

18 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

seL4 developer hangout reminder
by Birgit Brecknell 04 Jan '26

04 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