CAREER: Specifying and Verifying Correctness of Software Updates

Software updates are a fact of life, yet they are difficult for developers to get right because the new version must correctly interact with the previous version. Incorrect updates remain a surprisingly common source of catastrophic failures in practice. Formal verification, a technique where software is mathematically proven to behave as intended, is a promising approach to make software more reliable; however, with existing verification approaches, we don't know how to state (much less prove) compatibility. This project's novelties are to develop a definition of software update correctness and create the proof techniques to show that updates are correct before deploying them. The project's impacts are new verification tools that can be used to prove an update is compatible, and ultimately an understanding of update correctness that leads to more reliable systems. Verifying updates is especially important with increased use of AI-based coding agents, which will produce more reliable changes if they have feedback on whether an update is compatible with the already deployed code or not. Update correctness is also important for updates to machine learning (ML) infrastructure itself, which is also rapidly changing. We identify three fundamental update issues to focus on in this project: data-format compatibility, specifying the effect of data migration on a system's behavior, and verifying distributed-system rolling upgrades. The approach we take is to develop specifications for what a compatible update is in each of these cases: the specification is a desired property of the new code that considers any data that might be produced by the old code. Next, we develop a proof technique for proving these new specifications in Perennial, a program logic for the Go programming language that uses machine-checked proofs. Finally, we will apply the techniques to several examples of updates that are representative of real-world changes. The goal is to lay the formal foundations for an important aspect of software correctness. 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.