The purpose of this thread is to discuss what TrustZone support for the AArch64 seL4 kernel might look like, and whether that’s worth the cost.
TrustZone background
The security of a TrustZone-enabled system is achieved by partitioning all of the SoC’s hardware and software resources so that they exist in one of two worlds - the secure world for the security subsystem, and the normal world for everything else. From the point of view of an ARMv8-A processor, the system has two physical address spaces: one for secure transactions and another for non-secure transactions. Page table entries contain a field called the NS (non-secure) bit, which determines whether a page is mapped from the secure or non-secure physical address space. Furthermore, the processor state contains a global NS bit, which can only be modified by software executing at the highest exception level, EL3. When the NS processor state bit is set, the processor is said to be executing in the non-secure state, and can’t issue secure bus transactions, regardless of the values of the NS bits in its translation tables.
A typical TrustZone software stack hosts a TEE (Trusted Execution Environment) on secure-world resources, and a REE (Rich Execution Environment) on normal-world resources. A so-called “secure monitor” runs in EL3, and uses the NS processor state bit to implement a coarse context switch called a “world switch”. The simplicity of this coarse context switch minimizes the attack surface of the secure monitor.
seL4 + TrustZone
seL4 would be useful as a secure-world operating system (known as a Trusted Operating System or TOS) running in secure-EL1 (S-EL1), as a secure-world hypervisor (known as a Secure Partition Manager or SPM) running in S-EL2, or as a secure-world guest operating system running in S-EL1 on top of an SPM.
In any case, the AArch64 kernel would have to be extended with the distinction between the secure and non-secure physical address spaces so that it could construct translation structures with mappings from both address spaces, and so that it could enforce a policy which restricts kernel resources to secure memory.
Goals of this thread
- Survey the applications of TrustZone support for seL4 on AArch64, in order to determine the value of this proposed extension.
- Identify stakeholders.
- Explore the range of possible implementations of this proposed extension.
- Understand the costs to existing configurations of the kernel.