Formal Verification of Memory Isolation for the TrustZone-based TEE
Yuwei Ma, Qianying Zhang, Shijun Zhao, Guohui Wang, Ximeng Li, Zhiping Shi · 2020
The trusted execution environment (TEE) is the security basis of embedded systems, which can provide a hardware-based isolated execution environment for security-sensitive components. Isolation of memory is a critical mechanism of TEE, the security of which plays a very important role in TEE's construction. In this paper, we present a formal verification of security properties about the memory isolation mechanism of TEE systems based on the ARM TrustZone, which is a hardware security technology commonly used on billions of ARM processors to create TEE. We establish a formal model of memory isolation, which consists of the formalization of ARMv8 architecture hardware components related to memory isolation and the formalization of a TrustZone monitor supporting world switch. We formally explicit and verify the correctness properties of memory management along with the information flow security properties of the memory isolation mechanism. The formalizations and verifications are all performed in the interactive theorem prover Isabelle/HOL.