Formal Model Guided Conformance Testing for Blockchains
Filip Drobnjakovic, Amir Kashapov, Matija Kupresanin, Bernhard Scholz, Pavle Subotic
TL;DR
The paper tackles the problem of ensuring protocol conformance across multiple blockchain clients to prevent network splits and security vulnerabilities. It introduces the Formal Model Deterministic Simulation Environment (FMDSE), a bi-directional, model-guided conformance testing framework that combines a formal specification (via a language like TLA+) with a deterministic blockchain simulator to generate and verify traces in two complementary workflows. The approach is demonstrated on an industrial-strength DAG-based asynchronous consensus protocol (Sonic), revealing Type-I, Type-II, and property violations and showing the framework’s capability to scale with fuzzing while maintaining reproducibility. This framework enhances robustness for multi-client blockchains and offers a generalizable method for conformance testing in distributed systems where network-wide properties are critical.
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.