Formalizing Correct-by-Construction Casper in Coq

Elaine Li, Traian Serbanuta, Denisa Diaconescu, Vlad Zamfir, Grigore Rosu

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

Abstract

Correct-by-Construction Casper (CBC Casper) is an Ethereum candidate consensus protocol undergoing active design and development. We present a formalization of CBC Casper using the Coq proof assistant that includes a model of the consensus protocol and proofs of safety and non-triviality protocol properties. We leverage Coq's type classes to model CBC Casper at various levels of abstraction. In doing so, we 1) illuminate the assumptions that each protocol property depends on, and 2) reformulate the protocol in general, mathematical terms. We highlight two advantages of our approach: 1) from a proof engineering perspective, it enables a clean separation of concerns between theory and implementation; 2) from a protocol engineering perspective, it provides a rigorous, foundational understanding of the protocol conducive to finding and proving stronger properties. We detail one such new property: strong non-triviality.

Original languageEnglish (US)
Title of host publicationIEEE International Conference on Blockchain and Cryptocurrency, ICBC 2020
PublisherInstitute of Electrical and Electronics Engineers Inc.
ISBN (Electronic)9781728166803
DOIs
StatePublished - May 2020
Event2nd IEEE International Conference on Blockchain and Cryptocurrency, ICBC 2020 - Virtual, Online, Canada
Duration: May 2 2020May 6 2020

Publication series

NameIEEE International Conference on Blockchain and Cryptocurrency, ICBC 2020

Conference

Conference2nd IEEE International Conference on Blockchain and Cryptocurrency, ICBC 2020
CountryCanada
CityVirtual, Online
Period5/2/205/6/20

Keywords

  • blockchain
  • consensus protocols
  • Coq
  • Ethereum
  • formal verification

ASJC Scopus subject areas

  • Business, Management and Accounting (miscellaneous)
  • Accounting
  • Computer Networks and Communications
  • Information Systems and Management
  • Economics and Econometrics
  • Safety, Risk, Reliability and Quality
  • Control and Optimization

Fingerprint Dive into the research topics of 'Formalizing Correct-by-Construction Casper in Coq'. Together they form a unique fingerprint.

Cite this