- Devel - lists.sel4.systems

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

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

14 May '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 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