Igloo: End-to-End Verification of Distributed Systems

Former Members

• Wytse Oortwijn (TNO-ESI)
  
• Fábio Pakk Selmi-​Dei
• Martin Clochard

Introduction

We have recently proposed a novel methodology for the end-to-end verification of distributed systems. It combines the compositional refinement of abstract, event-based models of distributed systems with the verification of full-fledged program code using expressive separation logics, which support features of realistic programming languages like mutable heap data structures and concurrency.

Our method consists of the following six steps (see Figure):

1. Abstract model. We start a development with an initial abstract event-based model of the entire system for which we prove the desired trace properties.
2. Protocol model. We refine the abstract model into a protocol model, which contains the components of the distributed system to be developed and the environment in which it is supposed to run. This may include a fault model or attacker model.
3. Interface model. We prepare the model for a subsequent decomposition in to system components and the environment. This involves a refinement to match the interface between the components and the environment with the I/O libraries to be used in the implementation.
4. Decomposition. We decompose the monolithic interface model into separate models for each type of system component (e.g., clients and servers) and the environment.
5. Translation. The models of the system components are translated into \emph{I/O specifications} expressed in separation logic, which will serve as specifications of the component implementations.
6. Program verification. We implement the components and use a program verifier to prove that each component's code adheres to its I/O specification.

We proved that our formal framework soundly relates event-based system models to program specifications in a separation logic, such that successful verification establishes a refinement relation between the model and the code. As a result, the properties proven on the abstract and protocol models are preserved down to the real system. We formalized our framework, called Igloo, in Isabelle/HOL. Our approach allows us to leverage existing program verification tools (currently VeriFast for Java and Nagini for Python).

We have evaluated our framework on three case studies

1. a leader election protocol,
2. a primary-backup replication protocol, and
3. an authentication protocol.
   

For these we refined formal requirements into I/O specifications, which are then used to verify different implementations, written in Java and Python, in the existing VeriFast and Nagini code verifiers.

Objectives

Provide a formal development method spanning models and implementation where system-wide global correctness guarantees are preserved down to the implementation.

Publications

• Linard Arquint, Felix A. Wolf, Joseph Lallemand, Ralf Sasse, Christoph Sprenger, Sven N. Wiesener, David Basin, and Peter Müller. Sound Verification of Security Protocols: From Design to Interoperable Implementations. In IEEE Symposium on Security and Privacy, SP 2023, 2023
  [external page DOI | external page preprint]
• Christoph Sprenger, Tobias Klenze, Marco Eilers, Felix A. Wolf, Peter Müller, Martin Clochard, and David Basin. Igloo: Soundly Linking Compositional Refinement and Separation Logic for Distributed System Verification. OOPSLA 2020.
  [external page DOI | Download pdf (PDF, 461 KB) | external page preprint]