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

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.