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

SaTC：CORE：中：多核处理器中可证明安全、可用且高性能的 Enclave

• 批准号: 2115587
• 负责人: Srini Devadas
• 金额: $ 120万
• 依托单位: Massachusetts Institute of Technology
• 依托单位国家: 美国
• 项目类别: Continuing Grant
• 财政年份: 2021
• 资助国家: 美国
• 起止时间: 2021-10-01 至 2024-09-30
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=2115587&HistoricalAwards=false
• 关键词: SaTC; CORE; Medium; Provably; Secure

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.

在云计算和当今其他流行的计算机使用模式中，一台物理计算机由彼此不信任的用户贡献的不同应用程序共享。 共享计算机的资源必须在用户之间安全地划分;错误允许一个用户了解另一个用户的秘密或影响另一个应用程序的执行。 解决应用程序之间相互保护的挑战的一种有前途的方法是飞地，最著名的是自2015年以来推出的英特尔SGX架构，但SGX允许在应用程序执行时泄露机密。 该项目开发具有强大保护的飞地，专注于可用性，性能和保证。 首先，飞地在生产中仍然很少使用，因此该项目研究了简化硬件资源共享的新接口。 其次，为了激励社区采用，开发的安全区包含硬件优化，以免影响应用程序的运行时性能。第三，该项目开发硬件安全性的数学证明技术。 用于飞地的软件API设计中的计划方法包括有限的I/O通道接口（例如，强制执行固定的或相对可预测的调度）和新的灵活的分配资源的手段，如跨飞地的高速缓存行。 通过对存储器管理硬件的修改来实现新的飞地到飞地通信原语。 这些机制被证明是安全的最高标准的数学严谨性，通过机器检查的证明与Coq定理证明。 该技术是为了证明特定的飞地系统周期准确地模拟由基本网络连接的单独计算机组（每个飞地一个），并且通过将证明义务非明显地分解为不同组件的本地化安全条件（例如，处理器与存储器系统）。 这项研究产生了可用的飞地系统，研究人员将其作为亚马逊F1云FPGA系统的映像提供给公众，便于安全评估或扩展工作。该奖项反映了NSF的法定使命，并通过使用基金会的知识价值和更广泛的影响审查标准进行评估，被认为值得支持。