基于精化的可信执行环境内存隔离机制验证

Refinement-based Verification of Memory Isolation Mechanism for Trusted Execution Environment

可信执行环境(trusted execution environment,TEE)基于硬件隔离机制,为安全敏感应用提供隔离的执行环境,保护敏感数据的安全性.内存隔离机制是TEE的关键机制之一,用于对安全内存和非安全内存进行隔离,并对安全内存实施访问控制,如果其安全性不能保证,可能造成存储在安全内存中的敏感数据泄露.为验证TEE内存隔离机制的安全性,针对基于ARM TrustZone技术构建的TEE,提出一种基于精化的可信执行环境内存隔离机制安全性验证方法.建立抽象模型和具体模型,并定义两种模型之间的精化关系,在证明精化关系成立和抽象模型满足信息流安全性的前提下,验证具体模型的信息流安全性.具体模型建模了TEE内存隔离机制的关键硬件和软件,包括TrustZone地址空间控制器、MMU和TrustZone monitor等,在定理证明器Isabelle/HOL中,验证了该模型满足无干扰、无泄露、无影响等信息流安全属性.

A trusted execution environment(TEE) provides security-sensitive applications with an isolated execution environment based on hardware isolation mechanisms to protect sensitive data. The memory isolation mechanism is one of the key mechanisms of TEE,which is used to isolate the secure memory from the non-secure memory and to control the access to the secure memory. If the security of the memory isolation mechanism can not be guaranteed, sensitive data stored in the secure memory may be leaked. To verify the security of the TEE memory isolation mechanism, a refinement-based security verification method of the memory isolation mechanism is propose for ARM TrustZone-based TEE. An abstract model and a concrete model are established, a refinement relation between these two models is defined, and the information flow security of the concrete model is verified on the premise of proving that the refinement relation is held and the abstract model satisfies the information flow security properties. The proposed concrete model consists of key hardware and software of the TEE memory isolation mechanism, including TrustZone address space controller, MMU, and TrustZone monitor, and using the theorem prover Isabelle/HOL, it is verified that the concrete model satisfies the information flow security properties, such as noninterference, nonleakage, and noninfluence.