@inproceedings{DBLP:conf/tacas/CassezFA22,
  author    = {Franck Cassez and
               Joanne Fuller and
               Aditya Asgaonkar},
  editor    = {Dana Fisman and
               Grigore Rosu},
  title     = {Formal Verification of the Ethereum 2.0 Beacon Chain},
  booktitle = {Tools and Algorithms for the Construction and Analysis of Systems
               - 28th International Conference, {TACAS} 2022, Held as Part of the
               European Joint Conferences on Theory and Practice of Software, {ETAPS}
               2022, Munich, Germany, April 2-7, 2022, Proceedings, Part {I}},
  series    = {Lecture Notes in Computer Science},
  volume    = {13243},
  pages     = {167--182},
  publisher = {Springer},
  year      = {2022},
  url       = {https://doi.org/10.1007/978-3-030-99524-9\_9},
  doi       = {10.1007/978-3-030-99524-9\_9},
  timestamp = {Fri, 29 Apr 2022 14:50:36 +0200},
  biburl    = {https://dblp.org/rec/conf/tacas/CassezFA22.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org},
  urlpaper = {papers/eth2-tacas-22.pdf},
  abstract = {We report our experience in the formal verification of the reference implementation of the Beacon Chain.
  The Beacon Chain is the backbone component of the new Proof-of-Stake Ethereum 2.0 network: it is in charge of tracking 
  information about the validators,
  their stakes, their attestations (votes) and if some validators are found to be dishonest, to slash them (they lose some of their stakes).   
  The Beacon Chain is mission-critical and any bug in it could compromise the whole  network.
  The Beacon Chain reference implementation developed by the Ethereum Foundation is written in Python, and provides a detailed operational description of the state machine each Beacon Chain's network participant (node) must implement. 
  We have formally specified and verified the absence of runtime errors in (a large and critical part of) the Beacon Chain reference implementation using the verification-friendly language Dafny.
  During the course of this work, we have uncovered several issues, proposed verified fixes.
  We have also synthesised functional correctness specifications that enable us to provide guarantees beyond
  runtime errors. Our software artefact with the code and proofs in Dafny is available at \url{https://github.com/ConsenSys/eth2.0-dafny}.}
}

{"_id":"6J68HjM7gx9P757NE","bibbaseid":"cassez-fuller-asgaonkar-formalverificationoftheethereum20beaconchain-2022","author_short":["Cassez, F.","Fuller, J.","Asgaonkar, A."],"bibdata":{"bibtype":"inproceedings","type":"inproceedings","author":[{"firstnames":["Franck"],"propositions":[],"lastnames":["Cassez"],"suffixes":[]},{"firstnames":["Joanne"],"propositions":[],"lastnames":["Fuller"],"suffixes":[]},{"firstnames":["Aditya"],"propositions":[],"lastnames":["Asgaonkar"],"suffixes":[]}],"editor":[{"firstnames":["Dana"],"propositions":[],"lastnames":["Fisman"],"suffixes":[]},{"firstnames":["Grigore"],"propositions":[],"lastnames":["Rosu"],"suffixes":[]}],"title":"Formal Verification of the Ethereum 2.0 Beacon Chain","booktitle":"Tools and Algorithms for the Construction and Analysis of Systems - 28th International Conference, TACAS 2022, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Munich, Germany, April 2-7, 2022, Proceedings, Part I","series":"Lecture Notes in Computer Science","volume":"13243","pages":"167–182","publisher":"Springer","year":"2022","url":"https://doi.org/10.1007/978-3-030-99524-9\\_9","doi":"10.1007/978-3-030-99524-9_9","timestamp":"Fri, 29 Apr 2022 14:50:36 +0200","biburl":"https://dblp.org/rec/conf/tacas/CassezFA22.bib","bibsource":"dblp computer science bibliography, https://dblp.org","urlpaper":"papers/eth2-tacas-22.pdf","abstract":"We report our experience in the formal verification of the reference implementation of the Beacon Chain. The Beacon Chain is the backbone component of the new Proof-of-Stake Ethereum 2.0 network: it is in charge of tracking information about the validators, their stakes, their attestations (votes) and if some validators are found to be dishonest, to slash them (they lose some of their stakes). The Beacon Chain is mission-critical and any bug in it could compromise the whole network. The Beacon Chain reference implementation developed by the Ethereum Foundation is written in Python, and provides a detailed operational description of the state machine each Beacon Chain's network participant (node) must implement. We have formally specified and verified the absence of runtime errors in (a large and critical part of) the Beacon Chain reference implementation using the verification-friendly language Dafny. During the course of this work, we have uncovered several issues, proposed verified fixes. We have also synthesised functional correctness specifications that enable us to provide guarantees beyond runtime errors. Our software artefact with the code and proofs in Dafny is available at ˘rlhttps://github.com/ConsenSys/eth2.0-dafny.","bibtex":"@inproceedings{DBLP:conf/tacas/CassezFA22,\n author = {Franck Cassez and\n Joanne Fuller and\n Aditya Asgaonkar},\n editor = {Dana Fisman and\n Grigore Rosu},\n title = {Formal Verification of the Ethereum 2.0 Beacon Chain},\n booktitle = {Tools and Algorithms for the Construction and Analysis of Systems\n - 28th International Conference, {TACAS} 2022, Held as Part of the\n European Joint Conferences on Theory and Practice of Software, {ETAPS}\n 2022, Munich, Germany, April 2-7, 2022, Proceedings, Part {I}},\n series = {Lecture Notes in Computer Science},\n volume = {13243},\n pages = {167--182},\n publisher = {Springer},\n year = {2022},\n url = {https://doi.org/10.1007/978-3-030-99524-9\\_9},\n doi = {10.1007/978-3-030-99524-9\\_9},\n timestamp = {Fri, 29 Apr 2022 14:50:36 +0200},\n biburl = {https://dblp.org/rec/conf/tacas/CassezFA22.bib},\n bibsource = {dblp computer science bibliography, https://dblp.org},\n urlpaper = {papers/eth2-tacas-22.pdf},\n abstract = {We report our experience in the formal verification of the reference implementation of the Beacon Chain.\n The Beacon Chain is the backbone component of the new Proof-of-Stake Ethereum 2.0 network: it is in charge of tracking \n information about the validators,\n their stakes, their attestations (votes) and if some validators are found to be dishonest, to slash them (they lose some of their stakes). \n The Beacon Chain is mission-critical and any bug in it could compromise the whole network.\n The Beacon Chain reference implementation developed by the Ethereum Foundation is written in Python, and provides a detailed operational description of the state machine each Beacon Chain's network participant (node) must implement. \n We have formally specified and verified the absence of runtime errors in (a large and critical part of) the Beacon Chain reference implementation using the verification-friendly language Dafny.\n During the course of this work, we have uncovered several issues, proposed verified fixes.\n We have also synthesised functional correctness specifications that enable us to provide guarantees beyond\n runtime errors. Our software artefact with the code and proofs in Dafny is available at \\url{https://github.com/ConsenSys/eth2.0-dafny}.}\n}\n\n","author_short":["Cassez, F.","Fuller, J.","Asgaonkar, A."],"editor_short":["Fisman, D.","Rosu, G."],"key":"DBLP:conf/tacas/CassezFA22","id":"DBLP:conf/tacas/CassezFA22","bibbaseid":"cassez-fuller-asgaonkar-formalverificationoftheethereum20beaconchain-2022","role":"author","urls":{"Paper":"https://franck44.github.io/publications/papers/eth2-tacas-22.pdf"},"metadata":{"authorlinks":{}},"downloads":2,"html":""},"bibtype":"inproceedings","biburl":"https://franck44.github.io/publications/franck-pubs.bib","dataSources":["8742EsvjQfyP2fYBW"],"keywords":[],"search_terms":["formal","verification","ethereum","beacon","chain","cassez","fuller","asgaonkar"],"title":"Formal Verification of the Ethereum 2.0 Beacon Chain","year":2022,"downloads":3}