January 2026 - Devel - lists.sel4.systems

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

** 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