SaTC: CORE: Medium: Provably Secure, Usable, and Performant Enclaves in Multicore Processors

Massachusetts Institute Of Technology, Cambridge MA

Investigators

Abstract

In cloud computing and other popular modes of computer usage today, one physical computer is shared by different applications contributed by users who do not trust each other. The resources of the shared computer must be divided securely across the users; mistakes allow one user to learn another's secrets or influence another applications’ execution. A promising approach to address the challenge of protecting applications from one another is enclaves, best known through Intel's SGX architecture available since 2015, but SGX allows secrets to be leaked while applications execute. This project develops enclaves with strong protections, focusing on usability, performance, and assurance. First, enclaves have still been used relatively rarely in production, and the project therefore studies new interfaces that streamline the sharing of hardware resources. Second, to motivate adoption by the community, the developed enclaves encompass hardware optimizations so as not to affect runtime performance of applications. Third, the project develops techniques for mathematical proofs of hardware security. Planned approaches in software API design for enclaves include limited I/O channel interfaces (e.g., enforcing fixed or otherwise relatively predictable schedules) and new flexible means of allocating resources like cache lines across enclaves. New enclave-to-enclave communication primitives are realized through modifications to memory-management hardware. These mechanisms are being proved secure to the highest standards of mathematical rigor, through machine-checking of proofs with the Coq theorem prover. The technique is to prove that specific enclave systems cycle-accurately simulate groups of separate computers (one per enclave) connected by a basic network, and to prove such results modularly, via nonobvious decomposition of proof obligations into localized security conditions for different components (e.g., processor vs. memory system). This research produces usable enclave systems that the investigators make available to the public as images for Amazon's F1 cloud-FPGA system, facilitating easy bring-up for security evaluation or extending the work. This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.