Pranav Gaddamadugu

EECS Department, University of California, Berkeley

Technical Report No. UCB/EECS-2021-200

August 13, 2021

http://www2.eecs.berkeley.edu/Pubs/TechRpts/2021/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