Velisarios: Byzantine fault-tolerant protocols powered by coq

Vincent Rahli; Ivana Vukotic; Marcus Völp; Paulo Esteves-Verissimo

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 Esteves-Verissimo

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

23 Scopus citations

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 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 (US)
Title of host publication	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Publisher	Springer [email protected]
Pages	619-650
Number of pages	32
ISBN (Print)	9783319898834
DOIs	https://doi.org/10.1007/978-3-319-89884-1_22
State	Published - Jan 1 2018
Externally published	Yes

Access to Document

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

Cite this

@inproceedings{418966f8145649428c12afa7676ca181,

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 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.",

author = "Vincent Rahli and Ivana Vukotic and Marcus V{\"o}lp and Paulo Esteves-Verissimo",

note = "Generated from Scopus record by KAUST IRTS on 2021-03-16",

year = "2018",

month = jan,

day = "1",

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

language = "English (US)",

isbn = "9783319898834",

pages = "619--650",

booktitle = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer [email protected]",

}

Velisarios: Byzantine fault-tolerant protocols powered by coq. / Rahli, Vincent; Vukotic, Ivana; Völp, Marcus et al.
Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). Springer [email protected], 2018. p. 619-650.

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

TY - GEN

T1 - Velisarios: Byzantine fault-tolerant protocols powered by coq

AU - Rahli, Vincent

AU - Vukotic, Ivana

AU - Völp, Marcus

AU - Esteves-Verissimo, Paulo

N1 - Generated from Scopus record by KAUST IRTS on 2021-03-16

PY - 2018/1/1

Y1 - 2018/1/1

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

UR - http://link.springer.com/10.1007/978-3-319-89884-1_22

UR - http://www.scopus.com/inward/record.url?scp=85045650272&partnerID=8YFLogxK

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

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

M3 - Conference contribution

SN - 9783319898834

SP - 619

EP - 650

BT - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

PB - Springer [email protected]

ER -

Velisarios: Byzantine fault-tolerant protocols powered by coq

Abstract

Access to Document

Other files and links

Fingerprint

Cite this