To answer this question we need to look at what a platform port consists of and what guarantees are required for the platform.
Port the kernel
To port the seL4 kernel itself, such that seL4 can boot and launch a root task, requires the following:
- on ARM platforms (Both Aarch64 and Aarch32), the elfloader tool must be modified to load the kernel at the correct address.
- Add devices required by the kernel. seL4 only uses the timer and interrupt controller, as well as a UART in debug mode.
- TODO once the dtb stuff is merged, write how to add devices.
- Add the new platform to the build system.
Port seL4 test
- sel4test is the seL4 test suite, which although not comprehensive is designed to test a platform port is functioning. sel4test requires a working, user-level timer and a user-level serial driver.
Consider advanced features
- Do you want SMP? Then the elfloader requires further modification to launch separate cores.
- Do you want to run seL4 as a hypervisor on this platform? Once again, the elfloader needs to be modified and the correct time sources need to be used.
What about the proofs?
The majority of supported hardware is supported as a prototype: seL4 can run on that platform, but the proofs do not apply to that platform, which means no proof guarantees hold for that platform.