4 ms·

Are there any resources for running SeL4 on a raspberry pi or other arm SBC'S? The article mentions hypervisor support, which makes me think it'd be a possible

Are there any resources for running SeL4 on a raspberry pi or other arm SBC'S? The article mentions hypervisor support, which makes me think it'd be a possible way to run Linux on top of a secure RTOS. Working in the embedded world and I ponder what could be possible with a high security hypervisor.

im_down_w_otp 7y ago
seL4 isn't an RTOS, FWIW. There is hypervisor support, sort of. Insofar as there's enough there to build your own hypervisor (we ended up needing to do something like this), and there's a sample VMM for a very specific host and guest target combination available that's created via CAmkES. Making an seL4-based hypervisor truly cross-architecture capable as well as generalizable for different host and guest target configurations is a non-trivial, painstaking, arduous task. In fact making anything on seL4 truly cross-platform isn't easy. The kernel doesn't provide much in the way of unifying abstractions over the architecture differences. The different architecture details are mostly thrust onto you to figure out what kind of abstractions you want to make. The MCS (mixed criticality support) stuff in seL4 getting mainlined should make it theoretically possible to invent/create a hypervisor that enables you to run MCU oriented RTOSes & applications in an isolated context atop non-HRT hardware. Data61 has mentioned that they're going to take a whack at making some part of an AUTOSAR stack that runs in a context like this, but I have no idea how far along that is. Separately, we're looking at leveraging the same underlying capability for a variety of different adjacent purposes. That said, there are a variety of supported platforms you can already build seL4 for: https://docs.sel4.systems/Hardware/ https://docs.sel4.systems/Hardware/, our experience has been that some work better than others. It's possible to run in QEMU as well to get started.
- snvzz 7y ago
  How is seL4 not a hard RTOS? It even has proof of worst case time (WCET), which to my knowledge no other non-trivial RTOS does have. I'm very confused now.
  - msjyoo 7y ago
    seL4 at the moment doesn't have kernel interrupts. The kernel relies on run-to-completion and "incremental consistency" partly because IPC in seL4 is already short so the time window for a kernel interrupt to be needed is also correspondingly small, and because it makes proofs easier. Of course, this means there's possibilities of long tail latency for interrupts to be delivered to userspace if the kernel needs to run a long operation.
    - repolfx 7y ago
      My understanding of seL4 is that the kernel never really needs to run a long operation because it does so very little. For instance filesystems would be a usermode process, along with nearly all drivers. Isn't that why the MCS stuff works - the kernel may not be able to interrupt itself but that doesn't matter because it can interrupt userspace, which is where 99% of traditional kernel code ends up?
      - msjyoo 7y ago
        That's not quite true. It's not solely because seL4 does little. seL4 maintains low interrupt latency through "preemption points" - basically points where the kernel can and can only context-switch while maintaining global consistency. Keeping in mind I'm not an expert on this, I dug up these papers when I was vaguely looking, they may be useful to you: "Improving Interrupt Response Time in a Verifiable Protected Microkernel" https://ts.data61.csiro.au/publications/nicta_full_text/5391.pdf https://ts.data61.csiro.au/publications/nicta_full_text/5391... "To Preempt or Not To Preempt, That Is the Question" http://ts.csiro.au/publications/nicta_full_text/5859.pdf http://ts.csiro.au/publications/nicta_full_text/5859.pdf
        repolfx 7y ago
        Thanks, that's super helpful.
        snvzz 7y ago

im_down_w_otp 7y ago

seL4 isn't an RTOS, FWIW. There is hypervisor support, sort of. Insofar as there's enough there to build your own hypervisor (we ended up needing to do something like this), and there's a sample VMM for a very specific host and guest target combination available that's created via CAmkES. Making an seL4-based hypervisor truly cross-architecture capable as well as generalizable for different host and guest target configurations is a non-trivial, painstaking, arduous task. In fact making anything on seL4 truly cross-platform isn't easy. The kernel doesn't provide much in the way of unifying abstractions over the architecture differences. The different architecture details are mostly thrust onto you to figure out what kind of abstractions you want to make. The MCS (mixed criticality support) stuff in seL4 getting mainlined should make it theoretically possible to invent/create a hypervisor that enables you to run MCU oriented RTOSes & applications in an isolated context atop non-HRT hardware. Data61 has mentioned that they're going to take a whack at making some part of an AUTOSAR stack that runs in a context like this, but I have no idea how far along that is. Separately, we're looking at leveraging the same underlying capability for a variety of different adjacent purposes. That said, there are a variety of supported platforms you can already build seL4 for: https://docs.sel4.systems/Hardware/ https://docs.sel4.systems/Hardware/, our experience has been that some work better than others. It's possible to run in QEMU as well to get started.

snvzz 7y ago
How is seL4 not a hard RTOS? It even has proof of worst case time (WCET), which to my knowledge no other non-trivial RTOS does have. I'm very confused now.
- msjyoo 7y ago
  seL4 at the moment doesn't have kernel interrupts. The kernel relies on run-to-completion and "incremental consistency" partly because IPC in seL4 is already short so the time window for a kernel interrupt to be needed is also correspondingly small, and because it makes proofs easier. Of course, this means there's possibilities of long tail latency for interrupts to be delivered to userspace if the kernel needs to run a long operation.
  - repolfx 7y ago
    My understanding of seL4 is that the kernel never really needs to run a long operation because it does so very little. For instance filesystems would be a usermode process, along with nearly all drivers. Isn't that why the MCS stuff works - the kernel may not be able to interrupt itself but that doesn't matter because it can interrupt userspace, which is where 99% of traditional kernel code ends up?
    - msjyoo 7y ago
      That's not quite true. It's not solely because seL4 does little. seL4 maintains low interrupt latency through "preemption points" - basically points where the kernel can and can only context-switch while maintaining global consistency. Keeping in mind I'm not an expert on this, I dug up these papers when I was vaguely looking, they may be useful to you: "Improving Interrupt Response Time in a Verifiable Protected Microkernel" https://ts.data61.csiro.au/publications/nicta_full_text/5391.pdf https://ts.data61.csiro.au/publications/nicta_full_text/5391... "To Preempt or Not To Preempt, That Is the Question" http://ts.csiro.au/publications/nicta_full_text/5859.pdf http://ts.csiro.au/publications/nicta_full_text/5859.pdf
      - repolfx 7y ago
        Thanks, that's super helpful.
        snvzz 7y ago