Velisarios: Byzantine fault-tolerant protocols powered by Coq

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

Authors

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

Colleges, School and Institutes

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. 

Details

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
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
CountryGreece
CityThessaloniki
Period14/04/1820/04/18

Keywords

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