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