March 2025 - 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

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

06 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

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

18 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

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

10 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

Question about extensibility
by 1plus.yijia＠gmail.com 31 Mar '25

31 Mar '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 30 Mar '25

30 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 27 Mar '25

27 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 21 Mar '25

21 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 16 Mar '25

16 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 13 Mar '25

13 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