Hi all
A friendly reminder that the seL4 developer hangout is on again this week.
Wed 25 June, 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>
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.
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.
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
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>
