- Devel - lists.sel4.systems

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