RTEMS as a Guest/Manager on seL4 Microkernel

[Hesham Almatary]

Goals
Host RTEMS on seL4 in a way that leverages the strengths of both operating systems to bring a highly capable, robust, and secure environment to users.
RTEMS on seL4 can be used to host user applications or as the foundation of services which are available to all clients.

High Level Design
There are multiple patterns for hosting RTEMS on seL4. Each of these brings with it specific characteristics that need to be evaluated in terms of the Goal.
The first pattern is to host RTEMS as a guest executing in a privileged container. This likely requires few changes to RTEMS since the provided seL4 container is essentially identical to executing on the same board natively. This can bring the full capabilities of RTEMS to seL4 but it does not make use of the security guarantees provided by seL4. RTEMS would require direct access to every memory location, register, device and interrupt source it uses.
The second approach is to execute RTEMS in the least privileged paravirtualized seL4 container. This requires paravirtualizing RTEMS and using the virtual device drivers provided by seL4. This will require developing a BSP that is targeting the seL4 container, not a particular board. This design approach takes advantage of the protections offered by seL4.

Level: Advanced
Prerequisites: Strong C, Operating Systems and Microkernels hands-on experience preferably with both seL4 and RTEMS. Knowledge with hypervisor is also required.

References:
[1] ​https://heshamelmatary.blogspot.com/2015/12/rtems-port-for-risc-v-withwithout-sel4.html
[2] ​https://github.com/heshamelmatary/rtems-riscv
[3] ​https://sel4.systems/