Reference : Velisarios: Byzantine Fault-Tolerant Protocols Powered by Coq
Scientific congresses, symposiums and conference proceedings : Paper published in a book
Engineering, computing & technology : Computer science
Security, Reliability and Trust
http://hdl.handle.net/10993/35304
Velisarios: Byzantine Fault-Tolerant Protocols Powered by Coq
English
Rahli, Vincent mailto [University of Luxembourg > Interdisciplinary Centre for Security, Reliability and Trust (SNT) > >]
Vukotic, Ivana mailto [University of Luxembourg > Interdisciplinary Centre for Security, Reliability and Trust (SNT) > >]
Volp, Marcus mailto [University of Luxembourg > Interdisciplinary Centre for Security, Reliability and Trust (SNT) > >]
Verissimo, Paulo mailto [University of Luxembourg > Interdisciplinary Centre for Security, Reliability and Trust (SNT) > >]
Apr-2018
Velisarios: Byzantine Fault-Tolerant Protocols Powered by Coq
Yes
International
27th European Symposium on Programming (ESOP)
from 14-04-2018 to 20-04-2018
[en] Byzantine faults ; state machine replication ; formal verification ; Coq
[en] 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.
http://hdl.handle.net/10993/35304
FnR ; FNR8149128 > Paulo Esteves Verissimo > IISD > Strategic RTnD Program on Information Infrastructure Security and Dependability > 01/01/2015 > 31/12/2019 > 2015

File(s) associated to this reference

Fulltext file(s):

FileCommentaryVersionSizeAccess
Open access
Velisarios.pdfAuthor preprint749.13 kBView/Open

Bookmark and Share SFX Query

All documents in ORBilu are protected by a user license.