PSec: Programming Secure Distributed Systems using Enclaves
Shivendra Kushwah, Ankush Desai, Pramod Subramanyan, Sanjit A. Seshia · 2021
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.