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.