- Devel - lists.sel4.systems

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

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