Specification and Formal Analysis of Attestation Mechanisms in Confidential

Guest Speaker: Muhammad Usama Sardar, TU Dresden, Germany

Location: EMG.83 Robotarium Seminar Room, School of Mathematical and Computer Sciences (MACS), Earl Mountbatten building, First Gait, Heriot-Watt University Edinburgh Campus, Edinburgh EH14 4AS

Abstract:

Attestation is one of the most critical mechanisms in confidential computing (CC). This talk presents a novel approach based on the combination of Trusted Execution Environment (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.

Talk done joint with Cybersec / LAIV / DSG

About our Speaker:

Muhammad Usama Sardar

He 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 CCC Attestation 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, Principles of Dependable Systems, and Software Fault Tolerance.

** Notes:

We will have some snacks and drinks for free during the seminar, if you have any dietary requirements please let us know when you book the ticket.

Event Venue & Nearby Stays

HWU School of Mathematical & Computer Sciences, Floor0, Heriot-Watt University Edinburgh Campus, Edinburgh, United Kingdom

Concerts, fests, parties, meetups - all the happenings, one place.

Get App