Description
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.