Formal Model Guided Conformance Testing for Blockchains

TL;DR

This paper introduces a formal model-based framework for conformance testing of blockchain clients, aiming to detect protocol violations and prevent blockchain splits using deterministic simulation and trace analysis.

Contribution

It presents a novel framework combining formal models and deterministic simulation workflows for comprehensive protocol conformance testing of blockchain implementations.

Findings

Successfully applied to an industrial consensus protocol

Detected protocol violations missed by ad-hoc tests

Framework ensures high conformance and security

Abstract

Modern blockchains increasingly consist of multiple clients that implement a single blockchain protocol. If there is a semantic mismatch between the protocol implementations, the blockchain can permanently split and introduce new attack vectors. Current ad-hoc test suites for client implementations are not sufficient to ensure a high degree of protocol conformance. As an alternative, we present a framework that performs protocol conformance testing using a formal model of the protocol and an implementation running inside a deterministic blockchain simulator. Our framework consists of two complementary workflows that use the components as trace generators and checkers. Our insight is that both workflows are needed to detect all types of violations. We have applied and demonstrated the utility of our framework on an industrial strength consensus protocol.