Tacco: A Framework for Ensuring the Security of Real-World TEEs via Formal Verification

Abstract

Trusted Execution Environment (TEE) provides isolation for sensitive data in electronic devices and its compromise can lead to enormous losses. TEE’s information-flow security is essential and can be robustly ensured by formal methods. Nevertheless, the cross-domain API invocation of TEE is intricate for information-flow analysis, and the service provider on the TEE, i.e., trusted application, brings complexity to the TEE specification and verification. Existing research seldom delves into general TEEs that are compliant with GlobalPlatform (GP), which is an important and universal TEE standard. Furthermore, they are not in alignment with the requirement of Common Criteria certification. In this paper, we propose a TEE-applicable and common criteria-oriented framework to specify and verify the information-flow security of GP TEE, which is applied to the verification of the real-world commercial MiTEE. Firstly, we present a framework for TEE that aligns with the requirements of Common Criteria’s highest assurance level (EAL 7). It incorporates a domain-switch based mechanism to model the cross-domain TEE API invocation and a parameterized modeling approach to handle trusted applications. Secondly, we model GlobalPlatform-compliant TEE with the framework as GP TEE security model layer and function layer, which are reusable for all GP TEEs. Thirdly, we specify MiTEE as the MiTEE design layer that refines GP TEE model. Lastly, we verify the information-flow security of GP TEE and MiTEE via theorem proving and uncover four critical vulnerabilities in MiTEE. This work contributes to MiTEE’s acquirement of an EAL 5+ certificate. All works are carried out in Isabelle/HOL, with nearly 32000 lines of code.

Framework Overview

Theories

Download the Isabelle source code

Theory	Contents
GP TEE SecurityModel Layer	This is the security model of GlobalPlatform-compliant TEE (GP TEE), including several security objectives while this paper focus on the isolation. Information-flow properties are defined here, i.e., noninfluence. State machines for GP TEE and unwinding conditions are also defined.
GP TEE Function Layer	This layer includes the definitions of basic data structures and execution model, event specification, the instantiation proof, and security proofs of events. It is the implementation of the GP TEE function layer of our framework Tacco.
MiTEE Design Layer	This layer includes the model of MiTEE design layer, refinement proof between GP TEE function layer and MiTEE design layer, the security proof on new variables in MiTEE design layer, and the final security proof of MiTEE.