A Formalization of the Correctness of the Floodsub Protocol

TL;DR

This paper formally verifies the correctness of the Floodsub peer-to-peer pubsub protocol by mechanizing a proof that it refines a simplified specification called Broadcastsub, using Well-Founded Simulation.

Contribution

It provides the first mechanized, refinement-based correctness proof of a real-world pubsub protocol, Floodsub, using formal methods.

Findings

Floodsub correctly implements Broadcastsub

First mechanized proof of a real-world pubsub protocol

Uses Well-Founded Simulation for verification

Abstract

Floodsub is a simple, robust and popular peer-to-peer publish/subscribe (pubsub) protocol, where nodes can arbitrarily leave or join the network, subscribe to or unsubscribe from topics and forward newly received messages to all of their neighbors, except the sender or the originating peer. To show the correctness of Floodsub, we propose its specification: Broadcastsub, in which implementation details like network connections and neighbor subscriptions are elided. To show that Floodsub does really implement Broadcastsub, one would have to show that the two systems have related infinite computations. We prove this by reasoning locally about states and their successors using Well-Founded Simulation (WFS). In this paper, we focus on the mechanization of a proof which shows that Floodsub is a simulation refinement of Broadcastsub using WFS. To the best of our knowledge, ours is the first mechanized refinement-based verification of a real world pubsub protocol.