Casper the Friendly GHOST: A correct-by-construction blockchain

hmm hey everyone so this time I'm gonna start my talk for real no no kidding around we're gonna hear about a crack by construction block chain consensus protocol and you know I hope you're all excited to be here and I hope you're all aware that I'm starting to speak and so are coming into the room but I don't have time to wait so here we go so firstly let's do a basic introduction like consensus protocols are kind of fundamentally about deciding like notes on a distributed network making the same decisions even though they might have different views of the network right and those decisions you think of them as being on values but normally you know we think about in our context replicating a virtual machine or some kind of state machine so traditional consensus protocols decide on one block of transactions at a time whereas and they do it with irreversible finality with every single block right you come to a Byzantine quorum you sign the block and you and every block is created and there's never any Forks and this usually requires on the order of the number of validators messages for every block to accomplish this right because you have to come to consensus before you make every block essentially improve award consensus on the other hand we don't come to consensus on every block before we make it instead we have this kind of forking phenomena where we just try to put the block on there but if we fail it might leave but somehow if we wait long enough we feel like oh it's never gonna leave the block chain and these protocols have a much lower overhead so basically the thing that I'm gonna show you today is consensus protocol cast with a Friendly Ghost which finalized every block with asynchronous Byzantine fault tolerant consensus safety the way that traditional sense protocols do but is able to do this with the overhead of proof work law chains so you know it kind of represents some of the best of both worlds right both finalize decisions and also hyper low network overhead and the reason why this is cool is because it kind of provides us a unified way for thinking about both of these things so I'm gonna give a little overview of my talk and then I'm gonna go right into it so the consensus safety proof is this thing that all of the consensus protocols that are correct by construction process satisfying and then I'm gonna specify some of these things and then I'm gonna talk about maybe live this a little bit and then give some experimental observations where we're gonna see this kind of network efficiency that I'm talking about so let's get started so the consensus safety proof is probably the most important thing that you understand in order to grab grok this whole process so we need a few things for this thing to be fine we have protocol States and state transitions and we have an estimator and this thing called ask me safe team you can find them in a second and then we have this Theron this result that if nodes have a common future state in the protocol then they have because then they have consensus safety on decisions that are that have estimate safety so if I decide on something with estimate safety then I'm gonna get consensus safety for free if we have a common future and so basically protocol states are just like things in a group and purchased a transitions are kind of paths between them right an estimator takes these protocol states and maps them to in the binary consensus like a 0 or 1 and the blockchain consensus like a whole blockchain so it's kind of our fork choice rule mechanic right a little guess and estimator is not a decision it just guesses looks like we have so an estimate is safe basically if the estimator for all future possible protocol states that can be access from that from that state the the estimator returns this returns a value like 1 or has a blockchain that also is that that will always have that block in the chain so block is safe if all future blockchain Fork choice rules for choices have that block in the chain and a bit is safe if all future estimators have that bit so if two estimates are safe at two States and those states have a state in common then because those things are the estimates hold for all future states and they have one in common they'll both hold from in that one state that they have in common and that means they have to be consistent because you can't have you know the block be in the fork and not at the same at the same thing so in that was come the first part of the proof basically it says if noes have a common feature then they have consensus safety the next part basically is a construction to make sure that they will have a common future unless there's more than some number of visit defaults and the way this works is basically have protocol states which are messages we have state transitions which corresponds to receiving messages or increasing your the saw like you know going to super sets of protocol messages and if we count Byzantine faults and exclude the sets of messages I have too many faults then we can guarantee that they have a common future is unless there's that number of faults basically because first we allow all of them to have a common feature no matter what then we remove the states that have too many visiting faults and so two states will have a common future unless there's too many Byzantine faults and that gives us kind of our key result here which is that as long as there's not too many Byzantine fault so they have a common future and if a common future then they have consensus safety and so this this consensus safety proof basically says look I've always thought too many Byzantine faults then we have consensus safety and the cool thing about this is I had I had to say almost nothing about the consensus protocol right all I had to do was say it has protocol states and and I mean I said nothing about the nature of the estimator right and so now we're gonna kind of see this we're gonna see this thing happen so I'm going to define protocol messages and then the estimator isn't seen fault detection States and state transitions and then the an estimate safety for the binary consensus and then we're gonna do a tiny change and generate the walk team consensus and a tiny change and to validate rotation a tiny change and remove fault tolerance threshold from the protocol and that'll kind of demonstrate the the the power of the approach here so for the binary consensus we have protocol messages that are bits they sorry they have three parts a bit for the for the estimate sender which is like the node assented and a justification which is a set of messages the protocol messages dependency of the other if it's like in the justification or in those justifications basically if there's pre block pointers or pre patch pointers to it and then it's a dependency latest message is one which there's no there's there's nothing earlier right so dependencies earlier if you're not depending than later and a latest message is it's kind of extremum there so the way that the binary comes as this works is you look at all the validators latest messages if more of them by weight have zero then you pick zero and if more than by weight have one then you pick zero they pick one so basically if this sort of score of an estimate is the sum of the validators who have latest messages who have that estimate and if the score on zero is more than sierra one the estimator returns zero otherwise it returns one and otherwise and and if it's a tie then it returns it's kind of exception so so so that's kind of a definition of estimator and and that's that that's kind of gonna be necessary for us to have the concept of deciding on safe estimates so Byzantine faults are kind of this interesting and tricky thing basically each of these nodes have are making messages where they store they detest what they've seen from other nodes right and if it's ever the case that I have a set of messages where different nodes attest to having seen some node make messages that could never have possibly been made by a single node then we have a Byzantine fault because basically a single nodes with the way they're characterized is that they follow protocol executions according to the like the protocol executions in in the state so so here equivocation is this is this property that to knows that a data that it's that a note isn't actually a single-threaded and it means that they made two messages neither of which are in the dependency of the other so rather than including their messages in each other and having a single thread they have them all it's multi-threaded and we can basically are gonna be able to identify Byzantine nodes by their equivocations and we can like you know like count them all up we can measure their weight and then we can define protocol States as all of the sets of messages that evidence less than something were faults then we defined protocol executions just as supersets in those things and then we're basically done the binary estimate safety basically means that the so it's estimate is safe give us some fault tolerance in some state if for all future states that estimate is also the estimator in future states so there's I get this invariance right all future states will return zero all future states tomorrow and because of the way we constructed this this satisfies our safety proof they all have future states unless there's T faults if they have future states they have good sense of safety and so we have a binary consensus protocol with safety and you know this is kind of where we can relax because this was that was all the heart that was most of the hard work we're never gonna find the block tanks in this protocol and it's really gonna be a lot easier because we've already done most of the work so the blocks kind of look very similar to the messages for the binary consensus only instead of having a bit there's a there's another block in the first in the in the estimate spot so every block kind of has a pre every block kind of has a pre block a sender and justification and there's this thing called the Genesis block and like the and and and this is kind of a Heights the hot the heights of the blocks so you know this is me defining like all of the blocks being all the blocks at all the Heights so there's a couple more definition that we need basically instead of having an estimate just be the same we're gonna have the estimate be a member of the blockchain and that's what this represents like block one is in the blockchain a block two and then the score of a block is the weight of validators whose latest messages are have the Block in their block chains so if if five long if like five way to the validators have block a in their latest block chains and three of the weight have locked be in the latest block chains and block a will have a higher score so then we can have this fork choice rule it's called the greedy heaviest observer subtree you start at the Genesis block you look at the children of the Genesis block which are the blocks that have a free block pointer to the Genesis block and you ask what are their scores and their scores are given by whether or not or how much of the weight of the validators latest messages are on those block chains and then you pick the best child and then you kind of repeat the process where again you calculate the scores for each of the blocks by looking at the latest messages and seeing if who's validators latest messages are on those blocks and then you pick the block with the highest score until at some point you get to a block with no children and that's kind of represents the hole for choice the cool thing here is that protocol states the state transitions are defined exactly as before there is literally no change right we just like the tech Byzantine Falls is exactly the same way exclude defined protocol states and set some messages it with less than some faults and state transitions as super sets and then we can define estimate safety for the block block chain and basically is very similar and ease that for all future protocol states this block is in the blockchain that we're going to choose of those future states so a block is safe if at all future for choice rules that you make that block will be in there so that and that and that was actually it right because all the other stuff and then the the specification is really kind of like done there because and we got to benefit from all of the work we did earlier from the safety proof and the binary pretty much reuse most of those most of those most of that work and only had to redefine you only had to define the message type the score of blocks the fork choice rule and safety so that's pretty cool we were able to go from the binary consensus to the blockchain consensus with a minimum change safety Oracle's this is kind of important it's kind of important that we are able to detect safety I'm not sure happened this slide so and no like what I've shown so far is if you were to make estimate decisions on safe estimates then it would be consensus safe but you might you need a way we might actually need a way to figure out if that's the case so we have a couple of definitions here and this I'm gonna give like a simple way to do this so a validator sees another validator agreeing on an estimate if the latest in the latest message of validator I in their justification the latest message Missy from validator J has an estimate that agrees with the estimate that we're trying to say is safe an agreement in the binary consensus means that they are the same bit in the blockchain consensus means that they are in the Block in the blockchain of the other block so so VI sees BJ means that the validator I see the latest message from validator J that agrees and there's another definition you know that's cropped out and it basically says the VI can't see VJ disagree which means that they there's no new latest message from GJ that they could see that doesn't agree with the estimate and so basically if there's a set of validators who can't who see each other agree and can't see each other disagree it turns out that if they have some number of wait some amount of weight and that weight is more than more than half the weight then you then you can actually show that there are some amount of fault tolerance but our safety definition requires that we have t fault although we can tolerate up to T faults however there might already be some initial faults in our view so we kind of subtract that so basically as long as the the the this is this is kind of the overlap between two sets of Valladares that would like the overlap and weight of the validators in the klique if that's more than the fault tolerance then we're then we have safety it's very similar to a traditional kind of consensus safety proof only it's working on these estimates instead and the intuition is quite clear basically if in the clique they can't can't convince each other that they've seen something else and if they have more than half the weight then whoever can convince them from outside the clique won't have enough weight to actually contribute great so that actually was a hard part also but we're getting through it we're almost done so subjective fault tolerance thresholds is a pretty cool thing basically if you have two protocols which have the same words are the same except for the fact that they operate two different fault tolerance threshold and one of them is small on the other then consensus then no to make decisions in these protocols will actually have consensus safety as long as the number of Falls exhibited in their union of their views is less than the smallest of their fault tolerance thresholds and it's really cool because having fault tolerance partials in the protocol makes it easier to attack and pose a bunch of economic problems that are out of scope for this talk but stuff about cartelization and focal points validate a rotation this is an exciting thing so I mean I've changed the structure of the blockchain a little bit to add weights to the to the block right before we had validated weights kind of this global thing now we're gonna add weights to the justification though so the you know blocks give me the same as before like you know they have a block ascender justification and the justification now has this additional thing called the weights and then we can we need to be define the score of a block to use the weights of the parents block in order to actually choose that block so if block a has weights has a certain set of weights then the children walk a which are the blocks that have a pre-populated block a need to be chosen according those weights and not a single one of the other definitions need to change and so this is like really like all that we needed to do to do consensus safety sorry to do validate rotation with consent the safety basically because all of the definitions satisfy the the car crackers like the the abstract safety proof you know because like because they they you know they're they have a common feature unless there's t faults and they only decide on safe estimates so liveness is an interesting thing you know liveness means and knows like events are guaranteed to eventually make a decision there's a result in consensus literature called FLP and poss ability that means that you know you can't really be live and safe in an asynchronous network without and without using entropy or oh no without using entropy or cryptography but actually we have we have kind of a bigger issue than just have up being possibility which is that we never said anything about when validators were actually meant to send blocks they actually we just haven't specified that yet cuz all we really talked about is safety and so however we're gonna see in our experimental results in just a second that there are state sets of messages that they could get to which are safe and that means that as long as we can make those shapes then we can have liveness but and and we kind of know that in an in a synchronous network or in a partially synchronous network nodes can use timeouts to make this kind of message shape you know up to some number of faults and so and so if we were to pick one of these then we could we could give a we could give a lightness proof for some strategy that says oh look you guys have to figure out how to make a dag and this messages in this in this form but you know we're not really gonna do that we're just gonna leave liveness out of the story for now so I'm gonna I mean this is kind of the maybe the more exciting part of the talk so this is we're gonna look at actually and try to see what this looks like so these are three validators running the binary consensus and they the color here means that they've reached safety with some of them some amount of fault tolerance and kind of they they're they're the the numbers in here you see there's ones and that one's a zero it can be a little bit hard to see the numbers are their estimates and they need to have the estimate be the max weight of the latest messages they've seen in the justifications these arrows these lines are the met point to the messages that are included in the justification remember the the data structure is estimate which is a bit sender which is like you know validator one validator to about a three and the justification which is encoded with this with this structure showing you know a few more nodes company consents on a bit here so the darker color means that they have more fault tolerance this is kind of cool because it illustrates the the flexibility that we have about the order of message passing because we haven't said really anything at all actually about that now the blockchain consensus protocol is a little bit more complicated to think about because it's got these things called pre block pointers right so there's dotted lines these thin ones are justification pointers these are free block pointers the blue ones are the latest for Khalid ators and the red one is our fork choice so basically like you know the way the fork choice works is okay you know you so validator wanna has the most weight so from the Genesis block we go to balladeer one and here there's only has one parent and here we could we could have went that way or this way but actually the latest messages are here there and there and all of them have their weight here and so the weight is all on this fork and not on that one and so we pull left and then here you know there's a pre block pointer here and also another one there and if you look at the latest messages there's more of them here and so and so that's why we're gonna go there and and and and and what this kind of shows you here is that validator 3 has more weight than validator 1 right so the reason why we initially chose this actually wasn't because validator 0 had more weight is because all of their latest messages are on this one so here we go so this so this is kind of the blockchain consensus kind of an action for three notes there they're gonna like use greedy heaviest observed for choice rule where every every choice in the road that but first we went that way and then we went that way because more validators made walks there here we were only fork right there's this forking on the top and then here we achieve safety right this kind of say this is one of these things get colored to have a synchronous Byzantine fault tolerance safety and notice the word they fork at the top and they have safety at the bottom and the way we calculate safety here you know is using the safety Oracle that I described earlier where you look at these cleat which see each other agreeing can't see each other disagree now we can watch more nodes go faster and here's the you see some interesting stuff were like a bunch of a bunch of blocks will get finalized at the same time sometimes right because every the thing that kind of realize like blocks can contribute to the finality of many many blocks and and basically because every block you have will like agree and disagree with other blocks large number of them and which blocks you disagree with and agree with actually will determine how the safety Oracle turns out and so remember the colors not forking up here at the top lots of 4k like look at the red line it kind of goes and changes right like you don't really know if these blocks are confirmed or they're gonna be consensus but the ones down here are right so it's very much like a four key thing it's a kind of a blockchain like thing but this is really this is really what I'm talking about this is kind of what I was saying when I say that I can achieve asynchronous Byzantine fault tolerant consensus with the overhead of Nakamoto consensus if you if they do manage to send the messages around a round-robin then eventually you get to a point where every additional message finalized an additional block and this kind of overhead for finality of consensus at every block like one message per block for finale at any level of thought on a threshold is like theoretically optimal because you know you can't really get lower than one message for block and this kind of little interesting here you see that this validator has more weight than these two there's why the fourth choice rule this validator even though you saw that block whatever preferred to built on his like initial block than these ones because these two guys have less weight than this one and so this is kind of what I mean when I say that like you know we can achieve really really efficient asynchronous consensus a few so somehow you know I know it's like a bit much but I shared consensus safety proof that talks about you know these local determinations of estimate safety and how they're related to consensus safety we're able to define of watching consensus protocol through like basically by first defining the binary consensus protocol by the safety proof and making a really like minor change that doesn't affect the safety proof at all and then we were able to actually add validate a rotation and remove finality thresholds also with very minimal changes to the protocol and the reason why we can do this and why it's like so little work is because of the fact that the proofs that were lying on are not changing while we're making these changes right there we have like abstract safety proofs concrete protocols which we can tweak without changing the safety proof and you know we were able to achieve this really nice kind of latency numbers so that you know I think that you know this is hopefully gonna be educational hopefully gonna lead to new consensus protocols you know we actually have a bunch of Kuznets protocols that were mentioned here that were derived according this process replicating things like concurrent instead of sequential ones or like an integer through these domain for time stamping so here's a little secret mmm just now I published the prototype for the for these fourteen consensus and also this white like a specification in very much detail of all of this stuff and more incomplete description of the correct my construction process given at a very very high level of abstraction much higher than I even hinted at today so you know this kind of represents the state of the work today and you know I gear I'm excited for you guys to check it out and to take a look at the correct my construction consensus protocols and see if you know you find them as easy to reason about as I do and then we're done right so so Nate Danny worked really hard to help me get ready for DEFCON and get the code published get the papers ready you know million thanks to them Carl who just spoke last was the first person to really actually the first developer on the correct reconstruction Casper Greg Meredith who is here somewhere but I haven't seen him yet has you know really introduced me to the correct my construction process and help me really like formalize and like kind of take this mathematical approach finally metallic you know has been working with me on this stuff for years like three years more you know so thanks for think thanks a lot for everyone and thanks you for listening [Applause] [Music]