Velisarios: Byzantine fault-tolerant protocols powered by Coq

Vincent Rahli, Ivana Vukotic, Marcus Völp, Paulo Jorge Esteves Veríssimo

Research output: Chapter in Book/Report/Conference proceedingConference contribution

8 Citations (Scopus)
152 Downloads (Pure)

Abstract

Our increasing dependence on complex and critical information infrastructures and the emerging threat of sophisticated attacks, ask for extended efforts to ensure the correctness and security of these systems. Byzantine fault-tolerant state-machine replication (BFT-SMR) provides a way to harden such systems. It ensures that they maintain correctness and availability in an application-agnostic way, provided that the replication protocol is correct and at least n−f  n−f out of n replicas survive arbitrary faults. This paper presents Velisarios, a logic-of-events based framework implemented in Coq, which we developed to implement and reason about BFT-SMR protocols. As a case study, we present the first machine-checked proof of a crucial safety property of an implementation of the area’s reference protocol: PBFT. 

Original languageEnglish
Title of host publicationProgramming Languages and Systems
Subtitle of host publication27th European Symposium on Programming, ESOP 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Thessaloniki, Greece, April 14-20, 2018, Proceedings
EditorsAmal Ahmed
PublisherSpringer
Pages619-650
Number of pages32
ISBN (Electronic)9783319898841
ISBN (Print)9783319898834
DOIs
Publication statusPublished - 14 Apr 2018
Event27th European Symposium on Programming, ESOP 2018 - Thessaloniki, Greece
Duration: 14 Apr 201820 Apr 2018

Publication series

NameLecture Notes in Computer Science
PublisherSpringer
Volume10801
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference27th European Symposium on Programming, ESOP 2018
Country/TerritoryGreece
CityThessaloniki
Period14/04/1820/04/18

Keywords

  • Byzantine faults
  • State machine replication
  • Formal verification
  • Coq

Cite this