Formal Verification of Interrupt Isolation for the TrustZone-based TEE
Leping Zhang, Qianying Zhang, Xinyue Wang, Ximeng Li, Guohui Wang, Zhiping Shi, Yong Guan · 2023
ARM TrustZone is a hardware security technology commonly used to implement the Trusted Execution Environment (TEE), which is a hardware-based isolated execution environment in which security-critical software can execute without interference and is widely applied to embedded systems. Isolation of interrupts in the two security domains of TrustZone is an important security mechanism that plays a vital role in protecting the execution of the TEE. This paper introduces a formal modeling and verification approach for the interrupt isolation mechanism of the TEE based on TrustZone. We propose a model formalizing the TrustZone-based TEE system at the instruction level, which focuses on modeling system behaviors of interrupt handling and captures crucial instructions related to interrupt isolation. We formally define three types of properties for the model: correctness, safety, and information flow security. The verification results in the theorem prover Isabelle/HOL show that the model satisfies the above properties, which indicates that the interrupt isolation mechanism of TrustZone correctly enforces the isolation of interrupts and protects the TEE from being interfered with non-secure interrupts.