Formal verification study demonstrates vulnerability detection in IoT trusted execution environments, highlighting the effectiveness of executable API models for secure application design.
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.
No takes yet. Share an insight, caveat, or question.
Yu et al. (2026) studied this question.
Synapse has enriched 5 closely related papers on similar clinical questions. Consider them for comparative context: