Blogs (1) >>
POPL 2019
Sun 13 - Sat 19 January 2019 Cascais, Portugal
Sat 19 Jan 2019 11:40 - 12:05 at Sala VI - Contributed Talks 2 Chair(s): Enrico Tassi

Blockchain systems such as Ethereum are increasingly used as financial transaction mechanisms (cryptocurrencies). However, in a blockchain system, there may be several competing chains of blocks (forks) that only agree on the transaction history up to some point, potentially leading to some transactions being dropped. To address the problem of blockchain revisions, Buterin and Griffith proposed a blockchain finality system overlay called Casper. When enough participants are honest, Casper defends both against active attacks and catastrophic crashes. In ongoing work, we are formally verifying Casper in Coq, both at the abstract protocol level and at the level of a distributed blockchain system. We build directly on two previous modeling and verification efforts: verified abstract models of Casper in Isabelle/HOL, and a model in Coq of a general distributed blockchain system called Toychain. Our verification approach bridges these two efforts by translating Isabelle/HOL definitions and proofs to Coq and specializing Toychain definitions for Casper. We give an overview of our ongoing verification effort and outline how we encode and prove key Casper properties, such as accountable safety, which rules out agreement on conflicting blocks when less than one third of participants behave adversarially.

Abstract (coqpl19-final11.pdf)460KiB
Slides (coqpl-2019.pdf)367KiB

Sat 19 Jan

CoqPL-2019
11:15 - 12:30: CoqPL - Contributed Talks 2 at Sala VI
Chair(s): Enrico TassiINRIA
CoqPL-201911:15 - 11:40
Talk
Kiran GopinathanUniversity College London, Ilya SergeyYale-NUS College and National University of Singapore
File Attached
CoqPL-201911:40 - 12:05
Talk
Karl PalmskogUniversity of Texas at Austin, Milos GligoricUniversity of Texas at Austin, Lucas PeñaUniversity of Illinois at Urbana-Champaign, Grigore RosuUniversity of Illinois at Urbana-Champaign
File Attached
CoqPL-201912:05 - 12:30
Talk
File Attached