SHF: Medium: Configuration for Assurance: Safe, Live, and Secure Distributed Systems

以低成本开发高保证、高性能的分布式应用程序的能力将是搜索引擎、社交网络、云和移动计算应用程序成功和增长的关键。编程计算机应用程序的语言和系统一直是计算机科学的核心，分布式应用程序的开发也不例外。然而，分布式系统的正确性验证、性能优化和复杂算法的可靠执行仍然具有挑战性。该项目开发了一个集成的框架和支持方法和工具，使得(1)实用分布式算法的规范、测试、模拟和评估，以及(2)分布式算法的安全、实时和安全执行的系统编译、优化和验证。本研究扩展了分布式算法编程的高级语言DistAlgo，为动态分布式系统环境和需求提供了系统的声明。该项目通过将开发的方法和工具应用于最重要的实用分布式算法来评估它们，包括一致性、拜占庭一致性和具有随机故障和定时场景的区块链一致性，以及分布式存储。作为该项目的一部分，研究人员开发了一门新的新生通用主题课程，内容是关于解决问题的逻辑思维，特别是包括多方逻辑思维，基于十年来并行和分布式算法的成功教学和结晶，以及丰富的计算机科学教学经验。该奖项反映了NSF的法定使命，并通过使用基金会的智力优势和更广泛的影响审查标准进行评估，被认为值得支持。

The ability to develop high-assurance high-performance distributed applications at low cost will be key to the success and growth of search engines, social networks, cloud and mobile computing applications. Languages and systems for programming computer applications have always been at the core of computer science, and the development of distributed applications is no exception. Yet, correctness validation, performance optimization, and assured execution of complex algorithms for distributed systems remain challenging. This project develops an integrated framework and supporting methods and tools that enable (1) specification, testing, simulation, and evaluation of practical distributed algorithms, and (2) systematic compilation, optimization, and verification for safe, live, and secure execution of distributed algorithms.This research extends DistAlgo, a very high-level language for programming distributed algorithms, with systematic declarations for dynamic distributed system environments and requirements. The project evaluates the developed methods and tools by applying them to the most important practical distributed algorithms, including for consensus, Byzantine consensus, and blockchain consensus with stochastic failure and timing scenarios, and for distributed storage. As part of this project, the investigators develop a new freshman general topics course on logical thinking for problem solving, especially including multi-party logical thinking, building on a decade of successful teaching and crystallization of concurrent and distributed algorithms, and on broad experience teaching computer science.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.