Intel Trust Domain Extensions (TDX) is the upcoming trusted execution environment offering of Intel. One of the most critical processes of Intel TDX is the remote attestation mechanism. In this talk, we expose some of the discrepancies in Intel’s specifications of remote attestation that may potentially lead to design and implementation flaws. We explain how formal specification and verification using ProVerif could help avoid these flaws.

 

Muhammad Usama Sardar has been a Research Associate at TU Dresden since October of 2021. Previously, he received the prestigious DAAD research grant from May 2017 until September 2021 for his Ph.D. at TU Dresden. 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). His current research interests include the formal specification and verification of the remote attestation process in Trusted Execution Environments, with a special focus on Intel SGX and TDX.

Christof Fetzer's research focuses on Trusted Execution and Dependable Computing. He is a founder of CloudHeat GmbH, SIListra Systems GmbH, and Scontain UG. He has been a Professor at TU Dresden, Germany since 2004 and he received his Ph.D. from the University of California, San Diego.