Verification of Confidentiality Properties of Enclave Programs

  • Authors:
    Rohit Sinha (UC/Berkeley), Sriram K. Rajamani (Microsoft), Sanjit Seshia (UC/Berkeley), Kapil Vaswani (Microsoft)
    Publication ID:
    Publication Type:
    Received Date:
    Last Edit Date:
    2460.001 (University of California/Berkeley)


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 data center administrators. To help protect application secrets from such attacks, there is increasing interest in hardware implementations of primitives for trusted computing, such as Intel 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) 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.

Past Events

  Event Summary
20–22 September 2015
Sunday, Sept. 20, 2015, 8 a.m. — Tuesday, Sept. 22, 2015, 10 p.m. CT
Austin, TX, United States
Technical conference and networking event for SRC members and students.

4819 Emperor Blvd, Suite 300 Durham, NC 27703 Voice: (919) 941-9400 Fax: (919) 941-9450

Important Information for the SRC website. This site uses cookies to store information on your computer. By continuing to use our site, you consent to our cookies. If you are not happy with the use of these cookies, please review our Cookie Policy to learn how they can be disabled. By disabling cookies, some features of the site will not work.