Program Logics for Compositional Specification and Verification of Distributed Systems

It is hard to overstate the significance and ubiquity of distributed services in many aspects of the modern life, such as health care, online commerce, transportation, entertainment and cloud-based applications. Given the importance of distributed software and its complexity, stemming from its concurrent nature and the necessity to tolerate reordering and loss of packets, it is nowadays considered vital in industry to have a rigorous verification methodology for establishing its correctness properties, ensuring that, once a distributed system is up and running, it will never go wrong and will eventually complete its goals.

Real-world applications, including distributed ones, are not developed as standalone, monolithic pieces of code: they are rather built from multiple components, by composing the program machinery implemented in different modules, developed independently and then linked together. The benefit of such a compositional approach is thus the separation of concerns, which makes the development process modular: in order to use an implementation of a distributed protocol as a library, one should know what it does without bothering to understand how it works.

Alas, the potential of what is considered to be a good practice in modular software development, is not yet fully realised in the area of formal reasoning about distributed software. The existing approaches for specification and verification of distributed applications are predominantly focused on reasoning about systems as of standalone protocols, whose behavior is described using invariants of their execution histories, which are then checked using the protocols' abstract models. The absence of a uniform way of specifying and verifying implementations of distributed protocols and their clients (which might be themselves protocol implementations) introduces a gap in vertical compositionality of the formal reasoning: in order to prove correctness of a distributed library's client program, one should rely on the correctness result, established with respect to the library's model rather than its actual implementation. Furthermore, the way a distributed protocol is specified might employ a particular correctness condition, fixing its history invariants, such as linearizability, eventual or causal consistency, forcing one to adopt the corresponding verification methodology for the sake of reasoning about the protocol's clients. This diversity poses challenges with respect to horizontal compositionality, making it non-trivial to reason about non-toy applications that combine several protocols.

This project proposes to develop a uniform and modular approach for formally specifying and verifying implementations of distributed applications, in a machine-checked framework, addressing both issues of vertical and horizontal compositionality. The suggested methodology builds on the ideas of Hoare-style program logics for effectful concurrent programs and their mechanisation using dependent types. The proposed approach will thus establish a connecting link between the good practices of modular software development in the area of distributed computing and ideas of compositional reasoning about programs, as a way to formally verify them, therefore, delivering the strongest guarantees of their correctness.

The first set of general contributions of this research is in the development of sound logical foundations for compositional reasoning about distributed computations. A foundational approach to logic-based program verification has been historically established in the UK by the works of Hoare in '60s and more recently continued by a series of works by O'Hearn and his collaborators, resulting in the practical adoption and industrial acclaim of Infer, a static analysis tool, based on Separation Logic, which is now being actively used at Facebook. The work proposed here directly builds on those ideas, taking them to the new area of computing, and contributes to the Information and Communication Technologies (ICT) portfolio of EPSRC, within the area of Verification and Correctness.

The second set of contributions would come from enhancing the design of modern programming languages and frameworks for distributed computations, incorporating the ideas of protocols and dependent types to specify and compose their properties. This aspect fits into the ICT portfolio within the area of Programming Languages and Compilers. Furthermore, with the recent shift in the industry towards the multicore architectures attempting to leverage massive parallelism for efficient computations, one should be able to formally ensure the correctness of the corresponding system implementations. Therefore, this proposal will be of importance for the cross-cutting ICT priority concerned with Many-core architectures and concurrency in distributed and embedded systems.

Finally, in the longer term the proposed work contributes to applications in the EPSRC's Global uncertainties theme, providing a theoretical basis for creating robust distributed systems, resilient to cybersecurity threats in a world of communicating entities.