Collaborative Research: FMitF: Track I: Simplifying End-to-End Verification of High-Performance Distributed Systems

合作研究：FMitF：第一轨：简化高性能分布式系统的端到端验证

• 批准号: 2318953
• 负责人: Bryan Parno
• 金额: $ 37.5万
• 依托单位: Carnegie-Mellon University
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2023
• 资助国家: 美国
• 起止时间: 2023-10-01 至 2027-09-30
• 项目状态: 未结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=2318953&HistoricalAwards=false
• 关键词: Collaborative; Research; FMitF; Track; Simplifying

This project aims to simplify and automate the verification of high-performance distributed systems, i.e., systems that run on multiple computers to improve reliability and/or performance. Such systems are as crucial for our society as they are complex and subtle. This makes them a prime target for formal verification, a technique that can eliminate many classes of bugs from distributed systems. Existing verification approaches, however, are impractical: They require an unreasonable amount of human effort and intuition or rely on unrealistic assumptions about the systems they are verifying. This project will make a number of contributions to bring formal verification closer to practicality, targeting real-world, high-performance implementations, including those that rely on multi-threading. This project will develop Message Invariants, a new way to reason about a distributed system as if it were a centralized system, thus simplifying the human effort and intuition required. It will also explore Ownership Types: Distributed systems often involve concepts of ownership or uniqueness; e.g., when passing a lock around, or when moving keys from one system to another. Currently, such reasoning is done manually—and painstakingly—by the developer. The proposed work will formalize distributed Ownership Types to enable a type checker to quickly and automatically discharge many such obligations, thus simplifying the reasoning for developers. The ultimate aim of this project is to make formal verification of distributed systems a practical alternative to the current, best-effort approach of testing, an approach that has fundamental limitations when safeguarding today's large-scale systems from software errors. By automating the verification of real-world, high-performance distributed systems—unfettered by the limitations that come with existing automated approaches—this project aims to ensure that formal verification will not remain an academic curiosity, but will instead be actively adopted by practitioners. A shift from today's best-effort testing techniques to formally verified software will lead to a future where the software products that society depends on will be truly reliable and robust, backed by machine-checked mathematical proofs of correctness. The research program will be complemented by integrated education and outreach initiatives, including an annual summer school and activities focused on broadening participation in computing.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.

该项目旨在简化和自动化高性能分布式系统的验证，即在多台计算机上运行以提高可靠性和/或性能的系统。这样的系统对我们的社会至关重要，就像它们复杂而微妙。这使它们成为正式验证的主要目标，该技术可以消除分布式系统中的许多类别的错误。但是，现有的验证方法是不切实际的：它们需要不合理的人类努力和直觉，或者依靠对他们正在验证的系统的不现实假设。该项目将做出许多贡献，以使正式验证更接近实用性，以现实世界中的高性能实现为目标，包括依靠多线程的实现。该项目将开发消息不变性，这是一种推理分布式系统的新方法，就好像它是一个集中式系统一样，从而简化了所需的人类努力和直觉。还探索所有权类型：分布式系统通常涉及所有权或独特性的概念；例如，将锁定或将密钥从一个系统移动到另一个系统时。当前，这种推理是通过开发人员手动（艰苦的）手动进行的。拟议的工作将形式化分布式所有权类型，以使类型的检查器能够快速并自动履行许多此类义务，从而简化开发人员的推理。该项目的最终目的是使分布式系统的正式验证成为当前最佳测试方法的实用替代方法，这种方法在保护当今的大规模系统免于软件错误时具有基本限制。通过对现实世界的验证进行自动化，高性能分布式系统（因现有自动化方法所带来的局限性而没有），该项目旨在确保正式验证将不再是学术上的好奇心，而是将被从业者积极地采用。从当今最佳效劳测试技术转变为正式验证的软件将带来一个未来，社会依赖的软件产品将是真正可靠且可靠的，并得到了机器检查的正确性证据的支持。该研究计划将通过综合教育和外展计划完成，包括年度暑期学校和旨在扩大计算参与的活动。该奖项反映了NSF的法定任务，并通过使用该基金会的知识分子的优点和更广泛的影响来评估NSF的法定任务。