Reference : Velisarios: Byzantine Fault-Tolerant Protocols Powered by Coq

	Document type :	Scientific congresses, symposiums and conference proceedings : Paper published in a book
	Discipline(s) :	Engineering, computing & technology : Computer science
	Focus Areas :	Security, Reliability and Trust
	To cite this reference:	http://hdl.handle.net/10993/35304

Title :	Velisarios: Byzantine Fault-Tolerant Protocols Powered by Coq
Language :	English
Author, co-author :	Rahli, Vincent [University of Luxembourg > Interdisciplinary Centre for Security, Reliability and Trust (SNT) > >]
	Vukotic, Ivana [University of Luxembourg > Interdisciplinary Centre for Security, Reliability and Trust (SNT) > >]
	Volp, Marcus [University of Luxembourg > Interdisciplinary Centre for Security, Reliability and Trust (SNT) > >]
	Verissimo, Paulo [University of Luxembourg > Interdisciplinary Centre for Security, Reliability and Trust (SNT) > >]
Publication date :	Apr-2018
Main document title :	ESOP 2018
Peer reviewed :	Yes
Audience :	International
Event name :	27th European Symposium on Programming (ESOP)
Event date :	from 14-04-2018 to 20-04-2018
Keywords :	[en] Byzantine faults ; state machine replication ; formal verification ; Coq
Abstract :	[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.
Permalink :	http://hdl.handle.net/10993/35304
FnR project :	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): File Commentary Version Size Access Open access Velisarios.pdf Author preprint 750.08 kB View/Open

All documents in ORBi^lu are protected by a user license.

 

University of Luxembourg Library |  Feedback |  Legal notices Site Map