Hi Isaac

I am not familiar with ppc64le/IBM Power and don't regular do work inside the kernel itself so keep that in mind with my answer, but here is how I would go about porting a new architecture.

Booting is probably one of the hardest and most architecture dependent parts of seL4. You will notice that for ARM and RISC-V, seL4 requires some bootloader before it starts to do things like initialise hardware and enable virtual memory before jumping to the kernel code. Taking something like U-Boot and booting seL4 directly is not something possible on those architectures as far as I know.

Whether this matters for IBM Power, I am not sure. For example unlike ARM and RISC-V, x86 does not require any special bootloader to boot an seL4 image.

For the kernel, you would probably want to get the simplest configuration going first for testing, so that would probably be single-core, no MCS, no hypervisor or anything.

Once you think you've got booting setup the first thing I would do is get some kind of serial output in the kernel as soon as it starts. For this, it might not be as simple as just writing a serial driver and using it as soon as you get into the kernel entry point as, depending on the architecture, there will probably be some more hardware initialisation do to first. For example, on AArch64 the `activate_kernel_vspace` function needs to be called first before any of the serial output will work in the kernel (more info in [1]).

Once you get enough boot code to print out in the kernel, you can start following all the other architecture boot code (in src/arch/<ARCH>/kernel/boot.c) to setup the initial task (aka first user process). So I guess the next step will be getting the initial task working. This will require virtual memory working (which is highly architecture specific) as well as figuring out all the architecture specific parts of kernel objects. From there, I guess you could check if the initial task is working with `seL4_DebugPutChar`, getting to this point will probably be the bulk of the work as it means that the system call code needs to work.

After that, getting sel4test working would be a good goal.

Last year, there was a PR [2] to add the LoongArch architecture to seL4. To my knowledge, LoongArch is fairly similar to RISC-V so not sure how much help it will be but the important thing is that this architecture port is quite recent and so what kernel code they had to change is a good guide as it will not be too out of date compared to the last most recent architecture port (which was RISC-V I believe and was done 5-10 years ago).

[1]: https://github.com/seL4/seL4/issues/540.

[2]: https://github.com/seL4/seL4/pull/970

I hope this helps get you started. Others more familiar with the kernel, feel free to correct me on anything.

Ivan

On 5/3/24 01:07, Isaac Beckett wrote:

[isaactbeckett@gmail.com appears similar to someone who previously sent you email, but may not be that person. Learn why this could be a risk at https://aka.ms/LearnAboutSenderIdentification ]

Hello!

I’m writing to ask how someone would approach porting seL4 to a new CPU architecture. For example, ppc64le/IBM Power, since those systems can be run with limited or no black box firmware blobs, they could offer stronger security under seL4 since you can audit or replace the platform firmware in many cases. There’s even an OEM manufacturing Power9 systems with this in mind.

That said, I know supporting a new architecture is not trivial. New platform code would have to be written and verified, and existing userspace code for Arm and x86-64 may have to be adjusted.

How does one approach something like this? Is it feasible for someone less familiar with seL4’s internals to get something quick and dirty running as a proof of concept? _______________________________________________ Devel mailing list -- devel@sel4.systems To unsubscribe send an email to devel-leave@sel4.systems