A Formally Verified Protocol for Log Replication with Byzantine Fault Tolerance
OPEN ACCESS
Loading...
Author / Producer
Date
2020
Publication Type
Conference Paper
ETH Bibliography
yes
Citations
Altmetric
OPEN ACCESS
Data
Rights / License
Abstract
Byzantine fault tolerant protocols enable state replication in the presence of crashed, malfunctioning, or actively malicious processes. Designing such protocols without the assistance of verification tools, however, is remarkably error-prone. In an adversarial environment, performance and flexibility come at the cost of complexity, making the verification of existing protocols extremely difficult. We take a different approach and propose a formally verified consensus protocol designed for a specific use case: secure logging. Our protocol allows each node to propose entries in a parallel subroutine, and guarantees that correct nodes agree on the set of all proposed entries, without leader election. It is simple yet practical, as it can accommodate the workload of a logging system such as Certificate Transparency. We show that it is optimal in terms of both required rounds and tolerable faults. Using Isabelle/HOL, we provide a fully machine-checked security proof based upon the Heard-Of model, which we extend to support signatures. We also present and evaluate a prototype implementation.
Permanent link
Publication status
published
External links
Editor
Book title
2020 International Symposium on Reliable Distributed Systems (SRDS)
Journal / series
Volume
Pages / Article No.
101 - 112
Publisher
IEEE
Event
39th International Symposium on Reliable Distributed Systems (SRDS 2020) (virtual)
Edition / version
Methods
Software
Geographic location
Date collected
Date created
Subject
Byzantine fault tolerant; Consensus algorithms; Formal verification
Organisational unit
03975 - Perrig, Adrian / Perrig, Adrian
Notes
Due to the Coronavirus (COVID-19) the conference was conducted virtually.