- Titel
- Formal Specification and Verification of Architecturally-Defined Attestation Mechanisms in Arm CCA and Intel TDX
- Zitierfähige Url:
- https://nbn-resolving.org/urn:nbn:de:bsz:14-qucosa2-967631
- Quellenangabe
- IEEE access
Erscheinungsjahr: 2023
Jahrgang: 11
Seiten: 361-381
E-ISSN: 2169-3536 - Erstveröffentlichung
- 2023
- Abstract (EN)
- Attestation is one of the most critical mechanisms in confidential computing (CC). We present a holistic verification approach enabling comprehensive and rigorous security analysis of architecturally-defined attestation mechanisms in CC. Specifically, we analyze two prominent nextgeneration hardware-based Trusted Execution Environments (TEEs), namely Arm Confidential Compute Architecture (CCA) and Intel Trust Domain Extensions (TDX). For both of these solutions, we provide a comprehensive specification of all phases of the attestation mechanism, namely provisioning, initialization, and attestation protocol. We demonstrate that including the initialization phase in the formal model leads to a violation of integrity, freshness, and secrecy properties for Intel’s claimed trusted computing base (TCB), which could not be captured by considering the attestation protocol alone in the related work. We opensource our artifacts. Other researchers, including a team from Intel, are adopting our artifacts for further analysis.
- Andere Ausgabe
- Link zum Artikel, der zuerst in der Zeitschrift „IEEE access” bei IEEE erschienen ist.
DOI: 10.1109/ACCESS.2023.3346501 - Freie Schlagwörter (EN)
- Arm confidential compute architecture (CCA), confidential computing, formal specification, Intel trust domain extensions (TDX), remote attestation, trusted execution environment.
- Klassifikation (DDC)
- 004
- 621,3
- Verlag
- IEEE, New York, NY
- Version / Begutachtungsstatus
- publizierte Version / Verlagsversion
- URN Qucosa
- urn:nbn:de:bsz:14-qucosa2-967631
- Veröffentlichungsdatum Qucosa
- 18.06.2025
- Dokumenttyp
- Artikel
- Sprache des Dokumentes
- Englisch
- Lizenz / Rechtehinweis
CC BY 4.0