- Devel - lists.sel4.systems

QSOE: QNX-inspired OS with dual-kernel architecture (custom kernel & seL4)
by Yuri Zaporozhets 23 Jun '26

23 Jun '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 0

RFC: Enabling uROS on seL4
by HHN 22 Jun '26

22 Jun '26

Hi Everyone, I have recently been experimenting with porting uROS to seL4. uROS (micro-ROS) is a very minimal version of ROS (Robot Operating System) - a well known robotics middleware suite. I have implemented the micro-ROS examples <https://github.com/micro-ROS/micro-ROS-demos/tree/kilted/rclc> and the necessary system to run them on seL4 over here <https://github.com/Johan511/sel4_uros>. A high level explanation of the work can be found here <https://johan511.github.io/posts/2025-01-19-uros-on-sel4/>. I do not have any prior experience with Operating system development or with ROS, so any critiques are much appreciated. Thank you -- Hari Hara Naveen

2 2

seL4 developer hangout reminder
by Birgit Brecknell 22 Jun '26

22 Jun '26

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

1 0

libsel4 status
by Yanfeng Liu 02 Jun '26

02 Jun '26

Dear experts, It seems that currently libsel4 has many inlined functions thus user space code size is large. I am wondering if this is really necessary? If current libsel4 is not for production use, then it doesnt matter. Otherwise I am wondering if we need support size optimized config as well? I am hoping that libsel4 changes wont affect kernel verification? Regards, yf

3 4

seL4 developer hangout reminder
by Birgit Brecknell 25 May '26

25 May '26

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

1 0

Question about ASpec → ExecSpec session dependency and shared-types design choice
by li-jun zhang 20 May '26

20 May '26

shared-types design choice Hi seL4 verification team, my name is Li-Jun Zhang, a PDH student form Nanjing University. I'm studying the structure of spec/ROOT and have a question about a design choice I'd like to understand before considering whether it's worth trying to change. The observation ASpec is declared in spec/ROOT as session ASpec in "abstract" = Word_Lib + sessions "HOL-Library" Lib ExecSpec ... Across the codebase there are nine direct imports "ExecSpec.X" from spec-side files, through five targets: | Imported ExecSpec theory | Importing spec-side theory | | --- | --- | | ExecSpec.MachineTypes | CKernel.Kernel_C, CSpec.Kernel_C, ExecSpec.MachineMonad | | ExecSpec.InvocationLabels_H | ASpec.ArchDecode_A, ASpec.Decode_A | | ExecSpec.Event_H | ASpec.Syscall_A, DSpec.Syscall_D | | ExecSpec.Arch_Structs_B | ASpec.Arch_Structs_A | | ExecSpec.ArchLabelFuns_H | ASpec.InvocationLabels_A | Combined with the sessions ExecSpec declaration, this means any Haskell prototype edit transitively invalidates ASpec and AInvs builds — even when the edit doesn't touch any of the five shared targets, because sessions ExecSpec causes ExecSpec's whole content to be source-re-executed inside ASpec's ML state. The skeleton file spec/design/skel/ARM/Arch_Structs_B.thy carries the comment (* Architecture-specific data types shared by spec and abstract. *) which suggests these targets are understood as cross-pillar shared, yet they physically live inside the Haskell-derived ExecSpec session. The comment dates back to commit 2a03e81 (the initial open-source release in 2014), and the sessions ExecSpec line has survived multiple subsequent ROOT reorganizations (e.g. the 2018 session-qualified-imports work and the 2020-10 new ROOT requirements reorg), so I assume the structure is intentional rather than incidental. The hypothetical change Suppose the closure of the five shared targets within ExecSpec (12 theories total: MachineTypes, MachineMonad, MachineOps, MachineExports, Platform, Kernel_Config, Setup_Locale, Event_H, ArchInvocationLabels_H, InvocationLabels_H, ArchLabelFuns_H, Arch_Structs_B) were moved into a base KernelTypes session, with ASpec and ExecSpec both reparented to + KernelTypes. Then: sessions ExecSpec could be removed from ASpec's ROOT entry. A Haskell-side edit that doesn't touch the 12 shared theories would no longer invalidate ASpec / AInvs. Type identity is preserved as long as the moved files keep global_naming ARM_H — the fully qualified names (ARM_H.arm_vspace_region_use, etc.) referenced by downstream are unchanged. My question Was an extraction of this kind considered when the current structure was designed (presumably pre-2014, given the comment dates from the initial release)? Are there constraints — generation-pipeline output paths, type-equality concerns beyond the global_naming trick, methodological coupling between Haskell-as-canonical-source and the abstract spec, downstream tooling that references the ExecSpec.X FQNs, or anything else — that make the current sessions ExecSpec structure the deliberate choice? I'd rather not pursue a refactor that's already been considered and rejected for a reason I'm not seeing. Pointers to prior discussion (mailing-list threads, design notes, PRs) would be very helpful. Thanks Li-Jun Zhang

2 2

seL4 developer hangout reminder
by Birgit Brecknell 11 May '26

11 May '26

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

1 0

seL4 developer hangout reminder
by Birgit Brecknell 24 Apr '26

24 Apr '26

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

1 0

Last day to submit a talk proposal to the sel4 summit!
by June Andronick 21 Apr '26

21 Apr '26

It only requires an abstract describing your talk proposal. https://form.jotform.com/260147181364858 Looking forward to your submissions. Cheers, June

1 1

seL4 summit 2026: one week to go to submit a talk
by Birgit Brecknell 13 Apr '26

13 Apr '26

One week to go to submit a talk [0] for the seL4 Summit 2026 [1]! If you’d like to submit a talk, please upload an abstract of one page or less to the submission portal [2]. **Abstracts are due on 20 April 2026.** **NEW!** The 2026 edition of the seL4 summit will feature a **full first day** dedicated to **applications, overviews, and perspectives** on seL4-based systems and formally verified software in the real world. This will be followed by Days 2 and 3 focusing on more technical development, research, reports, and discussions. We are particularly keen to **welcome people who are new to seL4** or still developing their familiarity with the technology. The event will offer an **ideal opportunity to gain a high-level view of the landscape and ecosystem** of seL4 and its associated tools, frameworks and languages, as well as formally verified software in general, and to take stock of the latest updates. The seL4 Summit 2026 will be held 1 - 3 September 2026 at the Hyatt Regency Vancouver, Vancouver, Canada. The summit will be an in-person event. We’re looking forward to many exciting proposals! [0] https://sel4.systems/Summit/2026/cfp [1] https://sel4.systems/Summit/2026/ [2] https://form.jotform.com/260147181364858 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 13 Apr '26

13 Apr '26

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

1 0

New release of seL4, Microkit, CAmkES, capDL and Rust support
by Gerwin Klein 31 Mar '26

31 Mar '26

We're pleased to announce the release of - seL4 15.0.0: The seL4 microkernel https://docs.sel4.systems/releases/sel4/15.0.0 - Microkit 2.2.0: The seL4 Microkit for building static-architecture systems https://docs.sel4.systems/releases/microkit/2.2.0 - CAmkES 3.12.0: Component Architecture for microkernel-based Embedded Systems https://docs.sel4.systems/releases/camkes/camkes-3.12.0 - capDL 0.5.0: Tools for generating, parsing and loading capability distribution specifications https://docs.sel4.systems/releases/capdl/0.5.0 - rust-sel4 4.0.0: Rust support for seL4 userspace https://github.com/seL4/rust-sel4/releases/tag/v4.0.0 seL4 15.0.0 and the corresponding Rust support come with new features and will require updates if you are using the seL4 API directly. CAmkES and the capDL tool add domain schedules as a new feature and applications will need updates if they use the seL4 domain scheduler. The Microkit release should not require any update of user code compared to Microkit 2.1.0. Enjoy! Gerwin

1 0

seL4 developer hangout reminder
by Birgit Brecknell 30 Mar '26

30 Mar '26

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

16 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 02 Mar '26

02 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 16 Feb '26

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

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

seL4 developer hangout reminder
by Birgit Brecknell 24 Nov '25

24 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

seL4 developer hangout reminder
by Birgit Brecknell 10 Nov '25

10 Nov '25

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

FOSDEM’26: Microkernel and Component-Based OS - Call for Papers
by Alexander Boettcher 04 Nov '25

04 Nov '25

Hello, the planning started for the next FOSDEM 2026 and my colleagues managed to get a devroom, https://fosdem.org/2026/news/2025-10-31-devrooms-announced They are looking for great talks and demos. The “call for participation” (CfP) follows: We are happy to announce the CfP for the "Microkernel and Component-Based OS" devroom at the upcoming FOSDEM 2026. Developers and users of various free and open-source microkernel-based and component-based operating systems will meet again at FOSDEM during the weekend of January 31st and February 1st 2026 and will share a developer room. The Microkernel and Component-Based OS devroom is currently looking for your participation in the form of proposals for talks, demos and other related activities. Possible topics for the devroom include, but are not limited to: * Introduction of a specific OS or framework * Design of subsystems and the general architecture of an OS * Languages, tools and toolchains used * Enabling support for hardware architectures, devices and programming languages * Development processes, debugging * Maintenance, testing and release engineering * Safety, security and robustness * Trends and challenges * Research and open questions * Community and governance * Use cases, experiences and status updates * Best practices and lessons learned * Live demos Important Dates The deadline for submitting proposals is December 1, 2025 (23:55 CET). Please use the FOSDEM website at https://fosdem.org/submit, select the track "Microkernel and Component-Based OS" and include at least the following information: * Title of your proposal * Short abstract (one or two paragraphs) * Duration (20 - 30 minutes, including demos and Q&A) * Your full name * Your short bio The devroom schedule (with accepted talks) will be announced on the devroom website at https://fosdem.org/2026/schedule/track/microkernel by December 15, 2025. The schedule will also be posted to the devroom mailing list and the speakers will be notified via email. Like previous years, the devroom will take place as an in-person event at the ULB Campus Solbosch in Brussels, Belgium during the second half of February 1, 2026 (Sunday). Due to the high number of submissions that FOSDEM received again this year, our devroom has only been allocated half a day. Therefore, the final decision on the duration of the talks will be made by the devroom organizers based on the number of accepted proposals. Given these restrictions, eight to nine half hour slots with a speaking time of 20 to 25 minutes and 5 to 10 minutes of Q&A form the upper limit. Requirements The communication language of the devroom is English. All content must relate to free and open-source software. By participating in the event, you agree to the publication of your talk recordings, slides and other content provided under the same CC-BY license as all other FOSDEM content. All participants are expected to adhere to the Code of Conduct: https://fosdem.org/2026/practical/conduct/ Contact For the 2026 edition, the organizers of the devroom are * Sebastian Sumpf (sebastian.sumpf [at] genode-labs.com) * Josef Söntgen (josef.soentgen [at] genode-labs.com) For any comments, questions and suggestions, please do not hesitate to contact us directly or via microkernel-devroom-manager at fosdem.org. Announcements and inquiries are additionally available through the devroom mailing list https://lists.fosdem.org/listinfo/microkernel-devroom About the Devroom Since the first Microkernel OS Devroom at FOSDEM 2012, this devroom has been a part of each subsequent FOSDEM (with slight variations of the name). The focus gradually widened to include component-based and other operating systems. It has now become somewhat of a tradition for the open-source operating systems community, a kind of "extended family meeting" and it is one of the very few places where microkernel and operating-system enthusiasts meet regularly. To date, over two dozen projects have participated in one way or another. Many of the projects face similar challenges but come up with partially different solutions. Therefore, the goal of the devroom is to bring the various projects together, let them exchange ideas, cross-pollinate and socialize. As in the past, the devroom will offer the stage both to established community members and to newcomers. Our goal is to select talks in an inclusive manner and to create a balanced and unbiased schedule, while keeping the quality of the devroom as high as in previous years. About FOSDEM FOSDEM is a two-day conference organized by volunteers to promote the widespread use of free and open-source software. FOSDEM is widely recognized as one of the largest and best such events worldwide. FOSDEM covers a wide spectrum of free and open-source software and hardware projects and offers a platform for people to collaborate. To this end, FOSDEM has set up developer rooms (devrooms) where teams can meet and showcase their projects. Devrooms are a place for teams to discuss, hack and publicly present new ideas, latest results, lightning talks, news and proposals. Besides developer rooms, FOSDEM also offers main tracks, lightning talks, certification exams and project stands. In recent years, FOSDEM has been hosting more than 5000 developers annually at the ULB Solbosch Campus in Brussels, Belgium. The participation in FOSDEM is totally free and requires no registration, although the organizers gratefully accept donations and sponsorship. Devroom Dinner Over the years, it has become a tradition that devroom speakers and enthusiasts meet for dinner somewhere in Brussels after the event to continue discussions, socialize and meet old and new friends. We plan to follow that tradition in some form as well in 2026 and will inform you about the exact arrangements later. Hope to see all of you in Brussels! -- Alexander Boettcher Genode Labs https://www.genodians.org - https://www.genode.org

1 0

Sculpt 25.10 with seL4 image
by Alexander Boettcher 03 Nov '25

03 Nov '25

Hello, last week Genode released a new version of its open source OS - Sculpt OS 25.10 [0]. I took the opportunity to craft an PC image that also contains an (unofficial and experimental) Sculpt variant based upon seL4 as kernel [1]. The variant reflects to large degree the state I presented live [2,3] on the seL4 summit 2025 [4], beside that it is now based upon seL4 13.0 instead of 12.3. In case you are interested, feel free to check out [1] to run seL4 yourself with an interactive dynamic OS. Cheers, Alex. [0] https://genode.org/download/sculpt [1] https://genodians.org/alex-ab/2025-11-02-sculpt-multi-kernel [2] https://www.youtube.com/watch?v=N624i4X1UDw [3] https://sel4.systems/Summit/2025/abstracts2025.html#a-sculpt-os [4] https://sel4.systems/Summit/2025/ -- Alexander Boettcher Genode Labs https://www.genodians.org - https://www.genode.org

1 0

[RFC] New CAmkES-VM Example: supermicro_wg (Secure Communication using WireGuard)
by Alberto Lange 31 Oct '25

31 Oct '25

Hi all, As part of my final project in Telecommunications Engineering, I’ve been developing a new CAmkES-VM example that demonstrates secure communication between two instances of an encrypter application. The draft is available here: https://github.com/adl09/camkes-vm-examples/tree/master/apps/x86/supermicro… The supermicro_wg example extends zmq_samples and integrates WireGuard between three Linux 6.1 VMs. It runs on both QEMU and Supermicro E300-9D hardware with PCI passthrough. Since I’d like to make a PR of this work, I’d appreciate any feedback. Additionally, regarding Chris’s post on virtio-net for multicore ARM, I’ve applied that code to this example to resolve errors related to virtqueue memory size. Since I didn’t see a PR associated with that code, would it be appropriate for me to base a PR on it to contribute improvements in the x86 VMM, even though it isn’t my original work? I’d prefer if the original author submitted it, but I’m happy to help integrate or adapt it if needed. Best regards, Alberto Daniel Lange Instituto Balseiro - INVAP

1 0

seL4 developer hangout reminder
by Birgit Brecknell 27 Oct '25

27 Oct '25

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

"HVC is not supported for PSCI!" error for SMP on QEMU
by Jake Hamby 24 Oct '25

24 Oct '25

I've just started looking at seL4 for a hobby project to port RISC OS to run on 64-bit ARM. Since the OS is written primarily in 32-bit ARM assembly language, that means rewriting a lot of code in C, which is fine since I won't be having to write the supervisor-mode code that seL4 handles (the most difficult part to get right). I'm still working through the seL4 tutorials, and I'm sure I'll have more questions later, but here's an easy one that maybe someone can provide context for. When I tried running a tutorial in QEMU with SMP enabled, it failed with "HVC is not supported for PSCI!" Some investigation revealed that ARM has two different opcodes to make the same calls to the PSCI interface to turn on the other CPU cores. The only difference is HVC goes to EL2 and SMC goes to EL3. As part of the build, QEMU dumps a device tree that specifically defines "hvc" as the method to use. I also noticed the Raspberry Pi device trees have no "psci' nodes. I can patch seL4 to only work with HVC by patching the check and the assembly file to use "hvc" instead of "smc" but it'd be nice if there were a build config option to specify one or the other method for making PSCI calls, and then fail at runtime if the other method was found, especially since QEMU is so popular for testing that I assume people run into this often. It'd be a small #ifdef to require and use one or the other opcode. The one area of seL4 that I know I will need to modify will be to add a 32-bit ARM mode for running existing RISC OS software and modules. The only special criteria it needs to have is to route all SWI (SVC) calls to a fault handler so I can pass them to either a 32-bit handler or to the new 64-bit SWI handlers that I'll hopefully be able to start porting one at a time from the original A32 code. The 32-bit SWI handler can get/set the input/output parameters from the machine registers in the TCB, so that part's straightforward. I'll need to do some fakery for 32-bit code that wants to run in supervisor mode, to fake success when it calls privileged instructions. I'll know more as I continue designing and start implementing code. Unfortunately there'll eventually need to be an A32/T32 emulation mode of some sort for 64-bit only ARM CPUs like Apple's M-series, but that can come later, and I can use QEMU's CPU emulation until then (as opposed to hypervisor mode with "-accel hvf", which is 64-bit only). Also, I know the Raspberry Pi 5 that I want to support can run 32-bit ARM code at EL0 only, which is all I need. If anyone has suggestions or can see some fatal flaws in my assumptions, please let me know. Best regards, Jake Hamby

4 5

Not getting a verification email for Mattermost
by Koo Zhengqun 23 Oct '25

23 Oct '25

Hi all, I've signed up for the Trustworthy Systems Mattermost, but it's been a few days and I still haven't received a verification email. Yours sincerely, Zhengqun Koo

2 1

Re: [seL4 Announce] seL4 summit 2026: location survey
by Birgit Brecknell 20 Oct '25

20 Oct '25

Just a friendly reminder to fill in the survey about summit locations for 2026. https://form.jotform.com/252117628736865 *Please do so by 26 Oct 2025.* Feel free to forward to anyone you believe may want to attend the seL4 summit [0] next year. [0] https://sel4.systems/Summit On Mon, 13 Oct 2025 at 19:18, Announcements about seL4 -- low volume list <announce(a)sel4.systems> wrote: > After wrapping up a successful seL4 summit 2025 [0], we are now preparing for the seL4 summit 2026! The summit be in Canada, around Sep 2026. > > We have started investigating options for cities, and would like your feedback. We would greatly appreciate it if you could fill in this very short survey to tell us your opinions: > > https://form.jotform.com/252117628736865 > > *Please do so by 26 Oct 2025.* > > Feel free to forward to anyone you believe may want to attend the summit next year. > > [0] https://sel4.systems/Summit/2025/ > > 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 <mailto:birgit@sel4.systems>> > bbrcknl(a)gmail.com <mailto:bbrcknl@gmail.com> <mailto:bbrcknl@gmail.com <mailto:bbrcknl@gmail.com>> > _______________________________________________ > Announce mailing list -- announce(a)sel4.systems > To unsubscribe send an email to announce-leave(a)sel4.systems

1 0

seL4 summit 2026: location survey
by Birgit Brecknell 13 Oct '25

13 Oct '25

After wrapping up a successful seL4 summit 2025 [0], we are now preparing for the seL4 summit 2026! The summit be in Canada, around Sep 2026. We have started investigating options for cities, and would like your feedback. We would greatly appreciate it if you could fill in this very short survey to tell us your opinions: https://form.jotform.com/252117628736865 *Please do so by 26 Oct 2025.* Feel free to forward to anyone you believe may want to attend the summit next year. [0] https://sel4.systems/Summit/2025/ 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

Porting seL4 to STM32MP157
by Hugo V.C. 13 Oct '25

13 Oct '25

Hi, I want to port seL4 to STM32MP157 platform. I'm reading this: https://docs.sel4.systems/projects/sel4/porting.html and honestly its being a show stopper for me. Any plan to show, step by step (without assumptions) and with a real example, how to do that? Best,

3 4

seL4 developer hangout reminder
by Birgit Brecknell 13 Oct '25

13 Oct '25

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

Summit 2025: Multikernel BoF
by Daniel Schwyn 08 Oct '25

08 Oct '25

Dear all, Attached you will find the notes from the Birds of a feather session on the multikernel at the summit in Prague. Please let me know if something is missing or misrepresented. Best regards, Daniel

2 2

seL4 vs QNX and Linux benchmarks
by Andrew Warkentin 07 Oct '25

07 Oct '25

Somebody in the Zoom call the other day (IIRC it was Gernot) said that seL4 IPC is considerably faster than QNX IPC, but it seems that QNX is somehow faster in a simple benchmarking experiment in which a client repeatedly sends messages to a bit-bucket server, using the TSC to determine timing. I'm running both QNX and seL4 under identical VirtualBox configurations with a single core. I'm using a QNX 6.3.1 x86-32 image i have in my collection (x86-64 support was only added in 7.0; this is the most recent image I have with dev tools installed). The seL4 version I'm using is from February 2022 and is built for x86-64 with MCS enabled (the priority of the threads is 255, and both the timeslice and budget are the initial thread default of 5 ms). My benchmark times a loop of 10000 RPCs; for QNX it's just using the regular read() function on /dev/null or a custom server that also acts like /dev/null but forces a copy of the message into a server-provided buffer, and for seL4 I'm directly calling Send()/Recv()/Reply(). I've also tested Linux's /dev/null, and QNX's implementation actually seems somewhat faster than it (for the system /dev/null; the custom server's best case seems only slightly worse than under Linux). Under QNX and Linux I'm running a C implementation of the benchmark and under seL4 I tried both C and Rust implementations (which have very similar performance). The messages on QNX and Linux are 100 bytes, and on seL4 they are 2 words, which should be hitting the fast path. Here are the best and worst cases I got: seL4: 0.114-0.136s QNX, custom null server: 0.006-0.063s QNX, system null server: 0.002-0.022s Linux: 0.004-0.005s Has anyone else benchmarked seL4 IPC against that of QNX and gotten better (or comparable) results for seL4, unlike what I got? Is synchronous IPC just less optimized under seL4 than QNX?

6 13

seL4 developer hangout reminder
by Birgit Brecknell 29 Sep '25

29 Sep '25

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

1 0

Systems Researcher Position
by Yanyan Shen 24 Sep '25

24 Sep '25

Hi seL4 developers NIO uses seL4 as the kernel for the vehicle operating system, and we are seeking a systems software researcher / developer to join the team. Please see the job description. [https://nio.wd3.myworkdayjobs.com/NIO_Careers/job/San-Jose-US/Systems-Softw…] If you enjoy building systems from scratch, writing high quality system code, optimizing performance, turning your research ideas into awesome real-world products, and shaping the future of systems software for intelligent EVs, the position is for you. Please drop me an email if you would like to know more. Looking forward to hearing from you. Regards, Yanyan [Banner]<http://www.nio.io> This email and any files transmitted with it are confidential and intended solely for the use of the individual or entity to whom they are addressed. You may NOT use, disclose, copy or disseminate this information. If you have received this email in error, please notify the sender and destroy all copies of the original message and all attachments. Please note that any views or opinions presented in this email are solely those of the author and do not necessarily represent those of the company. Finally, the recipient should check this email and any attachments for the presence of viruses. The company accepts no liability for any damage caused by any virus transmitted by this email.

1 0

seL4 developer hangout reminder
by Birgit Brecknell 15 Sep '25

15 Sep '25

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

1 0

Kernel use of MPIDR_EL1 register on ARM
by Julia Vassiliki 10 Sep '25

10 Sep '25

For ARM platforms, the hardware provides access to the MPIDR ("Multiprocessor Identification Register") [1], which, amongst other things, provides access to 2 (or 3, for AArch64) affinity levels: Aff0, Aff1, Aff2, and possibly Aff3. However, seL4 instead seems to gather the CPU index from a loader-set `tpidr_el1`. /* tpidr_el1 has the logic ID of the core, starting from 0 */ mrs x6, tpidr_el1 /* Set the sp for each core assuming linear indices */ ldr x5, =BIT(CONFIG_KERNEL_STACK_BITS) mul x5, x5, x6 This is then overwritten later. with the kernel stack address. Is there any reasoning for why it was done this way? The elfloader [3] then has read the MPIDR and converted it to TPIDR_EL1 for the kernel, and it uses a generated table to map the MPIDR IDs to "logical core IDs" [4]. Here is the boot log for the TX2, which does use non-contiguous Aff0 IDs. Boot cpu id = 0x100, index=2 Core 257 is up with logic id 1 Core 258 is up with logic id 2 Core 259 is up with logic id 3 Enabling MMU and paging Of note here is 2 things: 1. That the ARM PSCI specification [5], for "target_cpu" when calling PSCI_ON or OFF methods (such as done in the elfloader) expects a MPIDR-like ID (I say "like" because it is with the "U" and "MT" bits masked out). In its current state, the seL4_BootInfo provided ID is instead the logical ID, which means that there's no way to see the value of MPIDR from userspace. 2. The GICv3 uses MPIDR affinity values when sending IPIs, and so the kernel does actually maintain a "mpidr_map" which wouldn't be necessary if everything talked in terms of MPIDRs. (It would still be required for other reasons on SMP as opposed to multikernel, though). BOOT_CODE void cpu_initLocalIRQController(void) { word_t mpidr = 0; SYSTEM_READ_WORD(MPIDR, mpidr); mpidr_map[CURRENT_CPU_INDEX()] = mpidr; active_irq[CURRENT_CPU_INDEX()] = IRQ_NONE; gicr_init(); cpu_iface_init(); } In the spirit of being a minimal hardware abstraction, I feel that it makes more sense for the kernel's APIs to be in terms of MPIDRs [6], but that it would probably be a breaking change. Internally, aside from this, it makes *more* sense for the kernel to think in terms of MPIDRs for the core values, rather than a "logical core ID". Some context for how this is represented in the device trees: In the device tree documentation 'Documentation/devicetree/bindings/arm/cpus.yaml' [2] the `<reg>` field of the cpus node tells the values of each of the CPU nodes; mapping the affinities (possibly non-contiguous) to a contiguous CPU index could be done with a build-time lookup table. For example, here is the first part of the OdroidC4 device tree, which tells us that node 0 is Aff0=0, Aff1=0. cpus { #address-cells = <0x02>; #size-cells = <0x00>; cpu@0 { device_type = "cpu"; reg = <0x00 0x00>; }; /* etc */ } [1]: https://arm.jonpalmisc.com/latest_sysreg/AArch64-mpidr_el1 [2] https://www.kernel.org/doc/Documentation/devicetree/bindings/arm/cpus.yaml [3]: https://github.com/seL4/seL4_tools/blob/26f94df7e97a04f8ee49c1e94a0aa120365… [4]: https://github.com/seL4/seL4_tools/blob/master/elfloader-tool/src/arch-arm/… [5]: https://documentation-service.arm.com/static/6703a8b8d7e4b739d817e10d [6]: So, the SMP affinity APIs, and BootInfo->nodeID field. Julia 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.

3 3

About MSI-X interrupts on x86
by Alberto Lange 06 Sep '25

06 Sep '25

Hi all, here Albert I’m working on a SuperMicro E300-9D server and trying to passthrough an Intel X557-AT2 NIC to a Linux 6.1 guest. The .camkes configuration seems to be right, here are the configs for the device (the device is correctly detected on the VM): vm2.vm_ioports = []; vm2.pci_devices = [ { "name":"outer_eth", "bus":0xb5, "dev":0x0, "fun":1, "irq":"outer_eth", "memory":[ {"paddr":0xf9000000, "size":0x01000000, "page_bits":12}, // BAR0 {"paddr":0xfb000000, "size":0x00008000, "page_bits":12}, // BAR3 ] } ]; vm2.vm_irqs = [ {"name":"outer_eth", "ioapic":0, "source":0xb, "level_trig":0, "active_low":1, "dest":12} ]; I’m seeing the following errors during boot and when bringing the interface up: [ 2.040786] i40e 0000:00:01.0: MAC address: 3c:ec:ef:d2:88:85 [ 2.090786] i40e 0000:00:01.0: MSI-X vector reservation failed: -38 [ 2.109960] i40e 0000:00:01.0: MSI-X not available, trying MSI [ 2.115660] i40e 0000:00:01.0: MSI init failed - -38 [ 2.121656] i40e 0000:00:01.0: MSI-X and MSI not available, falling back to Legacy IRQ [ 2.220802] i40e 0000:00:01.0 eth1: NIC Link is Up, 1000 Mbps Full Duplex, Flow Control: None [ 2.290774] i40e 0000:00:01.0: Features: PF-id[1] VSIs: 66 QP: 1 VxLAN Geneve PTP VEPA ... # ifconfig eth1 up [ 451.042525] i40e 0000:00:01.0 eth1: NETDEV WATCHDOG: CPU: 0: transmit queue 0 timed out 5770 ms [ 451.052764] i40e 0000:00:01.0 eth1: tx_timeout: VSI_seid: 391, Q 0, NTC: 0x0, HWB: 0x1, NTU: 0x1, TAIL: 0x1, INT: 0x0 [ 451.065876] i40e 0000:00:01.0 eth1: tx_timeout recovery level 2, txqueue 0 [ 456.082601] i40e 0000:00:01.0 eth1: NETDEV WATCHDOG: CPU: 0: transmit queue 0 timed out 10810 ms My thought is that this NIC does not work reliably with legacy IRQ mode. My question is: Is there any implementation of MSI-X interrupts for x86 in the seL4 VMM, or plans to support it? If such support exists, I would like to contribute, as I plan to share my project once it’s finished. Thanks in advance for any guidance or suggestions. Albert

3 4

Error on managing the same IRQ in 2 VM (x86) #84
by Alberto Lange 20 Aug '25

20 Aug '25

Hi! I'm working on top of the zmq_samples example, trying to set up 2 Ethernet devices on 2 of the 3 VM's. The passthrough for both VM's has been done, and both detect the NICs. For more information, this is the setup for the irqs in the camkes file: vm0.vm_irqs = [ {"name":"inner_eth", "ioapic":0, "source":0xb, "level_trig":1, "active_low":1, "dest":10} ]; vm2.vm_irqs = [ {"name":"outer_eth", "ioapic":0, "source":0xb, "level_trig":1, "active_low":1, "dest":12} ]; My problem is related to having the same IRQ11 in both e1000e devices. I can't control this; that is what QEMU provides. When I set up the first NIC in any VM, say VM0, doing ifconfig eth1 up, it works correctly, but when I try to bring up the other one, VM2, the whole system freezes for a moment. Then VM0 complains about this: [ 48.557120] irq 10: nobody cared (try booting with the "irqpoll" option) [ 48.557120] CPU: 0 PID: 0 Comm: swapper/0 Tainted: G W 4.9.337+ #19 [ 48.557120] df811f94 d08f1778 df807d00 00000000 df811fa8 d08f08e0 df807d00 00000000 [ 48.557120] d0459f68 df811fc4 d04596ec 0000000b 00000000 df807d00 00000000 d0459f68 [ 48.557120] df811fd8 d0457a55 00000000 df807d00 df807d64 df811fe8 d0457a7e df807d00 [ 48.557120] Call Trace: [ 48.557120] [ 48.557120] [] dump_stack+0x4f/0x63 [ 48.557120] [] __report_bad_irq+0x33/0x98 [ 48.557120] [] ? unmask_irq+0x22/0x22 [ 48.557120] [] note_interrupt+0x185/0x1c3 [ 48.557120] [] ? unmask_irq+0x22/0x22 [ 48.557120] [] handle_irq_event_percpu+0x31/0x38 [ 48.557120] [] handle_irq_event+0x22/0x3b [ 48.557120] [] handle_level_irq+0x52/0x80 [ 48.557120] [] handle_irq+0x91/0xb6 [ 48.557120] [ 48.557120] [ 48.557120] [] do_IRQ+0x33/0x99 [ 48.557120] [] common_interrupt+0x2c/0x34 [ 48.557120] [] ? __do_softirq+0x55/0x1a1 [ 48.557120] [] ? _local_bh_enable+0x6c/0x6c [ 48.557120] [] call_on_stack+0x40/0x46 [ 48.557120] [ 48.557120] [] ? irq_exit+0x56/0x91 [ 48.557120] [] ? do_IRQ+0x7f/0x99 [ 48.557120] [] ? common_interrupt+0x2c/0x34 [ 48.557120] [] ? default_idle+0x16/0x18 [ 48.557120] [] ? arch_cpu_idle+0xd/0xf [ 48.557120] [] ? default_idle_call+0x14/0x16 [ 48.557120] [] ? cpu_startup_entry+0xbb/0x158 [ 48.557120] [] ? rest_init+0x5d/0x5f [ 48.557120] [] ? start_kernel+0x339/0x343 [ 48.557120] [] ? i386_start_kernel+0x3e/0x40 [ 48.557120] handlers: [ 48.557120] [] e1000_intr [ 48.557120] Disabling IRQ #10 Any interruption goes to VM2; they all go to VM0 but are not intended to go to that one, so they are ignored. Any thoughts on this would be appreciated!

2 2

seL4 developer hangout reminder
by Birgit Brecknell 18 Aug '25

18 Aug '25

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

1 0

Experimental prototype of CHERI-enabled seL4 is released
by Hesham Almatary 13 Aug '25

13 Aug '25

Hello, The CHERI Alliance has released a prototype of CHERI-seL4, an experimental version of the seL4 microkernel with CHERI support. This release includes CHERI-Microkit, a lightweight userspace framework, and a set of exercises and tutorials designed to help developers explore CHERI’s potential in a real microkernel environment. The release is aimed at developers who want to build and experiment with memory-safe C/C++ software on seL4. It supports the draft CHERI-RISC-V architecture and runs on QEMU, Codasip’s X730 processor, CHERI-Toooba, and CHERI-CVA6 on FPGA. For those who are unfamiliar with CHERI, CHERI support in seL4 enables memory-safe C/C++ user-level projects and applications without having to (re)write code in languages like Rust. This complement's seL4's strong isolation between different components, enforced by the MMU and seL4's software capabilities. We welcome any feedback. Learn more: https://cheri-alliance.org/cheri-sel4-and-cheri-microkit-released/ Regards, Hesham

4 14

seL4 developer hangout reminder
by Birgit Brecknell 04 Aug '25

04 Aug '25

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

1 0

On LionsOS and Switches
by wocexeg869＠forexru.com 22 Jul '25

22 Jul '25

Many enterprise grade switches from Cisco to Juniper switches are running on Linux. That also is the case with prosumer hardware such as Ubiquiti, Mikrotik (CRS line), Aruba, etc... Wouldn't this be a good use case for LionsOS? The security of the layer 2 is an important part of the security of the overall network and it should be easier to implement compared to the firewall that is currently being worked on. Thank you for your attention to this matter!

3 2

seL4 developer hangout reminder
by Birgit Brecknell 21 Jul '25

21 Jul '25

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

1 0

seL4 developer hangout reminder
by Birgit Brecknell 07 Jul '25

07 Jul '25

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

1 0

seL4 developer hangout reminder
by Birgit Brecknell 23 Jun '25

23 Jun '25

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

Fwd: Re: I am interested in porting LionOS to X64 architecture
by Jingyao Zhou 11 Jun '25

11 Jun '25

Resend because I forgot to CC the mailing list. Begin forwarded message: From: Jingyao Zhou <jingyao.zhou(a)unsw.edu.au> Date: 5 June 2025 at 11:47:49 GMT+8 To: Peter Relich <prelich(a)intellisenseinc.com> Subject: Re: [seL4] Re: I am interested in porting LionOS to X64 architecture Hi Peter, I am glad to see that you are interested in contributing to x86 support for LionsOS! Several x86-related works/plans are going on in the Trustworthy Systems Team. For the seL4 kernel, there are pending pull requests for remappable MSI and IOAPIC supports that need to be updated and tested; we would like to add posted interrupts and MSI-x, but there are no concrete plans yet. For the x86 Microkit, we adopted Neutrality-CH's works and have been updating it (e.g. adding virtulization support). There are two major issues: * We need to figure out a nicer way to generate the machine description for x86 machines * We also need to add IOMMU supports We hope to upstream the work soon. For seL4 Device Driver Framework: we have working examples running on Supermicro servers as well as QEMU. We hope to upstream them soon as well. For adding x86 support for libvmm: the work is on hold due to the prerequisites, plus a kernel issue with multi-IOAPIC support. We will resume it as soon as possible. We apologize for the lack of information; we will keep our progress on x86 supports updated on GitHub in the future. Regards, Jade. ________________________________ From: Peter Relich via Devel <devel(a)sel4.systems> Sent: Wednesday, June 4, 2025 3:49 AM To: devel(a)sel4.systems <devel(a)sel4.systems> Subject: [seL4] Re: I am interested in porting LionOS to X64 architecture Thanks everyone. I got authorized to continue my effort, and I was looking into what is currently available. I don't have to worry about red/black channels for now, so confidentiality is not yet a priority. My main priority is to create a steel thread so that if the main operating system crashes, a giant robotic vehicle can be teleoperated or shutdown without hurting anyone. I saw that Neutrality-CH (Switzerland) had forked the Microkit library for x86 (https://github.com/Neutrality-ch/microkit) but they had only made two commits, the last one was in December 17. I tried to contact them a few weeks ago, but I didn't hear back so I'm not sure the status/funding of their project. Anyway, currently the VMM capabilities are not developed for their fork which would make deployment of an OS tedious. At first glance, it looks like I need to put some work into building a VMM into their fork by studying and then calling the seL4 vcpu, interrupt, x86_src routines into their Microkit fork? I guess my question now as I parse through everything. Is the Neutrality-CH fork the best, most recent x86 fork of the microkit? Or is there another library/fork I should consider for development? I saw that their approach for pre-generating an ELF file for the bootloader was the main obstacle for their pull request, but since I'm working on a specific Intel architecture (8th gen, uses Intel VT-x and VT-d for virtualization), I can avoid over generalizing my solution and focus on this specific application. Is there any value in extracting/porting the work performed in CAmkES x86 virtualization for the microkit x86 fork? Thanks again for all the help! -Peter ________________________________ The information contained in this e-mail and any attachments from Intellisense Systems may contain confidential and/or proprietary information, and is intended only for the named recipient to whom it was originally addressed. If you are not the intended recipient, any disclosure, distribution, or copying of this e-mail or its attachments is strictly prohibited. If you have received this e-mail in error, please notify the sender immediately by return e-mail and permanently delete the e-mail and any attachments. _______________________________________________ Devel mailing list -- devel(a)sel4.systems To unsubscribe send an email to devel-leave(a)sel4.systems Confidential communication - This email and any files transmitted with it are confidential and are intended solely for the addressee. If you are not the intended recipient, please be advised that you have received this email in error and that any use, dissemination, forwarding, printing, or copying of this email and any file attachments is strictly prohibited. If you have received this email in error, please notify me immediately by return email and destroy this email.

1 0

Re: I am interested in porting LionOS to X64 architecture
by Peter Relich 11 Jun '25

11 Jun '25

Thanks everyone. I got authorized to continue my effort, and I was looking into what is currently available. I don't have to worry about red/black channels for now, so confidentiality is not yet a priority. My main priority is to create a steel thread so that if the main operating system crashes, a giant robotic vehicle can be teleoperated or shutdown without hurting anyone. I saw that Neutrality-CH (Switzerland) had forked the Microkit library for x86 (https://github.com/Neutrality-ch/microkit) but they had only made two commits, the last one was in December 17. I tried to contact them a few weeks ago, but I didn't hear back so I'm not sure the status/funding of their project. Anyway, currently the VMM capabilities are not developed for their fork which would make deployment of an OS tedious. At first glance, it looks like I need to put some work into building a VMM into their fork by studying and then calling the seL4 vcpu, interrupt, x86_src routines into their Microkit fork? I guess my question now as I parse through everything. Is the Neutrality-CH fork the best, most recent x86 fork of the microkit? Or is there another library/fork I should consider for development? I saw that their approach for pre-generating an ELF file for the bootloader was the main obstacle for their pull request, but since I'm working on a specific Intel architecture (8th gen, uses Intel VT-x and VT-d for virtualization), I can avoid over generalizing my solution and focus on this specific application. Is there any value in extracting/porting the work performed in CAmkES x86 virtualization for the microkit x86 fork? Thanks again for all the help! -Peter ________________________________ The information contained in this e-mail and any attachments from Intellisense Systems may contain confidential and/or proprietary information, and is intended only for the named recipient to whom it was originally addressed. If you are not the intended recipient, any disclosure, distribution, or copying of this e-mail or its attachments is strictly prohibited. If you have received this e-mail in error, please notify the sender immediately by return e-mail and permanently delete the e-mail and any attachments.

2 2

Booting software on Odroid-C4
by Julia Royer 06 Jun '25

06 Jun '25

Hello, I would like to boot my Microkit software on an Odroid-C4, but I’m a bit confused about the process. Is there any tutorial available, or perhaps an existing U-Boot image that I could use? Thank you for your help. Best regards, Julia Royer

5 8

seL4 developer hangout reminder
by Birgit Brecknell 06 Jun '25

06 Jun '25

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

1 0

seL4 developer hangout reminder
by Birgit Brecknell 26 May '25

26 May '25

Hi all A friendly reminder that the seL4 developer hangout is on again this week. Wed 28 May, 8am 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 14 May '25

14 May '25

Hi all A friendly reminder that the seL4 developer hangout is on again this week. Wed 13 May, 10:00pm UTC. For your local date and time please see https://sel4.systems/contact/. 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 1

Libc on Microkit
by Julia Royer 06 May '25

06 May '25

Hello, I'm currently developing a simple communication application to explore seL4 and Microkit, and I'd like to use a C standard library (libc) in my project. I came across libsel4muslcsys and the seL4/musllibc repository. Are there any other components I should be aware of? Also, is there a specific way to integrate these into my project? Thank you for your help. Best regards, Julia Royer

2 2

Ethernet passthrough on x86 (QEMU)
by alberto.lange＠ib.edu.ar 29 Apr '25

29 Apr '25

Hi! I wanted to share another problem with you again, I hope it doesn't bother you. I'm trying to set up a small network between two simulations on QEMU of seL4 running a VM before dealing with hardware. I saw the tutorials related to Ethernet passthrough, but I'm not sure if the same approach applies when using QEMU. These are my configs for the minimal app example: vm0_config.ioports = [ {"start":0xc000, "end":0xc03f, "pci_device":0, "name":"Ethernet5"}, ]; vm0_config.pci_devices = [ { "name":"Ethernet5", "bus":0x0, "dev":0x3, "fun":0, "irq":"Ethernet5", "memory":[ {"paddr":0xfeb80000, "size":0x20000, "page_bits":12}, ], }, ]; vm0_config.irqs = [ {"name":"Ethernet5", "source":11, "level_trig":1, "active_low":1, "dest":10} ]; And checking what QEMU presents to seL4 as hardware: Bus 0, device 3, function 0: Ethernet controller: PCI device 8086:100e PCI subsystem 1af4:1100 IRQ 11, pin A BAR0: 32 bit memory at 0xfeb80000 [0xfeb9ffff]. BAR1: I/O at 0xc000 [0xc03f]. BAR6: 32 bit memory at 0xffffffffffffffff [0x0007fffe]. id "" But when I'm looking for the device on the VM: # lspci 00:00.0 Class 0600: 5e14:0042 I would appreciate any comments on this. Thanks in advance. Alberto Lange

1 0

Custom kernel for x86 VM
by alberto.lange＠ib.edu.ar 29 Apr '25

29 Apr '25

Hi! I'm Alberto, and I'm currently working on my Telecommunications Engineering thesis, which focuses on building a secure system using an seL4 virtual machine. Right now, I'm trying to use the minimal app from the camkes-vm-examples repository with a modified Linux kernel (v6.12.9) built using Buildroot. To do this, I've been replacing the kernel and rootfs files in the vm-linux/images directory with my custom ones. However, this has led to multiple errors during execution. I’d really appreciate some guidance on the correct way to integrate a custom kernel into the CAmkES VM framework. Specifically, should I be using the functions provided in the linux-source-helpers.cmake file to update the kernel and rootfs? Thanks in advance!

2 2

seL4 Summit 2025: extended deadline to submit a talk
by Birgit Brecknell 28 Apr '25

28 Apr '25

The deadline to submit a talk [0] for the seL4 Summit 2025 [1] has been extended until 2 May 2025. If you’d like to submit a talk, please upload an abstract of one page or less to the submission portal [2]. **Abstracts are due on 2 May 2025.** Also note the open invitation for a 5-minute slot to talk about your seL4 deployment [3]. The seL4 Summit 2025 will be held 3 - 5 September 2025 at the Grandior Hotel Prague, Prague, Czech Republic. The summit will be an in-person event. Registration and location details are available here [4] [0] https://sel4.systems/Foundation/Summit/2025/cfp [1] https://sel4.systems/Foundation/Summit/2025/ [2] https://form.jotform.com/250436091673861 [3] https://sel4.systems/Foundation/Summit/2025/cfp#sel4-deployment [4] https://events.linuxfoundation.org/sel4-summit/register/ 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 28 Apr '25

28 Apr '25

Hi all A friendly reminder that the seL4 developer hangout is on again this week. Wed 30 Apr, 8:00am UTC. For your local date and time please see https://sel4.systems/contact/. 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

hello_rumprun app not worked
by MOHAMAD REZA SHAFIEI 19 Apr '25

19 Apr '25

hi. i'm recently worked on sel4 with camkes framework. when i compile rumprun_hello on x86_64 platform its compiled and build correctly but when run with qemu by ./simulate script, program crashed with this errors: simple_get_extended_bootinfo_length@simple.h:600 simple_get_extended_bootinfo_length not implemented FAULT HANDLER: data fault from hello.hello_0_control (ID 0x1) on address 0x8, pc = 0x402b7f, fsr = 0x6 FAULT HANDLER: Register dump: FAULT HANDLER: rip :0x402b7f , . . so i found that this method not implemented yet so i return 0 in this method and resolved. for second problem that cause failure if trace program and i found that in "init rumprun" process the program failed in the /projects/sel4runtime/include/sel4_arch/x86_64/sel4runtime/thread_arch.h file and sel4runtime_set_tls_base method. so i read git log and in recently commit your team use sel4runtime for thread TLS, so when we run rumprun_hello, the program failed in sel4runtime_set_tls_base method. can you help me fix this bug? thanks for your attention. -- This email was Anti Virus checked by Security Gateway.

5 5

Issue when running rumprun_hello app from the CAmkES manifest
by dinukaamarasinghe817＠gmail.com 19 Apr '25

19 Apr '25

Hello all, mostly Kent, When I run the rumprun_hello app that's included in the CAmkES manifest, I encounter the following runtime errors: [...] Booting all finished, dropped to user space simple_get_extended_bootinfo_length@simple.h:608 simple_get_extended_bootinfo_length not implemented vka_cspace_alloc@vka.h:149 Unimplemented vka_alloc_object_at_maybe_dev@object.h:47 Failed to allocate cslot: error -1 init_rumprun@entry.c:306 [Cond failed: res != 0] Failed to allocate notification object This seems related to the simple->extended_bootinfo_len callback not being implemented, which causes downstream failures in object allocation (e.g. notification object). This issue appears specifically when running Rumprun-based apps. Would appreciate any insights or suggestions on how to resolve or properly set up this functionality. Note that i haven't modified any of the code here. Just tried to run the existing 'rumprun_hello' application.

1 0

Re: Register for the seL4 summit 2025
by Vasily A. Sartakov 16 Apr '25

16 Apr '25

Dear all, > Thanks for the info! A quick question for clarification: What is the difference between the Professional and the Hobbyist registration type? (Sorry if this is obvious to someone, but I'm unable to find an explicit explanation anywhere.) I guess, If you pay out of your own pocket, you are an enthusiast. if it is sponsored by your employer, you are a professional. — Dr.-Eng. V. A. Sartakov

3 2

Register for the seL4 summit 2025
by Birgit Brecknell 14 Apr '25

14 Apr '25

The seL4 summit 2025 [0] will be held in Prague, Czech Republic, 3 - 5 September 2025. The seL4 summit will cover the complete seL4 ecosystem, consisting of the verified microkernel, as well as all seL4-related technology, tools, infrastructure, products, projects, and people. Tickets include: - Participation in the 3-day conference, including talks, keynotes, seL4 updates & discussions - Networking with other seL4 experts and enthusiasts - Reception and dinner Register here [1] The early bird cut-off date is 3 August 2025. A number of informal social activities will be organised by the seL4 community for Tuesday 2 Sep 2025. Stay tuned for more info! [0] https://sel4.systems/Foundation/Summit/2025/ [1] https://events.linuxfoundation.org/sel4-summit/register/ 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>

2 1

DKernelSkimWindow=off
by Sanyou 14 Apr '25

14 Apr '25

Hi, I am testing sel4 on real Sanyou> x86 board now. I found that if we use parameter DKernelSkimWindow=off, we can see nothing on the uart. Can you give me any advice. Regards, Sanyoo

1 0

seL4 Summit 2025: one week to go to submit a talk
by Birgit Brecknell 14 Apr '25

14 Apr '25

One week to go to submit a talk [0] for the seL4 Summit 2025 [1]! If you’d like to submit a talk, please upload an abstract of one page or less to the submission portal [2]. **Abstracts are due on 21 April 2025.** Also note the open invitation for a 5-minute slot to talk about your seL4 deployment [3]. The seL4 Summit 2025 will be held 3 - 5 September 2025 at the Grandior Hotel Prague, Prague, Czech Republic. The summit will be an in-person event. Registration details to follow soon. We’re looking forward to many exciting proposals! [0] https://sel4.systems/Foundation/Summit/2025/cfp [1] https://sel4.systems/Foundation/Summit/2025/ [2] https://form.jotform.com/250436091673861 [3] https://sel4.systems/Foundation/Summit/2025/cfp#sel4-deployment 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 14 Apr '25

14 Apr '25

Hi all A friendly reminder that the seL4 developer hangout is on again this week. Tue 15 Apr, 10:00pm UTC. For your local date and time please see https://sel4.systems/contact/. 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

Running seL4 on bare-metal x86_64 PC
by saftab.rashid＠gmail.com 11 Apr '25

11 Apr '25

Hi, I am very new to sel4 and I am trying to run it bare-metal on an Intel Xeon x86_64 machine. I am following the instructions here PC99 | seL4 docs. I can run seL4 using the ./simulate script which runs the kernel under QEMU. However, I would like the run seL4 natively on my machine. After the build, I have the following images in the images/ directory. kernel-x86_64-pc99 sel4test-driver-image-x86_64-pc99 I have created a Grub2 menu entry by copying these images under /boot. However, when I boot using the created menu entry I get a black screen and I also see no output on the serial port. My Grub2 menu entry is as follows menuentry “Load seL4 VM” --class os { load_video insmod gzio insmod part_msdos insmod ext2 set root=‘(hd0,msdos2)’ multiboot /boot/kernel-x86_64-pc99 module /boot/sel4test-driver-image-x86_64-pc99 } I have also tried the multiboot2 protocol as I have an UEFI-supported system but it also doesn’t work. After booting into the seL4 VM I get a black screen and there is no output on the serial port. Any Idea what I am doing wrong?

2 2

Interactions between sDDF and libvmm
by Julia Royer 09 Apr '25

09 Apr '25

Hello, I am currently exploring libvmm and sDDF and I have a question regarding how sDDF is intended to be used in practice. From what I understand, sDDF is often seen in conjunction with libvmm in examples and documentation. My question is: Is sDDF meant to be used exclusively with libvmm, or can it also be used independently? If the latter is possible, is it considered a recommended or meaningful use case, or is the project mainly designed around integration with libvmm? Thank you for your help. Best regards, Julia Royer

2 1

seL4 Summit 2025: two weeks to go to submit a talk
by Birgit Brecknell 07 Apr '25

07 Apr '25

Two weeks to go to submit a talk [0] for the seL4 Summit 2025 [1]! If you’d like to submit a talk, please upload an abstract of one page or less to the submission portal [2]. **Abstracts are due on 21 April 2025.** Also note the open invitation for a 5-minute slot to talk about your seL4 deployment [3]. The seL4 Summit 2025 will be held 3 - 5 September 2025 at the Grandior Hotel Prague, Prague, Czech Republic. The summit will be an in-person event. Registration details to follow soon. We’re looking forward to many exciting proposals! [0] https://sel4.systems/Foundation/Summit/2025/cfp [1] https://sel4.systems/Foundation/Summit/2025/ [2] https://form.jotform.com/250436091673861 [3] https://sel4.systems/Foundation/Summit/2025/cfp#sel4-deployment 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 extensibility
by 1plus.yijia＠gmail.com 01 Apr '25

01 Apr '25

One the advantages of microkernel is the extensibility of user space components; however, doesn't the static system design eliminate this advantage? Do I miss something? I wonder if it possible to only recompile a component and replace an older one; if yes, if it possible to replace it in runtime.

2 1

seL4 developer hangout reminder
by Birgit Brecknell 31 Mar '25

31 Mar '25

Hi all A friendly reminder that the seL4 developer hangout is on again this week. Wed 2 Apr, 7:00am UTC. For your local date and time please see https://sel4.systems/contact/. 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

User-level proofs and capability revocation
by Anton Burtsev 28 Mar '25

28 Mar '25

Hi all I have a couple of questions on how user-level proofs are constructed in the seL4 ecosystem. Just to start, can someone point me to an example of a user-level proof, just so I can take a look at how specifications are exported to user processes and how everything is stitched together. But also, I'm a bit confused on what kind of assumptions are needed to build verified user-level code in the face of revocable memory. I.e., it seems that one needs to assume (and trust) that the memory of any verified (or even rather mission critical) process is never revoked. Maybe I'm wrong and missing something and you have a way in mind for how to bypass such trust. Or maybe one can argue that such trust is reasonable, which is probably true for a "flat" system in which the mission critical domain is created right from the trusted boot process or some trusted TCB above it. Yet it seems hard to argue that such trust is reasonable when the recursion is deeper, e.g., the boot process launches Linux, and then Linux tries to start some kind of a mission critical process like a microkernel-protected software TEE or something (out of its memory hence it can later revoke it). And one wants to build a proof about this TCB yet such proof needs to deal with memory that can be revoked at any time or assume that revocation is impossible. Just wandering what is the take on this. I apologize if this all is covered somewhere in seL4 docs and I just didn't dig deep enough. Thank you! Anton

7 14

seL4 libraries compatibility with Microkit
by Julia Royer 22 Mar '25

22 Mar '25

Hi, I understand that Microkit simplifies the seL4 API. However, I would like to know if it is still possible to use seL4 libraries when working with Microkit. If so, is there any benefit to doing so? Thank you in advance for your help. Kind regards, Julia Royer

2 2

seL4 developer hangout reminder
by Birgit Brecknell 17 Mar '25

17 Mar '25

Hi all A friendly reminder that the seL4 developer hangout is on again this week. Tue 18 Mar, 9:00pm UTC. For your local date and time please see https://sel4.systems/contact/. 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

Reminder: Call For Presentations for the seL4 Summit 2025
by Birgit Brecknell 14 Mar '25

14 Mar '25

Reminder: Call For Presentations [0] for the seL4 Summit 2025 [1] - Share your seL4 work - Share your seL4 experience - Share your seL4 thoughts Check the full Call For Presentations [0]. To propose a talk, upload an abstract of one page or less by **21 April 2025** to the submission portal [2]. Also note the open invitation for a 5-minute slot to talk about your seL4 deployment [3]. [0] https://sel4.systems/Foundation/Summit/2025/cfp [1] https://sel4.systems/Foundation/Summit/2025/ [2] https://form.jotform.com/250436091673861 [3] https://sel4.systems/Foundation/Summit/2025/cfp#sel4-deployment 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

Libvmm on Rasperry Pi 4B
by Julia Royer 12 Mar '25

12 Mar '25

Hello, I am currently working on a project aimed at exploring the capabilities of the seL4 microkernel and Microkit. For this purpose, I have chosen the Raspberry Pi 4B board. I noticed that libvmm is not yet supported for this platform. Do you have an estimate on when Raspberry Pi 4B might be supported? Thank you for your time and support. Kind regards, Julia Royer

2 5

Release 2.0.0 of Microkit
by Ivan Velickovic 09 Mar '25

09 Mar '25

Hello everyone, There is a new release of Microkit, version 2.0.0. This release contains various bug fixes, quality-of-life changes, features, and new board support. This is a major version bump due to a breaking change. Below the release notes, there is a section on how to upgrade from Microkit 1.4.1. You can download the pre-built SDK from GitHub: https://github.com/seL4/microkit/releases/tag/2.0.0 Ivan

5 11

seL4 for general purpose/desktop operating systems?
by Isaac Beckett 09 Mar '25

09 Mar '25

Hello! I saw Microkit 2.0 has just been released, and it’s prompted a question I’ve been thinking about since before Microkit, when CaMKes was the main thing: Both Microkit and Camkes are designed for embedded and/or static systems, where there is no detection/configuration of hardware at runtime, and in Microkit no swapping of components such as drivers. Is there any work ongoing to use seL4 for a general purpose operating system? Like, a situation where you may have e.g. PC style hardware that can have all sorts of reconfiguration between power-off and next boot, or even while booted and running. Of course this introduces a lot of attack surface, but it makes a lot more sense for a general purpose computer, rather than an embedded one. Is there any recent work/prior art on using seL4 outside of the context of deeply embedded systems? Thanks, Isaac

5 10

Deprecating old boards in the CI system
by Peter Chubb 05 Mar '25

05 Mar '25

Hi folks, There are a number of boards we currently support that we can no longer test, as the boards we had have died. Some of these have been out of production for more than five years. I'm intending to write up deprecation RFCs for any that noone is using -- please reply if you still have software you support on any of the SoCs on these boards: Arndale Exynos 5250 -- Introduced 2012, last available in 2018 Odroid X Exynos 4412 -- introduced 2012, last available 2018 Beagleboard Xm DM3730 -- introduced 2014, still available as new-old-stock, but no longer manufactured. Hikey960 Kirin 620 -- Introduced 2017, last available 2020 Inforce IFC6410 Snapdragon -- Introduced 2013; no userspace support at present -- Dr Peter Chubb https://trustworthy.systems/ Trustworthy Systems Group CSE, UNSW Core hours: Mon 8am-3pm; Wed: 8am-5pm; Fri 8am-12pm.

1 0

seL4 developer hangout reminder
by Birgit Brecknell 03 Mar '25

03 Mar '25

Hi all A friendly reminder that the seL4 developer hangout is on again this week. Wed 5 Mar, 7:00am UTC. For your local date and time please see https://sel4.systems/contact/. 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

Call For Presentations for the seL4 Summit 2025
by Birgit Brecknell 17 Feb '25

17 Feb '25

Call For Presentations [0] for the seL4 Summit 2025 [1] - Share your seL4 work - Share your seL4 experience - Share your seL4 thoughts Check the full Call For Presentations [0]. To propose a talk, upload an abstract of one page or less by 21 April 2025 to the submission portal [2]. Also note the open invitation for a 5-minute slot to talk about your seL4 deployment [3]. [0] https://sel4.systems/Foundation/Summit/2025/cfp [1] https://sel4.systems/Foundation/Summit/2025/ [2] https://form.jotform.com/250436091673861 [3] https://sel4.systems/Foundation/Summit/2025/cfp#sel4-deployment 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 17 Feb '25

17 Feb '25

Hi all A friendly reminder that the seL4 developer hangout is on again this week. Tue 18 Feb, 9:00pm UTC. For your local date and time please see https://sel4.systems/contact/. 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 03 Feb '25

03 Feb '25

Hi all A friendly reminder that the seL4 developer hangout is on again this week. Wed 5 Feb, 7:00am UTC. For your local date and time please see https://sel4.systems/contact/. 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 test on x86
by Yevgeny Lavrov 30 Jan '25

30 Jan '25

Hello, I'm new to seL4 and I'm just doing it for learning purpose. I'm trying to run seL4 test suite or simple hello world task from seL4 tutorials on the real hardware. So far I had no problems compiling seL4 test suite and running via QEMU for both x32 and x64 platforms. However, when I try to run it on the actual hardware following Running on real hardware tutorial for x86 I end up with no output at all and no error msgs that can give me a clue on where something went wrong. After compiling seL4test for x86, I ended up with two images in sel4_dir/images/ folder. Copied them over to /boot/sel4/ folder and created a new GRUB2 entry that looks like this menuentry “seL4 test suite” --class os { load video insmod gzio insmod part_msdos insmod ext2 set root=’(hd0,msdos5)’ multiboot /boot/sel4/kernel-ia32-pc99 module /boot/sel4/sel4test-driver-image-ia32-pc99 } update grub, restart and select the new entry from GRUB menu. I end up with blinking cursor on the top-left side of the screen. Please advise.

4 3

seL4 developer hangout reminder
by Birgit Brecknell 20 Jan '25

20 Jan '25

Hi all A friendly reminder that the seL4 developer hangout is on again this week. Tue 21 Jan, 9:00pm UTC. For your local date and time please see https://sel4.systems/contact/. 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

reclaiming root server memory frames
by Yanfeng Liu 18 Jan '25

18 Jan '25

Dear experts, I am wondering how seL4 app can reclaim some root server memory frames at later stage of bootstrapping? Regards, yf

1 1

seL4 developer hangout reminder
by Birgit Brecknell 06 Jan '25

06 Jan '25

Hi all A friendly reminder that the seL4 developer hangout is on again this week. Wed 8 Jan, 7:00am UTC. For your local date and time please see https://sel4.systems/contact/. 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

CDT traveling
by Yanfeng Liu 18 Dec '24

18 Dec '24

Dear experts, I am trying to understand the memory usage of a running seL4 demo with help of GDB. I am wondering how I can travel the Capability derivation tree starting from original untyped objects and see how memory are used. I noticed that `mdb_node_t` has `mdbPrev` and `mdbNext` pointer fields but not sure how can they be used to travel the capability derivation tree? Regards, yf

2 10

On Common IPC Patterns in Microkit
by Wanja.Zaeske＠dlr.de 16 Dec '24

16 Dec '24

Hi together, during the proceedings of the last seL4 summit I participated in a discussion about Microkit usability. In particular we were talking about common patterns for IPC in Microkit, potential pitfalls and how the Microkit Tutorial introduces some of them implicitly (by requiring the user to apply them). At some point Kent suggested to put the topic on the mailing list, so here we go 😊. When initially playing through the Microkit Tutorial, I assumed that the budget/period of a protection domain were providing uninterrupted time-slots. I was thus slightly surprised, when I found out that sending a notification to a higher priority PD would immediately preempt my current PD. Now, this on its own is not problematic, Gernot simply commented my mistake with "Yes, priorities are observed". However: When playing the Microkit tutorial, I understood the way to solve Part 2 (Serial Server to Client Communication) to be as follows: * [serial server] write received char to shared buffer. * [serial server] notify client. * [client] read char from shared buffer. This is also the current approach found in the provided solution [1]. This works in some (most!) cases, but it is not reliable. It could be that chars get lost, due to the serial server overwriting the buffer before it was consumed form the client. The specific details if this works depend upon the combination of: * Data size (not-so-critical with one byte, but more data means more time is required to consume the buffer form the client) * Budget/Period of the client (can the client read all data before it is preempted by exhaustion of its budget in the current period) * Hardware Performance (same as above) * Priorities (if the serial server is higher priority and gets triggered by another hardware event before the client can consume the char, it gets lost again) This is problematic: the details of the scheduling are not very explicit in the manual (roughly one half of a page), but the first example of IPC taught via the tutorial relies on a lot of implicit circumstance on how PDs are scheduled to function correctly. Now I have three suggestions to improve upon this. 1. In the tutorial, explicitly mention the possibility of using the same notification channel in the opposite direction for a read-ACK. If another serial interrupt comes, but no ACK was received, just log an error. The point is not, to introduce ring-buffers and a the machinery for robust communication -- that would like explode the scope for a simple tutorial. Rather, the point is to teach people that this IPC mechanism may silently fail (as in chars get dropped). 2. For certain scheduling + IPC scenarios, examples with a graphical representation would be good. Here are two examples: Sending data to a higher priority PD (via notifications + shared memory) [2] and sending data to a lower priority PD (via notification + shared memory + ACK notification) [3]. Please bear with me, my talent to intuitive graphical representation is of limited nature, this for sure could be made better looking. In the end, I'd like to have an engineer short on time quickly look up the current scenario (sharing data bi-/unidir?, other PD is strictly higher prio/lower prio?, silent loss of data tolerable or not?, ...) from a table, take a look at the timing diagram and pick the correct approach for the task at hand. Microkit does not provide very sophisticated IPC APIs, and that is good! It keeps Microkit small, and the API IMHO provides everything needed, for synchronous and asynchronous communication, for large and small data, ... But composing the IPC correctly is not trivial, so anything we can to take sharp edges of the experience without bloating the API should be considered. 3. I think, there is a finite number of relevant IPC scenarios. Maybe one can build a tool to verify them (something something Promela?) and display them graphically (something something PlantUML Timing Diagrams?). This could either be used to fill a chapter in the Microkit Manual ("Common IPC Patterns, their Behavior and Pitfalls"?), or exposed as small (Web?) GUI Tool. Maybe this could become part of a student thesis even? I hope the above might spark some thought on improving accessibility of Microkit. Kind Regards, Wanja [PlantUML diagram] [PlantUML diagram] [1] https://github.com/au-ts/microkit_tutorial/blob/6733b7864217831e4e77616647e… [2] https://www.plantuml.com/plantuml/uml/VL9DYzim4BthLppIGoxP49kwWHvADlHOIYc5F… [3] https://www.plantuml.com/plantuml/uml/XLDDYzim4BthLpnosKisnA4Ecq9BjlHOIkbbp… —————————————————————————— Deutsches Zentrum für Luft- und Raumfahrt (DLR) Institut für Flugsystemtechnik | Sichere Systeme & Systems Engineering | Lilienthalplatz 7 | 38108 Braunschweig Wanja Zaeske Telefon 0531 295-1114 | Fax 0531 295-2931 | wanja.zaeske(a)dlr.de<mailto:wanja.zaeske@dlr.de> DLR.de<http://www.dlr.de/>

6 7

address of L1 CNode Cap
by Yanfeng Liu 12 Dec '24

12 Dec '24

Dear experts, When reading section 3.3.2 of the latest seL4 manual, it says: > Figure 3.3 depicts an example CSpace. In order to illustrate these ideas, we determine the address of each of the 10 capabilities in this CSpace. I guess the total number of 10 is made of 3 caps for CNode types and 7 for non- CNode ones A~G as shown in diagram. However, in the following graph, the address of the L1 CNode Cap is missed. Thus I am curious what the address for that L1 CNode Cap? Regards, yf

2 2

seL4 developer hangout reminder
by Birgit Brecknell 09 Dec '24

09 Dec '24

Hi all A friendly reminder that the seL4 developer hangout is on again this week. Wed 11 Dec, 7:00am UTC. For your local date and time please see https://sel4.systems/contact/. 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

LionsOS musllibc old version? Vulnerable?
by Hugo V.C. 30 Nov '24

30 Nov '24

Hi, reading the dependencies of LionsOS I realized it is using an old version of muslibc : https://github.com/au-ts/musllibc/blob/81842bc43d0b49bbcca03ff5f506c6df8e2b… if this version has not been patched may be vulnerable to a remotely exploitable buffer overflow in the dns resolution: https://git.musl-libc.org/cgit/musl/commit/?id=45ca5d3fcb6f874bf5ba55d0e965… Can someone confirm or reject? Thanks.

3 3

find all seL4 threads
by Yanfeng 25 Nov '24

25 Nov '24

Dear experts, I am wondering when checking a running seL4 target from GDB, how can we find all threads? It seems that `ksReadyQueues[]` only holds a sub set. Regards, yf

3 3