Secure mode seL4 builds for ARM

seL4 kernel
#1

Hey,

At various junctures and at sundry times we encounter the question of whether or not we should have explicit builds of the seL4 kernel for ARM’s secure mode.

Usually when we encounter differences between a build of the kernel for secure vs non-secure world, we either ignore secure world, or we introduce code which attempts to navigate the middle road between them, whereas we technically should be doing separate builds of the kernel for secure mode (aka EL3) – similar to how we currently have separate binary image builds of the kernel for Hyp mode (aka EL2) vs Supervisor mode (aka EL1).

I don’t know whether or not we intend to ever have seL4 executing in secure world and acting as something like a trusted firmware executive that then controls the execution of some other software that is executing in non-secure world.

But the work of retrofitting the kernel for secure world might be easier if we make an explicit decision about whether or not we ever intend to support secure world seL4. I’m asking right now because similar to when we did the debug coprocessor work, and when we did the GIC work and we encountered secure mode implications, we’re about to encounter them again with the SMMU work.

–Thanks for your time

#2

Hi Kofi,

Please note that “secure” vs “normal” aka “non-secure” mode is orthogonal-ish to privilege levels:

  • EL1 (aka supervisor mode) exists in both modes
  • EL2 (aka hypervisor mode) presently exists in non-secure modes but soon also in secure mode
  • EL3 (aka monitor mode) only exists in secure mode

EL3 is meant for securely switching between modes (besides initialising the processor)

Our standard setup is presently non-secure EL1 (for compatibility with pre-V8 cores that don’t have EL2) or EL2. The kernel should probably “just work” in secure EL1 (and, once that’s here, secure EL2).

All that TrustZone stuff is sort-of irrelevant if you have real security with seL4, which means having a monitor (EL3) that just boots and than hands everything to seL4 in “non-secure” EL1 or EL2 and never using “secure” mode is a reasonable way to run the processor. Or have seL4 in secure mode in EL1 and never use “non-secure” mode, except that you then lose virtualisation support (but that drawback goes away when EL2 is supported in secure mode).

Having seL4 run in EL3 and everything else in EL0/EL1 should be possible, but you lose virtualisation (unless you run another hypervisor in EL2).

In practice, EL3 is often inaccessible (basically firmware), so that option often does not exist. Even where it does, it is probably simplest to just use EL3 for initialising and then handing over to seL4.

#3

Kofi,
having seL4 running as secure EL1 payload of the ATF would be interesting, especially some blueprints for the kernel modifications to support the SMC interface to ATF and the GICv2/v3/v4 interrupt models.