Loading Seminars

« All Seminars

  • This seminar has passed.

Comprehensive Specification and Formal Analysis of Attestation Mechanisms in Confidential Computing

June 28 (2023) @ 3:00 pm - 4:00 pm

Confidential Computing (CC) using hardware-based Trusted Execution Environments (TEEs) has emerged as a promising solution for protecting sensitive data in all forms. One of the fundamental characteristics of such TEEs is remote attestation which provides mechanisms for securely measuring and reporting the state of the remote platform and computing environment to a user. We present a novel approach combining TEE-agnostic attestation architecture and formal analysis enabling comprehensive and rigorous security analysis of attestation mechanisms in CC. We demonstrate the application of our approach for three prominent industrial representatives, namely Arm Confidential Compute Architecture (CCA) in architecture lead solutions, Intel Trust Domain Extensions (TDX) in vendor solutions, and Secure CONtainer Environment (SCONE) in frameworks. For each of these solutions, we provide a comprehensive specification of all phases of the attestation mechanism in confidential computing, namely provisioning, initialization, and attestation protocol. Our approach reveals design and security issues in Intel TDX and SCONE attestation. The talk is based on joint work [1] with Thomas Fossati and Simon Frost from Arm.

This is a joint seminar with FM-SEC.

Attendance via Zoom (ID:962 3227 7992, Passcode: 856952)
Livestream via Youtube


June 28 (2023)
3:00 pm - 4:00 pm
Seminar Tags:
, , ,




Muhammad Usama Sardar (TU Dresden)

Muhammad Usama Sardar is a Research Associate at TU Dresden working for the Transregional Collaborative Research Centre 248 "Foundations of Perspicuous Software Systems" (CPEC) since October 2021. His current research focuses on the formal specification and verification of architecturally-defined remote attestation for confidential computing, specifically Intel SGX, TDX and Arm CCA. He leads the recently accepted formal specification project in Confidential Computing Consortium (CCC) Attestation Special Interest Group (SIG), and contributes to various research networks, such as EuroProofNet (WG3), Open Compute Project (OCP), and Méthodes formelles pour la sécurité. He is also a tutor for the master’s courses: Systems Engineering 1, Principles of Dependable Systems, and Software Fault Tolerance.