CAREER: Verifying Distributed System Implementations

每天都有数十亿人依靠分布式系统来进行医疗、银行、交通等业务。尽管付出了昂贵的测试努力，但这些复杂的服务在实践中仍然失败，导致数据丢失和主要服务中断，威胁到每个人的便利、财务和安全。该项目正在开发必要的工具和技术来验证（数学证明）分布式系统实现在任何网络和机器错误行为组合下的安全性和可靠性。智力上的优点是开发组合验证技术，程序员可以独立地证明应用程序的正确性和容错组件的可靠性。更广泛的意义和重要性是为社会所依赖的核心计算基础设施提供严格的可靠性保证，并培养新一代工程师，他们将创建高性能、经过验证的分布式系统实现。该项目旨在通过开发验证系统变压器使验证变得容易，该变压器可以自动将简单系统包裹在保证保持等效的容错机制中。这种方法将应用程序正确性的关注点从容错中分离出来，从而简化了证明工作并实现了更好的代码重用。工业实践者已经在使用早期原型验证的系统变压器作为探索设计和替代实现的指南。这个项目的一个成果是一个广泛的此类变压器库，涵盖了广泛的关键分布式系统特性，包括重新配置、环维护和软件更新。该奖项反映了美国国家科学基金会的法定使命，并通过使用基金会的知识价值和更广泛的影响审查标准进行评估，被认为值得支持。

Billions of people depend on distributed systems every day for health care, banking, transportation, and more. Despite costly testing efforts, these complex services still fail in practice, leading to data loss and major service outages that threaten everyone's convenience, finances, and safety. This project is developing the tools and techniques necessary to verify (mathematically prove) safety and reliability for distributed systems implementations under any combination of network and machine misbehaviors. The intellectual merits are to develop compositional verification techniques where the programmer can independently prove correctness for applications and reliability for fault-tolerance components. The broader significance and importance are to provide rigorous reliability guarantees for the core computational infrastructure society depends on and to train a new generation of engineers who will create high-performance, verified distributed systems implementations.This project aims to make verification tractable by developing verified system transformers which automatically wrap simple systems with fault tolerance mechanisms guaranteed to preserve equivalence. This approach separates concerns of application correctness from fault tolerance which eases proof effort and enables greater code reuse. Industrial practitioners are already using an early prototype verified system transformer as a guide in exploring designs and alternate implementations. An outcome of this project is an extensive library of such transformers covering a broad range of critical distributed system features including reconfiguration, ring maintenance, and software update.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.