How model checking can help build trust in the design of distributed protocols like ... | Devcon SEA

[Music] hello thank you so my name is aov um the slides ah here the slides um happy to be here actually this is work done by myself uh tan hran who's also here in the room uh EUR C Thomas P who is also here and Roberto saltin and we're happy to have done this work supported by serum fun found so if you look at consensus ethereum consensus uh you probably see a lot of algorithms starting as Casper Gasper now we have single slot finality and recently on the Block we have uh three slot finality you can check uh the recent report uh by Franchesco Roberto tanhai and Luca and if you look into into these things uh you will see that there are a lot of definitions I cannot explain all of you uh all these definitions to you you will see that there are chain blocks slots uh checkpoints Justified checkpoints finalized checkpoints votes by validators FFG votes uh that connect these checkpoints and so on so forth so these are not simple algorithms so in our work we don't uh we don't have uh basically time budget to to do everything so we focus on accountable safety which means roughly speaking that if if you have a fork in consensus we should be able to identify at least oneir of the uh validators that are basically uh that produce this fork and they should be slashed so we focus on accountable safety here how would we be able to check that these protocols uh namely three uh three slot finality satisfy accountable safety well in science fiction solution when it's all good uh we would take the code in Python we'll take the executable spec in Python produce some examples maybe to convince ourselves that it kind of works but also would we would also produce an automatic proof of accountable safety unfortunately that's a bit of Science Fiction nowadays there are no of the-shelf solutions that would take executable python spec and reason about such complex algorithms as consensus so what we have been doing in this project we actually uh VI writing uh specifications in temperal logic factions that's a language invented by Les Lampard some time ago for reason about concurrent and distributed systems um and we did we did produce specifications by hand because there are no tools that would be able to do it although we have been thinking how we could automate that so basically the first specification we wrote was just two complex for the model Checkers uh we greatly produced obstructions using this specification and essentially produced like four levels of obstructions here so the model Checker could handle uh the complexity of the algorithm in the end we used the model check palache which uh is offloading the verification task to the smt solver Z3 and in addition to that as things were a bit slow we also wrote a specification in alloy which is also a well-known model Checker that is backed by aat solver and in addition to that we wrote uh smt constraints in uh CVC 5 using the theory of finite sets and cardinalities so we kind of did a lot of experiments here to check accountable safety on the different uh using different tools so as I told you model checking uh could help you how can it help you the first thing where it can help you is actually you can qu for interest in States if you have a large protocol it's not easy to produce examples and that's what model checking is good about for instance here I'm just writing an invariant saying there are no two conflicting blocks basically there is no fork and challenge the model Checker with this false invariant then the model Checker comes back in several minutes and shows me an example so actually these tools uh work uh as a good communication tool for protocol designers he is an example of such an execution you don't have to read it it's just laan but it's machine readable and it's an actual execution in in this specification so the second thing where this tools can help you is to show some properties uh not for all kinds of uh values but for small scopes for small parameters for instance here we have experiments for five blocks seven checkpoints 24 vots and as you can see when we increase the parameter space the tools uh slow down dramatically however we have some evidence uh that these properties hold true at least for the small parameters and that's again fast feedback that you can get without proven things in heavy tools so to come to the summary of of our work we believe that mche can actually helps in ensuring correctness of protocols uh we still need humans in the loops unfortunately we still need us basically to construct this abstractions and specifications uh tune in for the upcoming technical report we are going to publish all of it and you'll see it and thank you eum foundation for giving us a grant thanks a lot thank you Igor does anybody have any question okay okay I think it was very clear nobody has any re you have to quick and come back again at okay okay if there are no more questions just thank you for thank you we will