Compositional Higher-Order Reasoning about Distributed Systems

Introduction

Software systems are critical for the infrastructure of modern society, and software errors and security breaches pose enormous costs and risks. The traditional method of testing software systems is famously inadequate for guaranteeing the absence of errors and security breaches since not all execution paths are covered by testing. This is especially true for concurrent and distributed systems, where there are simply too many execution paths to test. This inadequacy has motivated research in formal methods for program verification that can offer mathematical proofs that all system behaviors meet some desirable property.

Importance of Abstraction Levels

To formally analyze and reason about software systems, it is important to consider models at many different levels of abstraction. Since many real software errors and security breaches stem from subtle problems in implementations of software systems, we focus on detailed, so-called semantic models of program execution.

Challenges in Compositional Verification

While there has been much research on abstract models for reasoning about distributed systems, there has been very little work on compositional verification of implementations of distributed systems. Compositional verification enables:

1. Specification of individual software modules
2. Verification of individual software modules
3. Verification of their composition

This approach is key to achieving scalable methods that apply to large programs, but the development of logics and methods for compositional reasoning is hard.

Progress in Concurrent Programs

For concurrent, non-distributed programs, there has been tremendous progress in the last decade on program logics for compositional verification, particularly through the development of so-called higher-order concurrent separation logics.

Goals of CHORDS

Leveraging this progress, CHORDS will research and develop new theories, program logics, and methods for mathematically rigorous compositional reasoning about implementations of distributed systems. This initiative aims to lay the foundation for tools that will help programmers create more correct and secure distributed systems.