Visible to the public Towards Formalization of Enhanced Privacy ID (EPID)-based Remote Attestation in Intel SGX

TitleTowards Formalization of Enhanced Privacy ID (EPID)-based Remote Attestation in Intel SGX
Publication TypeConference Paper
Year of Publication2020
AuthorsSardar, Muhammad Usama, Quoc, Do Le, Fetzer, Christof
Conference Name2020 23rd Euromicro Conference on Digital System Design (DSD)
Date PublishedAug. 2020
ISBN Number978-1-7281-9535-3
Keywordsattestation, composability, Computational modeling, cryptography, Enhanced Privacy ID (EPID), formal verification, Human Behavior, Intel SGX, privacy, Protocols, pubcrawl, remote attestation, resilience, Resiliency, Software, Testing, Trusted Execution Environment

Vulnerabilities in privileged software layers have been exploited with severe consequences. Recently, Trusted Execution Environments (TEEs) based technologies have emerged as a promising approach since they claim strong confidentiality and integrity guarantees regardless of the trustworthiness of the underlying system software. In this paper, we consider one of the most prominent TEE technologies, referred to as Intel Software Guard Extensions (SGX). Despite many formal approaches, there is still a lack of formal proof of some critical processes of Intel SGX, such as remote attestation. To fill this gap, we propose a fully automated, rigorous, and sound formal approach to specify and verify the Enhanced Privacy ID (EPID)-based remote attestation in Intel SGX under the assumption that there are no side-channel attacks and no vulnerabilities inside the enclave. The evaluation indicates that the confidentiality of attestation keys is preserved against a Dolev-Yao adversary in this technology. We also present a few of the many inconsistencies found in the existing literature on Intel SGX attestation during formal specification.

Citation Keysardar_towards_2020