- Devel - lists.sel4.systems

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

30 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 26 Oct '25

26 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 23 Oct '25

23 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 12 Oct '25

12 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