Muhammad Usama Sardar

He has been 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 focus is on the formal specification and verification of attested TLS for confidential computing. He leads the TEE formal specification project as well as the recently approved KBS formal verification project in Confidential Computing Consortium (CCC) Attestation Special Interest Group (SIG). He also contributes to various research networks, such as EuroProofNet (WG3), Méthodes formelles pour la sécurité, Internet Research Task Force (IRTF) Usable Formal Methods Research Group (UFMRG), as well as engineering networks, such as Internet Engineering Task Force (IETF) Remote ATtestation procedureS (RATS) WG, Transport Layer Security (TLS) WG, and Trusted Execution Environment Provisioning (TEEP) WG. He is also a tutor for the master’s courses: Systems Engineering 1, Principles of Dependable Systems, and Software Fault Tolerance.

Previously, he received the prestigious DAAD research grant from May 2017 till September 2021 at TU Dresden. He has done his masters from the School of Electrical Engineering and Computer Sciences (SEECS) at the National University of Sciences and Technology (NUST), Pakistan in 2015 with 2^nd position in his batch. His master’s dissertation was on the formal verification of distributed dynamic thermal management schemes, in collaboration with the Chair for Embedded Systems (CES) at the Karlsruhe Institute of Technology (KIT), Germany.

He has received best poster award in Postgraduate category in the International Conference on Digital Futures and Transformative Technologies (ICoDT2) in 2021, South Asia Triple Helix Association (SATHA) Innovation Award in 2018, best researcher of the year award in System Analysis and Verification lab in Pakistan in 2017, and best speaker awards at Workshop on Applications in ASIC Design (December 2016) and Workshop on Recent Trends in Theorem Proving (April 2016).

Contact information

Email:	muhammad_usama<dot>sardar<at>tu<minus>dresden<dot>de
Phone:	+49 351 463-42048
Office:	APB 3073

Research Interests

Confidential Computing
Trusted Execution Environments (specifically, Intel SGX, TDX and Arm CCA)
Remote Attestation
Formal Specification
(Applied) Formal Methods
Systems Security

Preprints

M. U. Sardar, T. Fossati, S. Frost, SoK: Attestation in Confidential Computing, 2022. [BibTeX]

Peer-reviewed Publications

Full papers

M. U. Sardar, T. Fossati, S. Frost, S. Xiong, Formal Specification and Verification of Architecturally-defined Attestation Mechanisms in Arm CCA and Intel TDX, IEEE Access, 2024. [Preprint] [Published version] [BibTeX]
G. P. Fernandez, A. Brito, A. P. P. Hartono, M. U. Sardar, C. Fetzer, A Last-Level Defense for Application Integrity and Confidentiality, 16th IEEE/ACM International Conference on Utility and Cloud Computing (UCC 2023), 4-7 December, 2023. [Preprint]
M. U. Sardar, C. Fetzer, Confidential Computing and Related Technologies: A Critical Review, Cybersecurity, 2023. [Preprint] [Published version] [Slides] [Video] [BibTeX]
M. U. Sardar, S. Musaev, C. Fetzer, Demystifying Attestation in Intel Trust Domain Extensions via Formal Verification, IEEE Access, 2021. [Preprint] [Published version] [BibTeX]
M. U. Sardar, R. Faqeh, C. Fetzer, Formal Foundations for Intel SGX Data Center Attestation Primitives, International Conference on Formal Engineering Methods (ICFEM), Singapore, 1-3 March 2021. [Preprint] [Published version] [BibTeX]
M. U. Sardar, D. L. Quoc, C. Fetzer, Towards Formalization of Enhanced Privacy ID (EPID)-based Remote Attestation in Intel SGX, Euromicro Conference on Digital System Design (DSD), Portorož, Slovenia, 26-28 August 2020. [Preprint] [Published version] [BibTeX]

Short/Perspective papers

M. U. Sardar, Understanding Trust Assumptions for Attestation in Confidential Computing, Doctoral Forum at 52nd Annual IEEE/IFIP International Conference on Dependable Systems and Networks (DSN 2022), Baltimore, Maryland, USA, 27-30 June, 2022. [Teaser video] [Full video] [Preprint] [Published version] [BibTeX]
M. U. Sardar, C. Fetzer, Formal Foundations for SCONE Attestation, 52nd Annual IEEE/IFIP International Conference on Dependable Systems and Networks (DSN 2022), Baltimore, Maryland, USA, 27-30 June, 2022. [Fast Abstract] [Teaser video][P reprint] [Published version] [BibTeX]

For a complete list of publications, see here

Invited Talks (without Formal Proceedings)

M. U. Sardar, A. Niemi, H. Tschofenig, T. Fossati, A rollercoaster ride on the formal analysis of attested TLS, Huawei, 8 Feb 2024 (online).
M. U. Sardar, T. Fossati, S. Frost, Comprehensive Specification and Formal Analysis of Attestation Mechanisms in Confidential Computing,

Heriot-Watt University, Edinburgh, UK, 17 May, 2023. [Joining details] [slides]
M. U. Sardar, T. Fossati, S. Frost, Comprehensive Specification and Formal Analysis of Attestation Mechanisms in Confidential Computing,

University of Edinburgh, Edinburgh, UK, 16 May, 2023. [Joining details] [Slides] [Video]
M. U. Sardar, T. Fossati, S. Frost, SoK: Attestation in Confidential Computing,

CISPA Helmholtz Center for Information Security, Saarbrücken, 15 Mar, 2023. [slides]
M. U. Sardar, T. Fossati, S. Frost, SoK: Attestation in Confidential Computing,

University of Luxembourg - Université du Luxembourg, Luxembourg, 13-14 Mar, 2023. [slides]
C. Fetzer, M. U. Sardar, Formal Foundations for SCONE attestation and Intel SGX Data Center Attestation Primitives, PAVeTrust, 2021. [Extended Abstract]
M. U. Sardar, C. Fetzer, Demystifying Attestation in Intel TDX via Formal Verification, invited talk at Confidential Computing Sweden meetup, 7 October 2021.

Tutorial (without Formal Proceedings)

M. U. Sardar, Attestation in Confidential Computing, International Conference on Emerging Trends in Smart Technologies (ICETST), Karachi, Pakistan, 23-24 September, 2022.

Recent and Upcoming Talks (without Formal Proceedings)

M. U. Sardar, Attested TLS and formalization, Confidential Computing Summit 2024, San Francisco, USA, 5-6 June, 2024. (Looking for sponsors)
M. U. Sardar, Challenges in the formal verification of attested TLS, Attested TLS workshop at Linaro Conenct, Madrid, Spain, 16 May, 2024. (Looking for sponsors)
Y. Deshpande, M. U. Sardar, Attested TLS and formalization, 2024 OCP Regional Summit, Lisbon, Portugal, 24-25 April, 2024. (Thanks to Swisstronik and softwEre education for funding)
M. U. Sardar, A. Niemi, H. Tschofenig, T. Fossati, Towards formal verification of attested TLS: Potential replay attacks on RA-TLS, 11th Workshop on Horn Clauses for Verification and Synthesis, Luxembourg, 7 April 2024. (Thanks to Veraison for funding)
M. U. Sardar, A. Niemi, H. Tschofenig, T. Fossati, Towards formal verification of attested TLS: Potential replay attacks on RA-TLS, 2024 Annual Meeting of the WG "Formal Methods in Security", Saint Pierre d’Oléron (France), 3-5 Apr 2024.
M. U. Sardar, T. Fossati, S. Frost, S. Xiong, Formal Specification and Verification of Architecturally-defined Attestation Mechanisms in Arm CCA and Intel TDX, NSA Hot Topics in the Science of Security (HotSoS) Symposium, Virtual, 2-4 April, 2024.
M. U. Sardar, A. Niemi, H. Tschofenig, T. Fossati, A rollercoaster ride on the formal analysis of attested TLS, EuroProofNet Tutorial, Dresden, Germany, 28 March 2024.
M. U. Sardar, Formal Analysis of RA-TLS, Crypto Forum Research Group (CFRG) @ IETF Meeting 119, 18 March 2024 (online) [slides]
M. U. Sardar, A. Niemi, H. Tschofenig, T. Fossati, A rollercoaster ride on the formal analysis of attested TLS, CCC Attestation SIG, 30 Jan 2024 (online). [slides]
M. U. Sardar, Towards Formal Specification and Verification of Attestation in Arm CCA and Intel TDX, Program Analysis and Verification on Trusted Platforms (PAVeTrust) 2023, Austin, Texas, USA (Virtual), 5 December, 2023. (Thanks to TBTL for funding) [slides]
M. U. Sardar, Perspicuity of Attestation Mechanisms in Confidential Computing, 24th International Conference on Formal Engineering Methods (ICFEM 2023), Brisbane, Australia, 21-24 November, 2023. (Thanks to TBTL for partial funding) [slides]
M. U. Sardar, Formal Specification and Verification of Attestation in Confidential Computing, IETF 118, Prague, Czechia, 4-10 November, 2023. [slides]
M. U. Sardar, Formal Specification and Verification of Attestation in Confidential Computing, Hardware and Architectural Support for Security and Privacy (HASP) 2023, Toronto, Canada (Virtual), 29 October, 2023. [slides] (Thanks to Flashbots for funding)
M. U. Sardar, T. Fossati, S. Frost, Formal Specification and Verification of Attestation in Confidential Computing, Confidential Computing Mini Summit (co-located with OSS EU), Bilbao, Spain, 18 September 2023. [slides] (Thanks to CCC for funding)
M. U. Sardar, T. Fossati, S. Frost, Formal Specification and Verification of Attestation in Confidential Computing, 16^th Conference on Intelligent Computer Mathematics, Cambridge, UK (Virtual), 6 September 2023. [slides]
M. U. Sardar, T. Fossati, S. Frost, Understanding Trust Assumptions for Remote Attestation via Formal Verification, Highlights of Logic, Games and Automata, Kassel, Germany, 24-28 July 2023. (Thanks to Secretarium for funding) [slides]
M. U. Sardar, T. Fossati, S. Frost, Comprehensive Specification and Formal Analysis of Attestation Mechanisms in Confidential Computing, 16th Interaction and Concurrency Experience, Lisbon, Portugal, 19 June, 2023.
M. U. Sardar, T. Fossati, S. Frost, SoK: Attestation in Confidential Computing, short talk at 44th IEEE Symposium on Security and Privacy, San Francisco, USA, 23 May, 2023. (Thanks to TBTL, Flashbots and konVera for funding) [slides]
M. U. Sardar, T. Fossati, S. Frost, SoK: Attestation in Confidential Computing, 2023 OCP Regional Summit, Prague, Czech Republic, 19-20 April, 2023. [slides]
M. U. Sardar, T. Fossati, S. Frost, SoK: Attestation in Confidential Computing, Hot Topics in the Science of Security (HotSoS) Symposium, Virtual, 3-5 April, 2023. [slides]
M. U. Sardar, T. Fossati, S. Frost, SoK: Attestation in Confidential Computing, 2023 Annual Meeting of the WG "Formal Methods for Security", Roscoff, France, 28-30 Mar, 2023. [slides]
M. U. Sardar, Tools and Techniques for Symbolic Protocol Verification,
WG3 Program Verification Meeting of EuroProofNet, Timisoara, Romania, 8-9 Feb, 2023. [slides] (Thanks to EuroProofNet for funding)
M. U. Sardar, Towards SoK: Attestation in Confidential Computing, Program Analysis and Verification on Trusted Platforms (PAVeTrust) co-located with ACSAC, Austin, Texas, USA, 6 December, 2022. (Thanks to TBTL UK for funding)
M. U. Sardar, Towards SoK: Attestation in Confidential Computing, glsec22: Software engineering at the service of system, software and network security, Paris, France, 24 November, 2022.
M. U. Sardar, Understanding Trust Assumptions for Attestation in Confidential Computing, Student forum at Formal Methods in Computer-Aided Design (FMCAD), Trento, Italy, 17-21 October, 2022. (Thanks to FMCAD Association for funding)
M. U. Sardar, Work-in-Progress: Towards a Standard Architecture for Attestation in Confidential Computing, Hardware and Architectural Support for Security and Privacy (HASP) co-located with MICRO, Chicago, USA, 1 October, 2022.
M. U. Sardar, Understanding Trust Assumptions for Attestation in Confidential Computing, Doctoral programme at Conference on Intelligent Computer Mathematics (CICM), Tbilisi, Georgia, 19-23 September, 2022.
M. U. Sardar, Unveiling Security Through Obscurity Approach of Intel TDX Remote Attestation, Inria Paris, France, 7 September, 2022.
M. U. Sardar, Unveiling Security through Obscurity Approach of Intel TDX Remote Attestation, Workshop on Foundations of Computer Security 2022 (FCS'22), Haifa, Israel, 11 August, 2022.
M. U. Sardar, Experiences on Online Teaching of Formal Methods to Systems Engineering Students, Formal Methods Education Online (FOMEO): Tips, Tricks & Tools 2022, Haifa, Israel, July 31-August 1, 2022.
M. U. Sardar, C. Fetzer, Intel's Specification of TDX Remote Attestation: colossal mistake or company policy?, Computability in Europe: Revolutions and Revelations in Computability, Swansea, UK, 11-15 July 2022. [slides]
M. U. Sardar, C.Fetzer, Understanding Trust Assumptions for Remote Attestation via Formal Verification, Logic Colloquium, Reykjavik, Iceland, 27 June - 1 July 2022. [slides]
M. U. Sardar, Understanding Trust Assumptions for Remote Attestation via Formal Verification, Highlights of Logic, Games and Automata, Paris, France, 28 June-1 July 2022. [slides]
M. U. Sardar, Attestation in Confidential Computing, MobileCamp, Dresden, Germany, 25-26 June 2022. [slides]
M. U. Sardar, C. Fetzer, Demystifying Attestation in Intel Trust Domain Extensions (TDX) via Formal Verification, Eleventh Scandinavian Logic Symposium (SLSS 2022), Bergen, Norway, 17-19 June 2022. [slides]
M. U. Sardar, C. Fetzer, Demystifying Attestation in Intel Trust Domain Extensions (TDX) via Formal Verification, 15th Interaction and Concurrency Experience (ICE) 2022, Lucca, Italy, 17 June 2022. [slides]
M. U. Sardar, C. Fetzer, An Exciting Journey from Trust to Trustworthiness in Confidential Computing, DAAD Alumni & Friends Colloquium, 2 June 2022.
M. U. Sardar, Formats for Attestation in Intel TDX, Confidential Computing Consortium Attestation Special Interest Group (SIG), 24 May 2022. [Slides] [Video]
M. U. Sardar, C. Fetzer, Intel's Specification of TDX Remote Attestation: colossal mistake or company policy?, short talk at Symposium on Security and Privacy, 22-26 May 2022. [slides]
M. U. Sardar, An Exciting Journey from Trust to Trustworthiness in Confidential Computing, CPEC Young Researchers Colloquium Series, 29 April 2022.
M. U. Sardar, C. Fetzer, Demystifying Attestation in Intel Trust Domain Extensions via Formal Verification, Logic4Peace, 22-23 April 2022. [Slides]
M. U. Sardar, S. Musaev, C. Fetzer, Inconsistencies in Specification of Intel TDX Remote Attestation, 9th Annual Hot Topics in the Science of Security (HoTSoS) Symposium, 5-7 April 2022. [Slides]
M. U. Sardar, S. Musaev, C. Fetzer, Demystifying Attestation in Intel Trust Domain Extensions via Formal Verification, Horn Clauses for Verification and Synthesis (HCVS) colocated with ETAPS 2022, Munich, Germany, 3 April 2022.
M. U. Sardar, C. Fetzer, Formal Specification and Verification of Intel TDX Remote Attestation, Doctoral Symposium in conjunction with Information Assurance and Security, 17 December 2021.
M. U. Sardar, C. Fetzer, Confidential Computing and Related Technologies: A Review, PAVeTrust co-located with Annual Computer Security Applications Conference (ACSAC), 6 December 2021. [Preprint] [Slides] [Video]
M. U. Sardar, C. Fetzer, Confidential Computing, Science Communication at DART Symposium, 26 November 2021.
M. U. Sardar, Inconsistencies in Specification of Intel TDX Remote Attestation, Doctoral Symposium at FM2021, 20 November 2021. [Video]
M. U. Sardar, Inconsistencies in Specification of Intel TDX Remote Attestation, ACM student research competition at SOSP, 25-28 October 2021.
M. U. Sardar, Formal Verification for Secure Hardware Systems, Doctoral Symposium at Conference on Intelligent Computer Mathematics, 26-31 July 2021.
M. U. Sardar, C. Fetzer, Formal Analysis of Remote Attestation in Trusted Execution Environments, OUTPUT, 8 July 2021.
M. U. Sardar, C. Fetzer, Demystifying Trust Domain Attestation via Formal Verification, short talk at 34^th IEEE Computer Security Foundations Symposium, 21-24 June 2021. [Slides]
M. U. Sardar, S. Musaev, C. Fetzer, Demystifying Trust Domain Attestation via Formal Verification, short talk at Symposium on Security and Privacy, 24-27 May 2021. [Video] [Slides]
M. U. Sardar, C. Fetzer, Formal Analysis of Remote Attestation Protocols in Trusted Execution Environments, Tenth Summer School on Formal Techniques, 22-28 May 2021.
M. U. Sardar, C. Fetzer, Formal Foundations for Intel SGX Data Center Attestation Primitives, Huawei poster competition at International Conference on Digital Futures and Transformative Technologies (ICoDT2), 20-21 May 2021. [Best poster award in Postgraduate category] [Media1][Media2] [Media3]
M. U. Sardar, R. Faqeh, C. Fetzer, Formal Foundations for Intel SGX Data Center Attestation Primitives, 8th Annual Hot Topics in the Science of Security (HoTSoS) Symposium, 13-15 April 2021.
M. U. Sardar, C. Fetzer, Formal Foundations for Intel SGX Data Center Attestation Primitives, New England Hardware Security Day 2021, 9 April 2021.
M. U. Sardar, C. Fetzer, Understanding Remote Attestation in Intel SGX and TDX via Formal Verification, Gemeinsames Jahrestreffen der GI-Fachgruppen Deduktionssysteme und Logik in der Informatik, 26 March 2021.
M. U. Sardar, C. Fetzer, Formal Foundations for Attestation in Hyperledger Avalon, Blockchain Techfest 2020, 30 October 2020. [Video] [EPID Preprint][DCAP Preprint]
M. U. Sardar, C. Fetzer, Formal Foundations for Intel SGX Data Center Attestation Primitives, Arm Research Summit, 9-11 September 2020. [Video] [Slides] [Preprint]

Rump session talks

M. U. Sardar, Formal Specification of Intel TDX RA, Rump session at
2022 Annual Meeting of the WG "Formal Methods for Security", Fréjus (France), 21-23 Mar 2022.
M. U. Sardar, On the Technical Flaws in CCC White Paper: Episode 4/n, Rump session at Indocrypt 2021, 12-15 December 2021. [Slides]
M. U. Sardar, On the Technical Flaws in CCC White Paper: Episode 3/n, Rump session at Asiacrypt 2021, 6-10 December 2021. [Slides]
M. U. Sardar, On the Technical Flaws in CCC White Paper: Episode 2/n, Rump session at CHES 2021, 13-17 September 2021. [Video] [Slides]
M. U. Sardar, On the Technical Flaws in CCC White Paper, Rump session at Crypto, 16-20 August 2021. [Video] [Slides]