Automating and Mechanizing Cutoff-based Verification of Distributed Protocols

TL;DR

This paper introduces a novel cutoff-based verification method for distributed protocols that reduces infinite state verification to finite state checks, avoiding the difficult task of finding inductive invariants.

Contribution

It formalizes a general cutoff approach within a protocol modeling language and provides an automatic synthesis algorithm, enabling verification of complex distributed protocols.

Findings

Successfully applied to complex protocols, establishing new cutoff results.

Reduces verification complexity by avoiding invariant discovery.

Demonstrates effectiveness with SMT encoding and static analysis.

Abstract

Distributed protocols are generally parametric and can be executed on a system with any number of nodes, and hence proving their correctness becomes an infinite state verification problem. The most popular approach for verifying distributed protocols is to find an inductive invariant which is strong enough to prove the required safety property. However, finding inductive invariants is known to be notoriously hard, and is especially harder in the context of distributed protocols which are quite complex due to their asynchronous nature. In this work, we investigate an orthogonal cut-off based approach to verifying distributed protocols which sidesteps the problem of finding an inductive invariant, and instead reduces checking correctness to a finite state verification problem. The main idea is to find a finite, fixed protocol instance called the cutoff instance, such that if the cutoff instance is safe, then any protocol instance would also be safe. Previous cutoff based approaches have only been applied to a restricted class of protocols and specifications. We formalize the cutoff approach in the context of a general protocol modeling language (RML), and identify sufficient conditions which can be efficiently encoded in SMT to check whether a given protocol instance is a cutoff instance. Further, we propose a simple static analysis-based algorithm to automatically synthesize a cut-off instance. We have applied our approach successfully on a number of complex distributed protocols, providing the first known cut-off results for many of them.