- Devel - lists.sel4.systems

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 2

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

seL4 developer hangout reminder
by Birgit Brecknell 07 Dec '25

07 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

seL4 developer hangout reminder
by Birgit Brecknell 23 Nov '25

23 Nov '25

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

question about the seL4/camkes-vm-examples
by PX 20 Nov '25

20 Nov '25

Hi,All I am trying to build the seL4 VMM example for the qemu-arm-virt platform from seL4/camkes-vm-exmaples. I can build the vmm image successfully, but I cannot run the image. Here are what I did: 1. I use the "../init-build.sh -DCAMKES_VM_APP=vm_minimal -DPLATFORM=qemu-arm-virt" command. 2. ninja After these two steps, the vmm image, capdl-loader-image-arm-qemu-arm-virt is successfully built. But when I run the generated scripts, ./simulate, to run the VMM on qemu, the vmm fails to boot up. The error message is attached below. I use Ubuntu 20.04 and QEMU emulator version 4.2.1. Do I miss something here? Do I use the correct version of the building environment? Any help would be appreciated! ./simulate ./simulate: QEMU command: qemu-system-arm -machine virt,virtualization=on,highmem=off,secure=off -cpu cortex-a15 -nographic -m size=2048 -kernel images/capdl-loader-image-arm-qemu-arm-virt ELF-loader started on CPU: ARM Ltd. Cortex-A15 r2p1 paddr=[61805000..62c02ebf] No DTB passed in from boot loader. Looking for DTB in CPIO archive...found at 6192264c. Loaded DTB from 6192264c. paddr=[60042000..60043fff] ELF-loading image 'kernel' to 60000000 paddr=[60000000..60041fff] vaddr=[e0000000..e0041fff] virt_entry=e0000000 ELF-loading image 'capdl-loader' to 60044000 paddr=[60044000..6140cfff] vaddr=[10000..13d8fff] virt_entry=1880c Enabling hypervisor MMU and paging Jumping to kernel-image entry point... Bootstrapping kernel Warning: Could not infer GIC interrupt target ID, assuming 0. available phys memory regions: 1 [60000000..c0000000] reserved virt address space regions: 4 [e0000000..e0042000] [e0042000..e0043da9] [e0044000..e140d000] [ff000000..ff200000] Booting all finished, dropped to user space *<<*seL4(CPU 0)* [decodeUntypedInvocation/205 T0xffc13400 "rootserver" @1070c]: Untyped Retype: Insufficient memory (1 * 33554432 bytes needed, 0 bytes available).>>* *<<*seL4(CPU 0)* [decodeUntypedInvocation/205 T0xffc13400 "rootserver" @1070c]: Untyped Retype: Insufficient memory (1 * 16777216 bytes needed, 0 bytes available).>>* *<<*seL4(CPU 0)* [decodeUntypedInvocation/205 T0xffc13400 "rootserver" @1070c]: Untyped Retype: Insufficient memory (1 * 16777216 bytes needed, 0 bytes available).>>* *<<*seL4(CPU 0)* [decodeUntypedInvocation/205 T0xffc13400 "rootserver" @1070c]: Untyped Retype: Insufficient memory (1 * 2097152 bytes needed, 0 bytes available).>>* *<<*seL4(CPU 0)* [decodeUntypedInvocation/205 T0xffc13400 "rootserver" @1070c]: Untyped Retype: Insufficient memory (1 * 65536 bytes needed, 0 bytes available).>>* run@main.c:1332 Invalid 'num_vcpus' attribute setting: Exceeds maximum number of supported nodes. Capping value to CONFIG_MAX_NUM_NODES (1) install_vm_devices@main.c:704 module name: map_frame_hack install_vm_devices@main.c:704 module name: init_ram Loading Kernel: 'linux' Loading Initrd: 'linux-initrd' Loading Generated DTB -------- *Pagefault from [vm0]: read prefetch fault @ PC: 0x4 IPA: 0x4, FSR: 0x6* *Context:* *r0: 0x0* *r1: 0xffffffff* *r2: 0x4f000000* *r3: 0x0* *r4: 0x0* *r5: 0x0* *r6: 0x0* *r7: 0x0* *r8: 0x0* *r9: 0x0* *r10: 0x0* *r11: 0x0* *r12: 0x0* *pc: 0x4* *r14: 0x0* *sp: 0x0* *cpsr: 0x9b* m-------- main_continued@main.c:1310 Failed to run VM Halting...

5 7

Trustworthy Systems releases LionsOS based firewall as a community project
by Courtney Darville 13 Nov '25

13 Nov '25

Hi all TS is proud to announce the release of a new proof-of-concept firewall running on LionsOS. You can find more details in the announcement on the TS website here<https://trustworthy.systems/content/news/#lionsos_firewall_release_25>. We are aiming to make this a collaborative project with the community! 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