PPoSS: Planning: High-Performance Certified Trust for Global-Scale Applications

PPoSS：规划：全球规模应用程序的高性能认证信任

• 批准号: 2118851
• 负责人: Zhong Shao
• 金额: $ 25万
• 依托单位: Yale University
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2021
• 资助国家: 美国
• 起止时间: 2021-10-01 至 2022-09-30
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=2118851&HistoricalAwards=false
• 关键词: PPoSS; Planning; Performance; Certified; Trust

A global-scale public infrastructure of distributed computing resources, in the form of data centers of various scales, has emerged in the past decade. Today, a user of this global infrastructure must trust the infrastructure vendors based on their informal textual contracts. This trust model provides limited legal protection of user interests and has become a key barrier for more services to migrate into the public infrastructure, stymieing innovation and competition. This project's key novelty is to build highly performant, certified execution environments (CEEs) for large-scale distributed systems. In doing so, the project explores, refines, and discovers design principles for scaling certified trust --- specifically, scaling up to include the entire software stack, and scaling out to include globally distributed resources. The project's main impact is to enable and promote trustworthy, performant, cost-effective uses of the public global infrastructure, empowering applications and services for a global market. Specifically it will lower the barrier of entrance for startups to enter a global market and as a result, foster competition and innovation, and make information technologies more accessible. It is intended to profoundly change many industries that traditionally heavily rely on proprietary IT infrastructures, e.g., mobile networks. The project makes three related scientific contributions. First, it contributes new technologies for building distributed CEE enclaves for running global-scale applications. CEEs extend remote attestation (as in trusted execution environments (TEEs)) with formal verification so the chain of trust can be used to establish not only the authenticity of enclave binaries but also the trustworthiness properties. Second, it provides hardware and software support to accelerate the underlying mechanisms for isolation, integrity, and confidentiality. These themes range from support for better isolation to CPUs and TEEs, but also include fast mechanisms for emerging hardware accelerators. Finally, the team of researchers explores the extension of certifiably trustworthy execution environments to emerging disaggregated datacenter designs using a software-defined-network-based decomposition of functionalities. The insights gleaned from their study guide the development of new algorithm-driven, data structure-driven, and hardware-driven solutions for the trustworthy disaggregated cloud design. During the Planning stage, the investigators are developing a prototype testbed to evaluate the feasibility of building a high-performance trustworthy global-scale mobile network using cloud-scale disaggregated CEEs. They are compiling a list of challenges which become the central research agenda for a full-scale, large proposal.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.

在过去十年中，以各种规模的数据中心的形式出现了全球范围的分布式计算资源公共基础设施。如今，这种全球基础设施的用户必须根据非正式的文本合同信任基础设施供应商。 这种信任模式对用户利益的法律保护有限，已成为更多服务迁移到公共基础设施、阻碍创新和竞争的关键障碍。 该项目的主要新颖之处在于为大型分布式系统构建高性能、经过认证的执行环境（CEE）。在此过程中，该项目探索、完善和发现了扩展认证信任的设计原则——具体来说，向上扩展以包括整个软件堆栈，并向外扩展以包括全球分布的资源。 该项目的主要影响是实现和促进全球公共基础设施的可信、高性能、经济高效的使用，为全球市场提供应用程序和服务。具体来说，它将降低初创企业进入全球市场的门槛，从而促进竞争和创新，并使信息技术更容易获得。它旨在深刻改变许多传统上严重依赖专有 IT 基础设施（例如移动网络）的行业。该项目做出了三项相关的科学贡献。首先，它贡献了构建分布式 CEE 飞地以运行全球规模应用程序的新技术。 CEE 通过形式验证扩展远程证明（如可信执行环境 (TEE)），因此信任链不仅可用于建立 enclave 二进制文件的真实性，还可用于建立可信属性。其次，它提供硬件和软件支持，以加速隔离、完整性和机密性的底层机制。这些主题包括对 CPU 和 TEE 更好隔离的支持，还包括新兴硬件加速器的快速机制。最后，研究团队探索使用基于软件定义网络的功能分解，将可证明可信的执行环境扩展到新兴的分类数据中心设计。从他们的研究中收集到的见解指导了新的算法驱动、数据结构驱动和硬件驱动解决方案的开发，以实现值得信赖的分类云设计。在规划阶段，研究人员正在开发一个原型测试台，以评估使用云规模分解 CEE 构建高性能、可信赖的全球规模移动网络的可行性。他们正在编制一份挑战清单，这些挑战将成为全面、大型提案的中心研究议程。该奖项反映了 NSF 的法定使命，并通过使用基金会的智力价值和更广泛的影响审查标准进行评估，被认为值得支持。

项目成果

Adore: atomic distributed objects with certified reconfiguration

Adore：具有经过认证的重新配置的原子分布式对象

• DOI: 10.1145/3519939.3523444
• 发表时间: 2022
• 期刊: PLDI 2022: Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation
• 作者: Honoré, Wolf;Shin, Ji-Yong;Kim, Jieung;Shao, Zhong
• 通讯作者: Shao, Zhong

Verified compilation of C programs with a nominal memory model

• DOI: 10.1145/3498686
• 发表时间: 2022-01
• 期刊: Proceedings of the ACM on Programming Languages
• 作者: Yuting Wang;Ling Zhang;Zhong Shao;Jérémie Koenig

Compositional virtual timelines: verifying dynamic-priority partitions with algorithmic temporal isolation

• DOI: 10.1145/3563290
• 发表时间: 2022-10
• 期刊: Proceedings of the ACM on Programming Languages
• 作者: Meng-qi Liu;Zhong Shao;Hao Chen;Man-Ki Yoon;Jung-Eun Kim

A Compositional Theory of Linearizability

• DOI: 10.1145/3571231
• 发表时间: 2023-01
• 期刊: Proceedings of the ACM on Programming Languages
• 作者: Arthur Oliveira Vale;Zhong Shao;Yixuan Chen

Layered and object-based game semantics

分层和基于对象的游戏语义

• DOI: 10.1145/3498703
• 发表时间: 2022
• 期刊: Proceedings of the ACM on Programming Languages
• 作者: Oliveira Vale, Arthur;Melliès, Paul-André;Shao, Zhong;Koenig, Jérémie;Stefanesco, Léo
• 通讯作者: Stefanesco, Léo