Secure mode seL4 builds for ARM

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.