Formal Specification and Verification of Architecturally-defined Attestation Mechanisms in Arm CCA and Intel TDX

Download
pdf

ABSTRACT

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 next-generation 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 open-source our artifacts. Other researchers, including a team from Intel, are adopting our artifacts for further analysis.

 

BIO

Muhammad Usama Sardar 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 formal specification project in Confidential Computing Consortium (CCC) Attestation Special Interest Group (SIG), and contributes to various research networks, such as EuroProofNet (WG3), Méthodes formelles pour la sécurité, Internet Engineering Task Force (IETF) Remote ATtestation procedureS (RATS) WG, Transport Layer Security (TLS) WG, and Trusted Execution Environment Provisioning (TEEP) WG, and Internet Research Task Force (IRTF) Usable Formal Methods Research Group (UFMRG). He is also a tutor for the master’s courses

Thomas Fossati is an engineer in the Linux kernel working group at Linaro.

Simon Frost is a Software Architect in the Architecture and Technology Group at Arm.

Shale Xiong is a Research Engineer in the Architecture and Technology Group at Arm. He specializes in formal verification and programming languages. Previously, he received PhD in computer science from Imperial College London in 2019.

 

 

Tags:
License: CC-2.5
Submitted by Regan Williams on