Formal Specification of Trusted Execution Environment APIs and Model Checking of Trusted Applications
TL;DR
A formal specification for TEE APIs using Maude focuses on the Trusted Storage API and the Cryptographic Operations API, both foundational to mobile and IoT applications and applies a state-space reduction technique based on invisible transitions to mitigate the state explosion problem.
Abstract
Trusted execution environments (TEEs) have emerged as a key technology in cybersecurity, providing isolated environments where sensitive computations can be executed securely. Trusted applications running in a TEE are developed using standardized APIs to which many TEE hardware platforms conform. However, formal executable models tailored to these standard TEE APIs have not been well developed. In this paper, we present a formal specification for TEE APIs using Maude. We focus on the Trusted Storage API and the Cryptographic Operations API, both foundational to mobile and IoT applications. To support the formal analysis of trusted applications, we also model the broader TEE infrastructure. In addition, we apply a state-space reduction technique based on invisible transitions to mitigate the state explosion problem. We demonstrate the effectiveness of our approach through the formal analysis of MQT-TZ, an open-source TEE application for IoT. Our formal analysis reveals a security vulnerability in the implementation of MQT-TZ. We patch the implementation and verify its correctness using model checking.