Freesia: Verifying Correctness of TEE Communication with Concurrent Separation Logic

The Trusted Execution Environment (TEE), a security extension in modern processors, provides a secure runtime environment for sensitive code and data. Although TEEs are designed to protect applications and their private data, their large code bases often harbor vulnerabilities that could compromise data security. Even though some formal verification efforts have been directed toward the functionality and security of TEE standards and implementations, the verification of TEE correctness in concurrent scenarios remains insufficient. This paper introduces an enhancement for ensuring concurrency safety in TEEs, named Freesia, which is formally verified using concurrent separation logic. Through a thorough analysis of the GlobalPlatform TEE standards, Freesia addresses data race issues in the TEE communication interfaces and ensures consistency protection for shared memory between the client and the TEE. A prototype of Freesia is implemented in the open-source TEE platform, OP-TEE. Additionally, the concurrency correctness of Freesia is modeled and verified using the Iris concurrent separation logic framework. The effectiveness and efficiency of Freesia are further demonstrated through real-world case study and performance evaluations.