A Correct by Construction Asynchronous Casper Protocol

[Music] I'd like to introduce our next speaker by just saying that he is going to be speaking on Casper and there are many different approaches to Casper proof of stake and um because I really wanted to um give lad zier a special introduction I think we should all chant Casper Casper Casper Casper Casper Casper Casper come on up [Applause] Vlad super dumb okay great I'm I'm miked up already uh White clicker all right let's just test the clicker great all right um all right are we ready to go time's rolling okay time to go uh so I'm going to present to you basically my research on uh correct by Construction Casper um you know which I've done over the last few months with a lot of thank with a lot of help and kind of got in from Greg Meredith I can't see him right now through all the glaring lights but I thought I'd give him a shout out right away so um so I'm going to cover some background knowledge for about consensus protocols and then I'm going to talk about and like cover my research for for Casper and then I'll kind of relate it to the previous literature and talk about future work so there's a lot to get through I'm going to do it really fast uh so for here's my little there a table of contents who cares right uh so what are consensus protocols consensus protocols basically are something that nodes Ed to make the same decision about something this is like the kind of traditional definition of consensus protocols that really um has it concept of decision as like at its core um and a consensus Proto and having consensus basically means that we have the protocol in a state where uh all of the protocol following noes are guaranteed to make the same decision um and and basically these protocol following nodes are the protocol is called safe if they're if when they make a decision uh they will always make the same decision it's called uh it's called live if uh there it's definitely the case that they will make a decision eventually in some in some in some in some kind of finite amount of time like you can like guarantee like prove that they will make a decision um so so those are like some basic concepts of livess and safety that and so let's let's review them quickly again so safety is the property that when knows decide they all decide the same thing liveness is the property that nodes will eventually decide um asynchronous networks are are basically this like Topic in and cons protocols that uh is not really related to asynchronous like calls and asynchronous Computing it just has to do with the fact that we don't have timing assumptions on the network um which basically means that Communications can arrive in any causally consistent order like any order where like you know if a message be that like is causally uh you know is caused by a message a like can't arrive like before message a that's like the only kind of the only kind of ordering that's imposed on network messages is the ordering that's imposed by the causation of the protocol State updates um and usually with asynchronous networks we we assume that the network that the messages get arrive event arrive eventually but we just we can't ever say in what order um so asynchronous consensus is kind of difficult and we kind of know this because of this flp impossibility result which says that like in an asynchronous Network you can't actually be live and safe and in the presence of one fault or more basically if if any of these um Communications can fail you can you can kind of show that in an asynchronous Network um you you can't be both guarantee that everyone will make the same decision and that we'll be able to make a decision in a finite amount of time and and the reason for this uh we're we're going to we're going to see through the course of this of of this talk um uh but but this this kind of gets at the point that a syn a synchronous consensus is really challenging because um the the lack of network assumptions makes it really hard for us to justify why the protocol would move forward from a state where we don't know what to decide to a state where we would know how to decide there needed to be some messages that flow that H uh for that to happen but if uh some messages might not actually make it then we can show that actually we can't prove that that there's a guarantee that in a finite amount of time uh this kind of decision will be made safely uh and now we just talk a little bit about Byzantine fall cont Byzantine faults you've probably heard of Byzantine fault tolerance um it's all the rage these days uh any basically normally what we say is that any node that isn't following the protocol is Byzantine uh and we normally also say that nods behave in arbitrary ways um we also have results that basically kind of also say that this is kind of hard stuff like B there's are like limits to what can be done normally there's like two results one of them is that in an asynchronous Network you can't have more than a third Byzantine fault tolerance and in a in you know where you have like safety right where I we have this property that if nodes decide they will all decide the same thing uh and we have a similar result for synchronous networks where like you can't tolerate half the nodes being faulty and also have all the nodes that are following the protocol be guaranteed to make the same decision uh so I'm kind of just asking you to like accept this at this point because we've got to go and get through the rest of the presentation uh so so so now I'm going to describe basically this is like correct by construction approach that I'm that I've been taking for uh my Casper research especially in the last couple of months uh basically there's like an outline and then I'm going to describe my data structures and give some definitions and then give the correct by construction binary uh decision a decision thing one thing I should have mentioned at the top of the talk is that like the the title of my talk is like slightly different than advertised so what what what I'm really going to be presenting is a correct by Construction asynchronous Casper consensus protocol that agrees on a bit so like it agrees on like zero or one uh and it's and it's going to be Byzantine fault tolerant and and correct by construction so no no network assumptions we can tolerate like Byzantine Behavior Uh but we only we only agree on a bit um and still I think that's worth presenting uh so basically so here's kind of the the approach that I'm taking um rather than thinking about the safety of decisions I'm I'm going to I'm going to think about estimates right so estimates are these things that kind of uh are sometimes defined in some consensus protocols but are always defined really in like the blockchain world an estimate is like a non-f finalized decision it's like a uh it's like a a proposal for a decision like when we talk about traditional consensus protocols all of the decisions that we're talking about are like what we call in blockchain World finality right like finalized decisions that will never get reverted where these nodes like commit to this value and will'll never ever ever change their minds because like that's what the protocol says and like that's the definition of consensus oh my God we're running out of time so we use estimates and uh you know so we and and they mean finality so basically we're going to Define uh a notion of safety on estimates b b and and basically what we're going to do is try to and we're going to construct an adversary which will try to change an estimate for a particular node with a particular view who has an estimate uh in order and if that adversary succeeds then that estimate will be uh be unsafe because in that particular uh Network context for example uh it's possible for that estimate to change uh and and and basically um uh the the reason why we're doing this is because an estimate is kind of a very P personal thing whereas the sa and the safety of an estimate meaning like oh my estimate can't change is a is it's much easier to determine on a local view than the safety of a consensus protocol which has to do with the decisions that different nodes make across the network um and so I think it's just easier to reason about so and and if we have this result which you know I'm going to show that we do or I may I'll show somewhere that we do even if I don't show you today uh that if nodes calculate that their estimates are safe uh then they both will have the same estimate um so and and this is actually going to guarantee our correct decision rule basically nodes are going to calculate if the estimate is safe and if it's safe then they can decide and that's going to be like the correct by construction approach where uh the the the decisions are all going to be the same I.E we're going to have SA safety because the only time when people are going to decide is after they've run this ideal adversary and saw that their estimate can't be changed and if like my estimate can't be changed then I'm like it's cool for me to make this decision because I know uh that that that'll be fine so now let's go into like the real like kind of formal model and like the technical kind of more the more technical part of the talk so basically um this is the main data structure that we're going to be dealing with these bets are they have three things an estimate a justification and a sender the estimate is basically a bit in this case because we're just doing binary consensus the justification is a set of bets or the empty set and the uh sender is like you know a validator so validators are some fixed set they have weights the weights have this tiebreaking property which means that any two subsets of the validators have different weights so that like I don't get ties ties are an annoying Edge case um so we have this other data structure called a view and a view is just a set of bets so we have bets which are have estimates justifications which are sets of bets and senders we have uh we have weights on the validators names for the validators and Views and these are all of the data structures that we will use to talk to Define everything that I'm going to like talk about for the course of this talk and that everything everything that's like defined in the correct by construction like approach um and it's worth noting that the BET structure is a dag uh and you can represent it kind of like this where I'm going to line up validators right so so the the the number on the Node is the estimate of the bet the edges correspond to which bets are in the justification and the kind of vertical alignment along these along these letters corresponds to like which validator made that bet here validator one made two bets one with estimate zero one with estimate one validator two similarly and they've got all these justifications pointing everywhere it's great so now we're going to start going some definitions where we're just going to define a whole bunch of stuff that we're used to talking about sometimes um sometimes there going be new stuff in terms of like this data structure that we just have that that I just defined and which basically is like the model that everything is going to sit on um so um a bet is a is a dependency of another bet if it's in the justification or if it's in the dependency of anything in the justification um it's a recursive definition but there's a really pretty picture the red bet is in the dependency of the blue bets basically because it is uh Upstream from them in the in these arrows um so equivocation is something that we sometimes talk about in consensus protocols I have a formal definition here of what it means for two bets to be an equivocation basically they have the same sender they're not the same bet and neither of them are the dependency of the other so basically they represent kind of uh a bet made with a justification that like ignored the fact that they previously had made a bet there's no way to make two bets and have neither of them be in the ad justication of the other without kind of intentionally leaving out something that you knew because you can't be ignorant of the fact that you made a bet really uh so here are some examples of equivocations the colored bets are equivocations um the two red ones you know and the two blue ones they don't include each other in their dependencies there's no like there's no you know Arrow saying that the one knows about the zero or that like the one up there knows about the other one um so these are equivocations and equivocations correspond to something important when we when we talk about Byzantine faults and kind of our ideal adversary um so the latest bet is another definition basically because we have this dependency relation it kind of defines like a causally after what we can also have is like from a particular view we can say oh these some certain bets are the latest here some drawings right these these bets they don't have any nodes uh with an arrow point uh pointing out there's no arrows pointing out of these uh out of these bets into another bet from the same validator so they're so like those two bets on the left are the latest nodes latest bets from validator one um not that they're an equivocation uh validator 2 validator 3 also have some latest bets there it kind of has an intuitive thing right it's like the latest bet that we've observed from them and they have we have these like little arrows to help us find the way um so an bet is invalid if the estimate of the bet is not the maximum weight estimate given the view and their justification so the justification is a set of bets it's got a view and it's got some latest bets in there and you can wait uh you know every validator has a wait every validator has a latest bet and I'm going to say okay look if these validators have an estimate one and the latest bet those validators have an estimate zero but these ones have more weight then like my bet having all that stuff into justification uh would only be valid if my estimate was one basically we're running like a majority kind of election here when we have only the uh only valid bets around people are always going to choose the major the maximum weight estimates uh so then we have this definition of Byzantine validator so this is something where normally people would Define Byzantine validator oh it doesn't follow the protocol but here what we're going to do is Define our goal is to Define everything in terms of the data structure that we set out initially right um we haven't even said what the protocol is exactly so it's saying that it's not part of the protocol doesn't really make sense and we want to make it correct by construction Byzantine fault tolerance so we can't really use the definition of oh if you're not following the protocol then you're Byzantine because we haven't even constructed the protocol yet right uh so what we're going to say is that NOS or Byzantine if they either produce an invalid bet or equivocate and this is great because in terms of our little data structure then like either you're like a sequential node that's always producing valid bets or you've done some craziness and you're lying basically you're they like telling what some node one thing telling another node the other thing uh or you're producing invalid bets and and and those are something we can identify in our bet structure and is like bad right uh and I lied about my definition of of invalid earlier you actually have to include exclude the Byzantine nodes in your calculation here so like you know if a bet has if a if a node has two latest bets you just like drop their weight to zero uh if a node made an invalid bet you drop their weight to zero um here are some invalid bets there's like not majority estimates given the weights that were observed below uh I'm just going to power through because we've got a lot to cover um so basically an an estimate is safe in a view uh uh basically if um there there is no possible future of an of the view which means like additions of bets to that view where the estimate is changed um in a particular context in this case we're just talking about an asynchronous Network so so an estimate is safe in an asynchronous network if no matter what valid bets you added no matter what Communications occur the majority estimate just won't change so all possible futures of this state of the protocol in just only asynchronous conditions I.E like any causally consistent sequence of of message passing is cool uh um there's there the estimate is the same or there is no possible future where the estimate is different then it's then it's safe but this is kind of uh not a constructive definition so that won't do for our correct by construction kind of thing what we need to do instead is calculate safety by producing this adversary that tries to kind of make the network condition happen um that changes the estimate so here's an example of an an adversary that like shows this bet from from validator 3 to validator 2 in order to induce validator 2 to produce a new bet because now validator 2 sees a different max weight estimate uh and that changes the overall max weight estimate that we see from the The View as a whole so like that first view was like not safe um and and basically we have a slight issue when we're trying to calculate this this this this adversary because we have side effects uh so so what we're going to do is actually have a lower bound and ignore ignore the side effects basically because the side effects if they help the attacker the attacker can can go with and if they don't the attacker will ignore so this attacker is stronger than normal so if this attacker fails then definitely your thing is safe um uh uh so basically the way that to con do the constru construction for uh the ideal the ideal attacker for an asynchronous network is basically to only allow bets that have the uh the the don't have the victim estimate in there to travel and only allow bets that don't have victim the victim is estimate in there to be made so the the adversary just like stops all bets that disagree with his estimate from traveling across the network um and like that's the kind of Ideal Network adversary for an asynchronous network uh and then the decision rule in asynchronous network is oh once I calculate that my estimate can't change under this ideal adversary I decide and that's correct by construction because um you know the the there's no way um for two NOS in the same in the in the in in the network to disagree about whether there's a possible future of that Network where they have different estimates um because they're they're they're because they're both modeling this asynchronous network it's a little bit of a subtle argument basically because uh if they have different estimate then one of them has to be later than the other which meant that the first one has to have a possible future that changes it one of the estimates to the other um but we're really running out of time uh uh so with equivocation uh we also do this thing where only The Bets with the wrong the wrong fly around but you also get some additional flexibility about where you can add bets cuz you don't have to only add them on the end latest bets right you can add bets anywhere because like equivocate equivocating validators are crazy they just they just add bets wherever right um so but but it's like the same type of idea where like if we're safe in that equivocating environment then like we decide okay we can stop and it's like a correct by construction decision function of like when to stop participating the consens I.E when to make this final decision right so this is very related to like finality and that whole discussion right so I'm going to try to quickly relate this to existing research basically the only stuff that I've talked about here has been expost kind of safety measure where we don't actually look we didn't talk about liveness at all uh and so we don't violate FP impossibility at all we have vistine fault tolerance and safety and asynchronicity we don't have liveness that's great um and basically we can see why we don't have liveness because like if we if we if we don't so like if we if we don't have safety at a particular point then we cannot prove that we will advance to a point where we do have safety in the context of this um adversary because that adversary by the virtue of the fact that we said we don't have safety is able to change our estimate and therefore um uh uh we can actually become safe from a position where we aren't safe in a way that's provable uh and so like we haven't violated IP at all um so basically uh we it was cool that we did it only this expost measurement of sa rather than reasoning about liveness at all because that's normally not usually what happens so like there exist views in this expost world where you have extremely high levels of fault tolerance where like all but one node could be faulty and your estimate still won't change because like any of these faults will be detected by everyone and those weights of those nodes will drop to zero but so it's very very safe but there's like no way to actually get to that point if all nodes but one are Byzantine because they'll presumably not participate in the network behavior that was required to create that kind of system uh so it's not l we don't actually have a guarantee that we'll get there from a point where we don't have it to this like point where we're safe uh so uh I think it provides kind of an interesting view into business default tolerance in general and I hope we can extend this Research into live livess and also toine everything in terms of the same data structures right because these bets being passed around really do basically map exactly on to the kinds of restraints on the network that we normally have so we have a whole bunch of future work right so what I just said liveness um I want to make a conservative attacker that the minimum izes the amount of equivocation that needs to happen by weight uh this will improve the uh computational complexity of stopping in uh in a bantine fault context we need to move from consent on a bit to consent on the evm we need to do validator rotation we need to add economics um so we can like run it in public and we need to do like complexity and performance optimization and basically you know improve like the theory the specification the documentation the implementation by the way I do have an implementation of the correct by like correct by construction thing I mean mostly I have the ideal adversary implemented in like python for equivocating faults so like that's cool in asynchronous network um my time is almost up and my slides are done thanks for listening excellent thank you lad good job