Igloo: Soundly Linking Compositional Refinement and Separation Logic for Distributed System Verification

TL;DR

Igloo introduces a formal framework that combines compositional refinement of distributed system models with expressive separation logic verification of actual code, enabling sound, full-system verification.

Contribution

It presents a novel methodology and formal framework that relate event-based models to program code in separation logic, facilitating comprehensive distributed system verification.

Findings

Successfully verified leader election, replication, and security protocols.

Refined formal requirements into executable code in Java and Python.

Integrated protocol development tools with existing program verifiers.

Abstract

Lighthouse projects such as CompCert, seL4, IronFleet, and DeepSpec have demonstrated that full verification of entire systems is feasible by establishing a refinement relation between an abstract system specification and an executable implementation. Existing approaches however impose severe restrictions on either the abstract system specifications due to their limited expressiveness or versatility, or on the executable code due to their reliance on suboptimal code extraction or inexpressive program logics. We propose a novel methodology that 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. The main technical contribution of our work is a formal framework that soundly relates event-based system models to program specifications in separation logics, such that successful verification establishes a refinement relation between the model and the code. We formalized our framework, Igloo, in Isabelle/HOL. Our framework enables the sound combination of tools for protocol development with existing program verifiers. We report on three case studies, a leader election protocol, a replication protocol, and a security protocol, for which we refine formal requirements into program specifications (in Isabelle/HOL) that we implement in Java and Python and prove correct using the VeriFast and Nagini tools.