A Design and Verification Methodology for Secure Isolated Regions

Rohit Sinha, Manuel Costa, Akash Lal, Nuno P. Lopes, Sriram Rajamani, Sanjit A. Seshia, and Kapil Vaswani. A Design and Verification Methodology for Secure Isolated Regions. In Proceedings of the 37th annual ACM SIGPLAN conference on Programming Language Design and Implementation (PLDI), pp. 665–681, June 2016.

Download

[pdf] 

Abstract

Hardware support for isolated execution (such as Intel SGX) enables development of applications that keep their code and data confidential even while running on a hostile or compromised host. However, automatically verifying that such applications satisfy confidentiality remains challenging. We present a methodology for designing such applications in a way that enables certifying their confidentiality. Our methodology consists of forcing the application to communicate with the external world through a narrow interface, compiling it with runtime checks that aid verification, and linking it with a small runtime library that implements the interface. The runtime library includes core services such as secure communication channels and memory management. We formalize this restriction on the application as Information Release Confinement (IRC), and we show that it allows us to decompose the task of proving confidentiality into (a) one-time, human-assisted functional verification of the runtime to ensure that it does not leak secrets, (b) automatic verification of the application's machine code to ensure that it satisfies IRC and does not directly read or corrupt the runtime's internal state. We present slash-confidential: a verifier for IRC that is modular, automatic, and keeps our compiler out of the trusted computing base. Our evaluation suggests that the methodology scales to real-world applications.

BibTeX

@inproceedings{sinha-pldi16,
  author = {Sinha, Rohit and Manuel Costa and Akash Lal and Nuno P. Lopes and Rajamani, Sriram and Seshia, Sanjit A. and Vaswani, Kapil},
  title     = {A Design and Verification Methodology for Secure Isolated Regions},
  booktitle = {Proceedings of the 37th annual ACM SIGPLAN conference on Programming Language Design and Implementation (PLDI)},
  Year = {2016},
  Month = {June},
  pages = "665--681",
  abstract = {Hardware support for isolated execution (such as Intel SGX) enables development 
of applications that keep their code and data confidential 
even while running on a hostile or compromised host. 
However, automatically verifying that such applications satisfy confidentiality 
remains challenging.  We present a methodology for designing such applications 
in a way that enables certifying their confidentiality.  
Our methodology consists of forcing the application to communicate with the 
external world through a narrow interface,  
compiling it with runtime checks that aid verification, 
and linking it with a small runtime library that implements the interface. 
The runtime library includes core services such as secure communication channels and memory management. 
We formalize this restriction on the application as Information Release Confinement (IRC), 
and we show that it allows us to decompose the task of 
proving confidentiality into (a) one-time, human-assisted functional verification of 
the runtime to ensure that it does not leak secrets, (b) automatic verification of the application's 
machine code to ensure that it satisfies IRC and does not directly read or corrupt the 
runtime's internal state.  
We present slash-confidential: a verifier for IRC that is modular, automatic, and keeps our compiler out 
of the trusted computing base. 
Our evaluation suggests that the methodology scales to real-world applications.  
},
}