PPoSS: Planning: High-Performance Certified Trust for Global-Scale Applications
PPoSS: Planning: High-Performance Certified Trust for Global-Scale Applications
批准号:
2118851
负责人:
Zhong Shao
金额:
$25.0万
依托单位:
依托单位国家:
美国
项目类别:
Standard Grant
财政年份:
2021
资助国家:
美国
项目状态:
已结题
起止时间:
2021-10-01 至 2022-09-30
中文摘要
点击翻译按钮获取中文摘要
英文摘要
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.
期刊论文(6)
专著(0)
科研奖励(0)
会议论文
登录
查看更多内容
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
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]
通讯作者:
Meng-qi Liu;Zhong Shao;Hao Chen;Man-Ki Yoon;Jung-Eun Kim
DOI:
10.1145/3498686
发表时间:
2022-01
期刊:
Proceedings of the ACM on Programming Languages
影响因子:
--
作者:
[Yuting Wang;Ling Zhang;Zhong Shao;Jérémie Koenig]
通讯作者:
Yuting Wang;Ling Zhang;Zhong Shao;Jérémie Koenig
DOI:
10.1145/3571231
发表时间:
2023-01
期刊:
Proceedings of the ACM on Programming Languages
影响因子:
--
作者:
[Arthur Oliveira Vale;Zhong Shao;Yixuan Chen]
通讯作者:
Arthur Oliveira Vale;Zhong Shao;Yixuan Chen
SHORTSTACK: Distributed, Fault-tolerant, Oblivious Data Access
SHORTSTACK:分布式、容错、不经意的数据访问
DOI:
--
发表时间:
2022
期刊:
USENIX Symposium on Operating Systems Design and Implementation
影响因子:
--
作者:
[Vuppalapati, Midhul, Babel, Kushal, Khandelwal, Anurag, Agarwal, Rachit]
通讯作者:
Agarwal, Rachit
共 6 条
SHF: Small: Compositional Certified Concurrent Abstraction Layers
-
批准号:2313433
-
项目类别:Standard Grant
-
资助金额:$54.0万
-
财政年份:2023
-
负责人:Zhong Shao
-
依托单位:
FMitF: Track I: ADVERT: Compositional Atomic Specifications for Distributed System Verification
-
批准号:2019285
-
项目类别:Standard Grant
-
资助金额:$74.99万
-
财政年份:2020
-
负责人:Zhong Shao
-
依托单位:
SHF: Medium: DeepSEA: A Language for Programming and Synthesizing Certified Software
-
批准号:1763399
-
项目类别:Continuing Grant
-
资助金额:$80.0万
-
财政年份:2018
-
负责人:Zhong Shao
-
依托单位:
SaTC: CORE: Small: Formal End-to-End Verification of Information-Flow Security for Complex Systems
-
批准号:1715154
-
项目类别:Standard Grant
-
资助金额:$50.0万
-
财政年份:2017
-
负责人:Zhong Shao
-
依托单位:
NeTS: Small: A Virtualized Network Resource Pool for Software-Defined Network Management
-
批准号:1712674
-
项目类别:Standard Grant
-
资助金额:$35.07万
-
财政年份:2016
-
负责人:Zhong Shao
-
依托单位:
AitF: The Fuzzy Log: A Unifying Abstraction for the Theory and Practice of Distributed Systems
-
批准号:1637385
-
项目类别:Standard Grant
-
资助金额:$60.0万
-
财政年份:2016
-
负责人:Zhong Shao
-
依托单位:
Collaborative Research: Expeditions in Computing: The Science of Deep Specification
-
批准号:1521523
-
项目类别:Continuing Grant
-
资助金额:$204.64万
-
财政年份:2015
-
负责人:Zhong Shao
-
依托单位:
SHF: Small: VeriQ: Formal Quantitative Software Verification in Realistic Application Scenarios
-
批准号:1319671
-
项目类别:Standard Grant
-
资助金额:$44.97万
-
财政年份:2013
-
负责人:Zhong Shao
-
依托单位:
TC: Medium: Making OS Kernels Crash-Proof by Design and Certification
-
批准号:1065451
-
项目类别:Standard Grant
-
资助金额:$111.63万
-
财政年份:2011
-
负责人:Zhong Shao
-
依托单位:
TC:Large:Collaborative Research:Combininig Foundational and Lightweight Formal Methods to Build Certifiably Dependable Software
-
批准号:0910670
-
项目类别:Standard Grant
-
资助金额:$58.0万
-
财政年份:2009
-
负责人:Zhong Shao
-
依托单位:
TC:Small: Formal Reasoning about Concurrent Programs for Multicore and Multiprocessor Machines
-
批准号:0915888
-
项目类别:Standard Grant
-
资助金额:$50.0万
-
财政年份:2009
-
负责人:Zhong Shao
-
依托单位:
CPA-SEL-T: Domain Specific Languages, Logics, and Proofs for Certified Software Design
-
批准号:0811665
-
项目类别:Continuing Grant
-
资助金额:$85.0万
-
财政年份:2008
-
负责人:Zhong Shao
-
依托单位:
CT-ISG: Certified Runtime Code Manipulation
-
批准号:0716540
-
项目类别:Standard Grant
-
资助金额:$10.0万
-
财政年份:2007
-
负责人:Zhong Shao
-
依托单位:
CT-ISG: Modular Development of Certified Concurrent Code
-
批准号:0524545
-
项目类别:Standard Grant
-
资助金额:$40.0万
-
财政年份:2005
-
负责人:Zhong Shao
-
依托单位:
Collaborative Research: High-Assurance Common Language Runtime
-
批准号:0208618
-
项目类别:Continuing Grant
-
资助金额:$40.0万
-
财政年份:2002
-
负责人:Zhong Shao
-
依托单位:
ITR: FLINT---A Mobile-Code Infrastructure for Advanced Languages
-
批准号:0081590
-
项目类别:Continuing Grant
-
资助金额:$30.0万
-
财政年份:2000
-
负责人:Zhong Shao
-
依托单位:
Typed Common Intermediate Format
-
批准号:9901011
-
项目类别:Continuing Grant
-
资助金额:$32.0万
-
财政年份:1999
-
负责人:Zhong Shao
-
依托单位:
CAREER: Type-Directed Compilation
-
批准号:9501624
-
项目类别:Continuing Grant
-
资助金额:$10.5万
-
财政年份:1995
-
负责人:Zhong Shao
-
依托单位:
海外基金