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 条
  • [31] Formal Specification and Verification of JXTA's Endpoint Routing Protocol
    Konga, Yannick L. Kala
    Djouani, Karim
    [J]. IEEE AFRICON 2011, 2011,
  • [32] Integrating semi-formal and formal software specification techniques
    Wieringa, R
    Dubois, E
    [J]. INFORMATION SYSTEMS, 1998, 23 (3-4) : 159 - 178
  • [33] Formal Specification and Verification of Self-Adaptive Concurrent Systems
    Fakhir, Muhammad Ilyas
    Kazmi, Syed Asad Raza
    [J]. IEEE ACCESS, 2018, 6 : 34790 - 34803
  • [34] Formal specification for secure electronic data interchange system in Maude
    Wu, JunFeng
    Miao, HuaiKou
    [J]. 2007 IEEE INTERNATIONAL CONFERENCE ON AUTOMATION AND LOGISTICS, VOLS 1-6, 2007, : 526 - +
  • [35] Formal specification of holonic multi-agent systems framework
    Rodriguez, S
    Hilaire, V
    Koukam, A
    [J]. COMPUTATIONAL SCIENCE - ICCS 2005, PT 3, 2005, 3516 : 719 - 726
  • [36] Formal Verification of GP Specification based Embedded Operating System
    Sun, Haiyong
    Lei, Hang
    Qiao, Lei
    Yang, Zheng
    [J]. PROCEEDINGS OF THE 2ND INTERNATIONAL CONFERENCE ON COMPUTER SCIENCE AND APPLICATION ENGINEERING (CSAE2018), 2018,
  • [37] Formal Specification and Model Checking of an Autonomous Vehicle Merging Protocol
    Liu, Minxuan
    Dang Duy Bui
    Duong Dinh Tran
    Ogata, Kazuhiro
    [J]. 2021 21ST INTERNATIONAL CONFERENCE ON SOFTWARE QUALITY, RELIABILITY AND SECURITY COMPANION (QRS-C 2021), 2021, : 333 - 342
  • [38] Making the most of formal specification through animation, testing and proof
    Bicarregui, J
    Dick, J
    Matthews, B
    Woods, E
    [J]. SCIENCE OF COMPUTER PROGRAMMING, 1997, 29 (1-2) : 53 - 78
  • [39] E-store: formal specification
    Uros, T
    Uros, I
    [J]. EEE '05: PROCEEDINGS OF THE 2005 INTERNATIONAL CONFERENCE ON E-BUSINESS, ENTERPRISE INFORMATION SYSTEMS, E-GOVERNMENT, AND OUTSOURCING, 2005, : 201 - 207
  • [40] FORMAL SPECIFICATION AND DESIGN TIME TESTING
    GERRARD, CP
    COLEMAN, D
    GALLIMORE, RM
    [J]. IEEE TRANSACTIONS ON SOFTWARE ENGINEERING, 1990, 16 (01) : 1 - 12
12345