How can I port seL4 to a new ARM hardware platform?

seL4 kernel
1

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.

2

If the proofs do not hold for a particular platform, is there any benefit to using seL4 on that platform?

3

It depends on how far away the platform is from a verified setup.

For instance, a port to a different board in the verified platform configured with the verified feature set may only change a few hardware setup details such as kernel base address or hardware initialisation during boot. One can reasonably easily validate manually wether the proof assumptions still hold for this port without actually doing anything to the proofs.

If it’s a very different feature set, e.g. includes SMP, then the value diminishes, but you still have a lot of code that has gone through verification and will at least not misbehave on its own as long as it is not called from new platform code in states or with arguments that don’t satisfy its preconditions. And of course any new code could have defects as well. So there is still value, but not as much, and of course there is no full proof any more (until someone adds that proof).

1 Like