Velisarios: Byzantine fault-tolerant protocols powered by Coq

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

doi:10.1007/978-3-319-89884-1_22

Velisarios: Byzantine fault-tolerant protocols powered by Coq

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

Computer Science

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

8 Citations (Scopus)

218 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 language	English
Title of host publication	Programming Languages and Systems
Subtitle of host publication	27th 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
Editors	Amal Ahmed
Publisher	Springer
Pages	619-650
Number of pages	32
ISBN (Electronic)	9783319898841
ISBN (Print)	9783319898834
DOIs	https://doi.org/10.1007/978-3-319-89884-1_22
Publication status	Published - 14 Apr 2018
Event	27th European Symposium on Programming, ESOP 2018 - Thessaloniki, Greece Duration: 14 Apr 2018 → 20 Apr 2018

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer
Volume	10801
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	27th European Symposium on Programming, ESOP 2018
Country/Territory	Greece
City	Thessaloniki
Period	14/04/18 → 20/04/18

Keywords

Byzantine faults
State machine replication
Formal verification
Coq

Access to Document

10.1007/978-3-319-89884-1_22Licence: Creative Commons: Attribution (CC BY)

Vincent_Rahli_et_al_Velisarios_Programming_Languages_and_Systems_2018
Checked for eligibility: 22/07/2019
Final published version, 563 KBLicence: Creative Commons: Attribution (CC BY)

https://doi.org/10.1007/978-3-319-89884-1_22Licence: Creative Commons: Attribution (CC BY)

Cite this

Rahli, V., Vukotic, I., Völp, M., & Veríssimo, P. J. E. (2018). Velisarios: Byzantine fault-tolerant protocols powered by Coq. In A. Ahmed (Ed.), Programming Languages and Systems : 27th 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 (pp. 619-650). (Lecture Notes in Computer Science; Vol. 10801). Springer. https://doi.org/10.1007/978-3-319-89884-1_22

Rahli, Vincent ; Vukotic, Ivana ; Völp, Marcus et al. / Velisarios : Byzantine fault-tolerant protocols powered by Coq. Programming Languages and Systems : 27th 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. editor / Amal Ahmed. Springer, 2018. pp. 619-650 (Lecture Notes in Computer Science).

@inproceedings{6e0bbb694393487c802eadd26184673c,

title = "Velisarios: Byzantine fault-tolerant protocols powered by Coq",

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{\textquoteright}s reference protocol: PBFT. ",

keywords = "Byzantine faults, State machine replication, Formal verification, Coq",

author = "Vincent Rahli and Ivana Vukotic and Marcus V{\"o}lp and Ver{\'i}ssimo, {Paulo Jorge Esteves}",

year = "2018",

month = apr,

day = "14",

doi = "10.1007/978-3-319-89884-1_22",

language = "English",

isbn = "9783319898834",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "619--650",

editor = "Amal Ahmed",

booktitle = "Programming Languages and Systems",

note = "27th European Symposium on Programming, ESOP 2018 ; Conference date: 14-04-2018 Through 20-04-2018",

}

Rahli, V, Vukotic, I, Völp, M & Veríssimo, PJE 2018, Velisarios: Byzantine fault-tolerant protocols powered by Coq. in A Ahmed (ed.), Programming Languages and Systems : 27th 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. Lecture Notes in Computer Science, vol. 10801, Springer, pp. 619-650, 27th European Symposium on Programming, ESOP 2018, Thessaloniki, Greece, 14/04/18. https://doi.org/10.1007/978-3-319-89884-1_22

Velisarios: Byzantine fault-tolerant protocols powered by Coq. / Rahli, Vincent; Vukotic, Ivana; Völp, Marcus et al.
Programming Languages and Systems : 27th 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. ed. / Amal Ahmed. Springer, 2018. p. 619-650 (Lecture Notes in Computer Science; Vol. 10801).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

TY - GEN

T1 - Velisarios

T2 - 27th European Symposium on Programming, ESOP 2018

AU - Rahli, Vincent

AU - Vukotic, Ivana

AU - Völp, Marcus

AU - Veríssimo, Paulo Jorge Esteves

PY - 2018/4/14

Y1 - 2018/4/14

N2 - 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.

AB - 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.

KW - Byzantine faults

KW - State machine replication

KW - Formal verification

KW - Coq

U2 - 10.1007/978-3-319-89884-1_22

DO - 10.1007/978-3-319-89884-1_22

M3 - Conference contribution

SN - 9783319898834

T3 - Lecture Notes in Computer Science

SP - 619

EP - 650

BT - Programming Languages and Systems

A2 - Ahmed, Amal

PB - Springer

Y2 - 14 April 2018 through 20 April 2018

ER -

Rahli V, Vukotic I, Völp M, Veríssimo PJE. Velisarios: Byzantine fault-tolerant protocols powered by Coq. In Ahmed A, editor, Programming Languages and Systems : 27th 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. Springer. 2018. p. 619-650. (Lecture Notes in Computer Science). doi: 10.1007/978-3-319-89884-1_22