PSec: Programming Secure Distributed Systems using Enclaves

Shivendra Kushwah, Ankush Desai, Pramod Subramanyan, and Sanjit A. Seshia. PSec: Programming Secure Distributed Systems using Enclaves. In ACM Asia Conference on Computer and Communications Security (ASIACCS), pp. 802–816, ACM, 2021.

Download

[pdf] 

Abstract

We introduce PSec, a domain-specific language for programming secure distributed systems. PSec is a state-machine based programming language with information flow control capabilities that leverages Intel SGX enclaves to provide security guarantees at runtime. Combining state machines and information flow control with hardware enclaves enables programmers to build complex distributed systems without inadvertently leaking sensitive information to adversaries. We formally prove the security properties of PSec and evaluate our work by programming several real-world examples, including One Time Passcode and Secure Electronic Voting systems. We present performance results of PSec systems and show that there is an acceptable performance overhead of approximately 3x for long running systems with a possible minimum of approximately 1.2x, as compared to baseline systems that do not provide any security guarantees.

BibTeX

@inproceedings{kushwah-asiaccs21,
  author    = {Shivendra Kushwah and
               Ankush Desai and
               Pramod Subramanyan and
               Sanjit A. Seshia},
  title     = {{PSec}: Programming Secure Distributed Systems using Enclaves},
  booktitle = {{ACM} Asia Conference on Computer and Communications Security (ASIACCS)},
  pages     = {802--816},
  publisher = {{ACM}},
  year      = {2021},
  abstract  = {We introduce PSec, a domain-specific language for programming secure distributed systems. PSec is a state-machine based programming language with information flow control capabilities that leverages Intel SGX enclaves to provide security guarantees at runtime. Combining state machines and information flow control with hardware enclaves enables programmers to build complex distributed systems without inadvertently leaking sensitive information to adversaries. We formally prove the security properties of PSec and evaluate our work by programming several real-world examples, including One Time Passcode and Secure Electronic Voting systems. We present performance results of PSec systems and show that there is an acceptable performance overhead of approximately 3x for long running systems with a possible minimum of approximately 1.2x, as compared to baseline systems that do not provide any security guarantees.},
}