Formal Specification of Trusted Execution Environment APIs

被引：1
|
作者：
Yu, Geunyeol [1 ]
Chae, Seunghyun [1 ]
Bae, Kyungmin [1 ]
Moon, Sungkun [2 ]
机构：
[1] Pohang Univ Sci & Technol, Pohang, South Korea
[2] Samsung Elect, Hwasung, South Korea
来源：
FUNDAMENTAL APPROACHES TO SOFTWARE ENGINEERING, FASE 2024 | 2024年 / 14573卷
基金：
新加坡国家研究基金会;
关键词：
Trusted execution environments; formal specification; formal methods; model checking; rewriting logic; Maude;
D O I：
10.1007/978-3-031-57259-3_5
中图分类号：
TP31 [计算机软件];
学科分类号：
081202 ; 0835 ;
摘要：
Trusted execution environments (TEEs) have emerged as a key technology in the cybersecurity domain. A TEE provides an isolated environment in which sensitive computations can be executed securely. Trusted applications running in TEEs are developed using standardized APIs that many hardware platforms for TEE adhere to. However, formal models tailored to standard TEE APIs are not well developed. In this paper, we present a formal specification of TEE APIs using Maude. We focus on Trusted Storage API and Cryptographic Operations API, which are foundational to mobile and IoT applications. The effectiveness of our approach is demonstrated through formal analysis of MQT-TZ, an open-source TEE application for IoT. Our formal analysis has revealed security vulnerabilities in the implementation of MQT-TZ, and we patch and confirm its integrity using model checking.
引用
收藏
页码：101 / 121
页数：21
相关论文
共 50 条
  • [41] Open-TEE - An Open Virtual Trusted Execution Environment
    McGillion, Brian
    Dettenborn, Tanel
    Nyman, Thomas
    Asokan, N.
    2015 IEEE TRUSTCOM/BIGDATASE/ISPA, VOL 1, 2015, : 400 - 407
  • [42] Index Obfuscation for Oblivious Document Retrieval in a Trusted Execution Environment
    Shao, Jinjin
    Ji, Shiyu
    Glova, Alvin Oliver
    Qiao, Yifan
    Yang, Tao
    Sherwood, Tim
    CIKM '20: PROCEEDINGS OF THE 29TH ACM INTERNATIONAL CONFERENCE ON INFORMATION & KNOWLEDGE MANAGEMENT, 2020, : 1345 - 1354
  • [43] Trusted Execution Environment-Based Authentication Gauge (TEEBAG)
    Balisane, Ranjbar A.
    Martin, Andrew
    PROCEEDINGS OF THE 2016 NEW SECURITY PARADIGMS WORKSHOP (NSPW'16), 2016, : 61 - 67
  • [44] Task Offloading in Trusted Execution Environment empowered Edge Computing
    Li, Yuepeng
    Zeng, Deze
    Gu, Lin
    Zhu, Andong
    Chen, Quan
    2020 IEEE 26TH INTERNATIONAL CONFERENCE ON PARALLEL AND DISTRIBUTED SYSTEMS (ICPADS), 2020, : 316 - 323
  • [45] Ecosystems of Trusted Execution Environment on Smartphones - A Potentially Bumpy Road
    Umar, Assad
    Akram, Raja Naeem
    Mayes, Keith
    Markantonakis, Konstantinos
    PROCEEDINGS OF THE 2017 THIRD INTERNATIONAL CONFERENCE ON MOBILE AND SECURE SERVICES (MOBISECSERV), 2017,
  • [46] Trusted Execution Environment: State-of-the-Art and Future Directions
    Zhang F.
    Zhou L.
    Zhang Y.
    Ren M.
    Deng Y.
    Jisuanji Yanjiu yu Fazhan/Computer Research and Development, 2024, 61 (01): : 243 - 260
  • [47] Data Enclave: A Data-Centric Trusted Execution Environment
    Xu, Yuanchao
    Pangia, James
    Ye, Chencheng
    Solihin, Yan
    Shen, Xipeng
    2024 IEEE INTERNATIONAL SYMPOSIUM ON HIGH-PERFORMANCE COMPUTER ARCHITECTURE, HPCA 2024, 2024, : 218 - 232
  • [48] Privacy-preserving genotype imputation in a trusted execution environment
    Dokmai, Natnatee
    Kockan, Can
    Zhu, Kaiyuan
    Wang, XiaoFeng
    Sahinalp, S. Cenk
    Cho, Hyunghoon
    CELL SYSTEMS, 2021, 12 (10) : 983 - +
  • [49] Formal specification and implementation of an environment for automatic distribution
    Parsa, Saeed
    Bushehrian, Omid
    ADVANCES IN GRID AND PERVASIVE COMPUTING, PROCEEDINGS, 2007, 4459 : 543 - 554
  • [50] SDD: A trusted display of FIDO2 transaction confirmation without trusted execution environment
    Xu, Peng
    Sun, Ruijie
    Wang, Wei
    Chen, Tianyang
    Zheng, Yubo
    Jin, Hai
    FUTURE GENERATION COMPUTER SYSTEMS-THE INTERNATIONAL JOURNAL OF ESCIENCE, 2021, 125 : 32 - 40
12345