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

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

• 批准号: 2318954
• 负责人: Manos Kapritsos
• 金额: $ 37.5万
• 依托单位: Regents of the University of Michigan - Ann Arbor
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2023
• 资助国家: 美国
• 起止时间: 2023-10-01 至 2027-09-30
• 项目状态: 未结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=2318954&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.

该项目旨在简化和自动化高性能分布式系统的验证，即在多台计算机上运行的系统，以提高可靠性和/或性能。这些系统对我们的社会至关重要，因为它们既复杂又微妙。这使得它们成为正式验证的主要目标，正式验证是一种可以消除分布式系统中许多类错误的技术。然而，现有的验证方法是不切实际的：它们需要大量不合理的人力和直觉，或者依赖于对他们正在验证的系统的不切实际的假设。这个项目将做出许多贡献，使形式化验证更接近实用性，针对现实世界的高性能实现，包括那些依赖于多线程的实现。该项目将开发消息不变量，这是一种将分布式系统当作集中式系统进行推理的新方法，从而简化了所需的人力和直觉。它还将探讨所有权类型：分布式系统通常涉及所有权或唯一性的概念；例如，当传递锁或将密钥从一个系统移动到另一个系统时。目前，这样的推理是由开发人员手工完成的，而且非常辛苦。建议的工作将使分布式所有权类型形式化，使类型检查器能够快速自动地履行许多此类义务，从而简化开发人员的推理。这个项目的最终目标是使分布式系统的正式验证成为当前测试的一种实际替代方法，这种方法在保护当今的大规模系统免受软件错误的侵害时具有根本的局限性。通过对真实世界的高性能分布式系统的自动化验证——不受现有自动化方法的限制——该项目旨在确保正式验证不再是学术界的好奇心，而是将被实践者积极采用。从今天的最大努力测试技术到正式验证软件的转变将导致一个未来，在这个未来，社会所依赖的软件产品将是真正可靠和健壮的，由机器检查的正确性数学证明支持。这项研究计划将由综合教育和推广活动来补充，包括每年的暑期学校和旨在扩大计算机参与的活动。该奖项反映了美国国家科学基金会的法定使命，并通过使用基金会的知识价值和更广泛的影响审查标准进行评估，被认为值得支持。