Rohit Sinha and Sriram Rajamani and Sanjit A. Seshia and Kapil Vaswani

EECS Department, University of California, Berkeley

Technical Report No. UCB/EECS-2015-162

June 1, 2015

http://www2.eecs.berkeley.edu/Pubs/TechRpts/2015/EECS-2015-162.pdf

Security-critical applications running in the cloud constantly face threats from exploits in lower computing layers such as the operating system, virtual machine monitors, or even attacks from malicious datacenter administrators. To help protect application secrets from such attacks, there is increasing interest in hardware implementations of primitives for trusted computing, such as Intel’s Software Guard Extensions (SGX). These primitives enable hardware protection of memory regions containing code and data, root of trust for measurement, remote attestation, and cryptographic sealing. However, vulnerabilities in the application itself (e.g. incorrect use of SGX instructions, memory safety errors) can be exploited to divulge secrets. We introduce Moat, a tool which formally verifies confidentiality properties of applications running on SGX. We create formal models of relevant aspects of SGX, develop several adversary models, and present a verification methodology for proving that an application running on SGX does not contain a vulnerability that causes it to reveal secrets to the adversary. We evaluate Moat on several applications, including a one time password scheme, off-the-record messaging, notary service, and secure query processing.

---

BibTeX citation:

@techreport{Sinha:EECS-2015-162,
    Author= {Sinha, Rohit and Rajamani, Sriram and Seshia, Sanjit A. and Vaswani, Kapil},
    Title= {Verification of Confidentiality Properties of Enclave Programs},
    Year= {2015},
    Month= {Jun},
    Url= {http://www2.eecs.berkeley.edu/Pubs/TechRpts/2015/EECS-2015-162.html},
    Number= {UCB/EECS-2015-162},
    Abstract= {Security-critical applications running in the cloud constantly face threats from exploits in lower computing layers such as the operating system, virtual machine monitors, or even attacks from malicious datacenter administrators. To help protect application secrets from such attacks, there is increasing interest in hardware implementations of primitives for trusted computing, such as Intel’s Software Guard Extensions (SGX). These primitives enable hardware protection of memory regions containing code and data, root of trust for measurement, remote attestation, and cryptographic sealing. However, vulnerabilities in the application itself (e.g. incorrect use of SGX instructions, memory safety errors) can be exploited to divulge secrets. We introduce Moat, a tool which formally verifies confidentiality properties of applications running on SGX. We create formal models of relevant aspects of SGX, develop several adversary models, and present a verification methodology for proving that an application running on SGX does not contain a vulnerability that causes it to reveal secrets to the adversary. We evaluate Moat on several applications, including a one time password scheme, off-the-record messaging, notary service, and secure query processing.},
}

EndNote citation:

%0 Report
%A Sinha, Rohit 
%A Rajamani, Sriram 
%A Seshia, Sanjit A. 
%A Vaswani, Kapil 
%T Verification of Confidentiality Properties of Enclave Programs
%I EECS Department, University of California, Berkeley
%D 2015
%8 June 1
%@ UCB/EECS-2015-162
%U http://www2.eecs.berkeley.edu/Pubs/TechRpts/2015/EECS-2015-162.html
%F Sinha:EECS-2015-162