Evaluating SGX’s Remote Attestation Security Through the Analysis of Copland Phrases

Veloz Baez, Freddy

Etd

Evaluating SGX’s Remote Attestation Security Through the Analysis of Copland Phrases

Public

SGX is a set of extensions to Intel’s chip architecture that allows a process to run securely in an isolated computing environment known as an enclave and store secrets that cannot be accessed by the system in which the process is located. This gives the necessary assurance to a remote party that the computations being run in the enclave can be trusted, which is a vital requirement in cloud computing. SGX achieve this via remote attestation, the process of receiving evidence over a network about the state of a target machine and appraising it. In this work, we use Copland, a declarative language created to codify the intricacies of layered attestation protocols, to express SGX’s attestation processes. We also analyze the different components that participate in the protocols and identify limitations that may be exploited, as well as other components that could potentially be future targets. We achieve these goals by analyzing the SGX Copland phrases with Chase, a model-finder tool presented by Rowe et al. that can find possible attack scenarios in an attestation protocol. By considering different assumptions and attack targets and producing seldom adversary scenarios, we are able to give insights into SGX’s attestation security. Additionally, we explore some limitations in the way Copland can describe complex attestation protocols like SGX, the implications of these obstacles and how to respond to them when analyzing Copland phrases.

Creator