Formally Verifying Trusted Execution Environments with UCLID5

Pranav Gaddamadugu

EECS Department, University of California, Berkeley

Technical Report No. UCB/EECS-2021-200

August 13, 2021

This publication is archived. It is kept only for reference purposes, so it is no longer being updated and may not meet accessibility standards. If you need this content in a different format, please email webteam@eecs.berkeley.edu.

http://www2.eecs.berkeley.edu/Pubs/TechRpts/2021/Archive/EECS-2021-200.pdf

Hardware enclaves provide integrity and confidentiality guarantees of a remote execution on a machine owned by an untrusted third party using hardware-enforced isolation and attestation mechanisms. Although the sophistication of enclave designs has been increasing, few are formally verified. In this work, we use a formal tool, called UCLID5, to model and verify an abstract enclave platform. We then extend our standard model to encompass a novel extension of the Keystone enclave platform called Cerberus, which enables secure and efficient multiprocessing inside enclaves and reduces enclave initialization latency. We use UCLID5 to formally verify that Cerberus provides strong integrity and confidentiality guarantees to enclave programs.

Advisors: Sanjit A. Seshia

BibTeX citation:

@mastersthesis{Gaddamadugu:EECS-2021-200,
    Author= {Gaddamadugu, Pranav},
    Title= {Formally Verifying Trusted Execution Environments with UCLID5},
    School= {EECS Department, University of California, Berkeley},
    Year= {2021},
    Month= {Aug},
    Url= {http://www2.eecs.berkeley.edu/Pubs/TechRpts/2021/EECS-2021-200.html},
    Number= {UCB/EECS-2021-200},
    Abstract= {Hardware enclaves provide integrity and confidentiality guarantees of a remote execution on a machine owned by an untrusted third party using hardware-enforced isolation and attestation mechanisms. Although the sophistication of enclave designs has been increasing, few are formally verified. In this work, we use a formal tool, called UCLID5, to model and verify an abstract enclave platform. We then extend our standard model to encompass a novel extension of the Keystone enclave platform called Cerberus, which enables secure and efficient multiprocessing inside enclaves and reduces enclave initialization latency. We use UCLID5 to formally verify that Cerberus provides strong integrity and confidentiality guarantees to enclave programs.},
}

EndNote citation:

%0 Thesis
%A Gaddamadugu, Pranav 
%T Formally Verifying Trusted Execution Environments with UCLID5
%I EECS Department, University of California, Berkeley
%D 2021
%8 August 13
%@ UCB/EECS-2021-200
%U http://www2.eecs.berkeley.edu/Pubs/TechRpts/2021/EECS-2021-200.html
%F Gaddamadugu:EECS-2021-200