CAREER: Building Reliable Distributed Systems with Refinement Types

University Of California-Santa Cruz, Santa Cruz CA

Investigators

Abstract

This award is funded in whole or in part under the American Rescue Plan Act of 2021 (Public Law 117-2). Today's most important computer systems are distributed systems: those that consist of multiple machines that communicate by sending messages over a network, and where individual machines or network connections may fail independently. Programming such systems is notoriously difficult and error-prone due to messages being reordered or delayed and the possibility of machines and network connections failing. Widely-used protocols are meant to ensure, for instance, a given message delivery order or a given data consistency policy, but machine-checked proofs ensuring the correctness of executable implementations of these protocols are rare. The goal of this project is to mechanically verify real, executable implementations of distributed systems, using powerful tools built into a general-purpose programming language. The project's novelties are in its focus on immediately executable implementations, and in its modular verification approach that separates lower-level message delivery concerns from higher-level application semantics. The project's impacts will be in improving the overall trustworthiness and reliability of distributed software systems. The project further aims to create approachable entry points to research, and to develop students' scientific communication skills, by integrating the creation of zines and videos about distributed systems verification into the investigator and project team's teaching and research practices, and making the resulting materials freely available online. The project's approach to language-level distributed systems verification centers around refinement types: data types that let programmers specify logical predicates that restrict the set of values described by a type, and that can be checked at compile time by an SMT solver. The project uses Liquid Haskell, which extends the Haskell programming language with support for refinement types, and which can further be used for extrinsic verification, that is, defining functions to state and prove theorems. The investigator and team will use Liquid Haskell to develop mechanically verified, modular libraries for implementing distributed systems. A novel verified message delivery library will form the foundation for additional verified components, such as libraries providing replicated data types and distributed data stores. Furthermore, the project investigates combining the strengths of Liquid Haskell with those of interactive proof assistants such as Agda. These investigations culminate in a comprehensive survey of such hybrid automated/interactive verification tools, and provide a holistic scientific understanding of the design space. 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.