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.

Hello Peter, On 2025-06-03 18:49, Peter Relich via Devel wrote:
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.
Wouldn't you want such watchdog kind of functionality (also) on the robotic vehicle itself? E.g. in case a cable or antenna breaks. If you have that, it is questionable whether running just Linux in a VM on top of seL4 adds anything. It will complicate things and increase the chance of software misbehaving on the Linux side, as running it as a VM is not fully transparent.
I saw that their approach for pre-generating an ELF file for the bootloader was the main obstacle for their pull request
They were trying to shoe-horn the Arm/RISC-V way of doing things onto x86, where it doesn't make sense. Instead, they should move what the loader does to the startup/monitor task, like Ivan said in one of the comments: "One potential solution to look into is appending the PD data to the monitor and having its initialisation process slightly differ so that it reads from that memory instead of device memory. This would mean we do not have to make patches to the kernel as well." So my advise would be to work on that instead of adapting the existing x86 patches for seL4 itself. You should be able to re-use some of their Microkit commits though. But then again, if you want something ready to use and don't have much requirements about the seL4 part of things, why not use camkes? I would also port the Linux code to seL4 instead of VMing it all, as that setup doesn't make much sense to me. All in all, if you have control over the robot software, running seL4 there seems to make more sense than running it on the Linux based control side. Greetings, Indan

Thanks for the comments, but there's a lot of trade offs I have to make and your options won't work for me. I didn't list all the requirements I have to follow, but I'll list a few comments below just so you understand what I'm trying to do here. If what I'm doing is a fool's errand, please do tell me π. I'm also still trying to get caught up with everything seL4, so if I make any obvious faux pas here, please don't hesitate to point it out. 1) The program assumption is that I'd make minimal changes to the robot software, I have to structure the containerization and partitioning around it. That may not be 100% possible, but I'm trying to get to a solution that can use different robotics software since the U.S. changed its priorities a few months ago. They want a bigger commercial influence in the autonomy space and they don't want the curse of vendor lock, so we have to write systems that are more interoperable. Definitely not the easiest way to go about things, but its now a hard requirement. Hence why I want to containerize multiple VM's. Initial deployment is with Ubuntu, then ROS, then multiple PDs with different ROS nodes to demonstrate high assurance RAM separability between essential (i.e., remote control and safety) and standard (sensors, autonomy) operations. 2) CAmkES is a definite no go for me. It loses its high assurance verification if you accidently misconfigure your system and you have to reconfigure our system every time you change some aspect of your application. Itβs a giant headache for what I'm doing. If I develop a CAmkES app, my customer will probably fire me. I think they already have a lot of CAmkES solutions, they want something new. I definitely appreciate your insight on the Rust Rebased version. After hearing that the x86 project is still developing, I'm thinking for now it might make more sense if I start getting a ROS2 environment on QEMU with an ARM architecture up and running and one the x86 version is ready, I can do the migration. At least I'll have some competency/experience with seL4/microkit by then so the migration shouldn't be too bad. I can then at least from the ARM side, test or set up the environment to do verification of the architecture. This is a 20 month project for me, so I just have to make sure I'm making incremental progress and building out a modular (as possible) architecture that will benefit robots π Thanks again for your comments. Best, Peter -----Original Message----- From: Indan Zupancic <indan@nul.nu> Sent: Tuesday, June 10, 2025 4:55 AM To: Peter Relich <prelich@intellisenseinc.com> Cc: devel@sel4.systems Subject: Re: [seL4] Re: I am interested in porting LionOS to X64 architecture CAUTION: This email originated from outside of Intellisense. Do NOT click links or open attachments unless you recognize the sender and know the content is safe. Hello Peter, On 2025-06-03 18:49, Peter Relich via Devel wrote:
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.
Wouldn't you want such watchdog kind of functionality (also) on the robotic vehicle itself? E.g. in case a cable or antenna breaks. If you have that, it is questionable whether running just Linux in a VM on top of seL4 adds anything. It will complicate things and increase the chance of software misbehaving on the Linux side, as running it as a VM is not fully transparent.
I saw that their approach for pre-generating an ELF file for the bootloader was the main obstacle for their pull request
They were trying to shoe-horn the Arm/RISC-V way of doing things onto x86, where it doesn't make sense. Instead, they should move what the loader does to the startup/monitor task, like Ivan said in one of the comments: "One potential solution to look into is appending the PD data to the monitor and having its initialisation process slightly differ so that it reads from that memory instead of device memory. This would mean we do not have to make patches to the kernel as well." So my advise would be to work on that instead of adapting the existing x86 patches for seL4 itself. You should be able to re-use some of their Microkit commits though. But then again, if you want something ready to use and don't have much requirements about the seL4 part of things, why not use camkes? I would also port the Linux code to seL4 instead of VMing it all, as that setup doesn't make much sense to me. All in all, if you have control over the robot software, running seL4 there seems to make more sense than running it on the Linux based control side. Greetings, Indan ________________________________ 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.
participants (2)
-
Indan Zupancic
-
Peter Relich