Formalizing and Verifying GP TEE TA Interface Specification Using Coq

The ARM TrustZone platform has provided a trusted execution environment (TEE) for mobile device to improve system security. The Global Platform presents a TEE Internal Core API Specification to define the TEE, the TEE system architecture, and the Internal and Client API specifications. However, hackers can still attack the TEE by means of the tampering the message stored in the communication buffer that is used to exchange information between the TEE and REE world. In order to solve this problem, this paper presents a formal security model of the Open image in new window Interface and verifies the correctness of this model using Coq based on the GP specification. The formalization identifies the TA Interface specification as well as modelling the valid trace of TA Interface based on a one-session application, which can effectively detect and filter the invalid TA service request that from REE. These results are useful for the standard institutions and TEE developers to develop security TA software and prevent from hackers attack.