Ethereum Foundation Devcon2, 19 Oct 2016

Previous Meeting Next Meeting

⏯

youtube image

►

From YouTube: A Correct by Construction Asynchronous Casper Protocol

Description

Visit the https://archive.devcon.org/ to gain access to the entire library of Devcon talks with the ease of filtering, playlists, personalized suggestions, decentralized access on IPFS and more.
https://archive.devcon.org/archive/watch/2/a-correct-by-construction-asynchronous-casper-protocol

This technical talk covers the ongoing formal verification and implementation efforts behind a correct-by-construction asynchronous byzantine-fault tolerant binary version of the Casper consensus protocol that is currently under development. Work extending the correct-by-construction approach to virtual machine replication, validator rotation and public economic consensus will also be discussed.

Speaker(s): Vlad Zamfir
Skill level: Advanced
Track: Developer Infrastructure
Keywords: technical, casper, byzantine, nodes, binary, decision, construction, consensus, fault, tolerance, finality, estimate, justification, sender, bet, protocol, equivocation, validators

Follow us: https://twitter.com/efdevcon, https://twitter.com/ethereum
Learn more about devcon: https://www.devcon.org/
Learn more about ethereum: https://ethereum.org/

Devcon is the Ethereum conference for developers, researchers, thinkers, and makers.
Devcon 2 was held in Shanghai, China on Sep 19 - 21, 2016.
Devcon is organized and presented by the Ethereum Foundation, with the support of our sponsors. To find out more, please visit https://ethereum.foundation/

A

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 steak and on because I really wanted to give Ladd's m fear. Special introduction. I think we should all chant Casper Casper.

B

Casper Casper Casper Casper Casper come on up, lad, whoo.

C

Okay, great I'm, miked up ready, white clicker, all right, let's just test the clicker great all right all right. Are we ready to go times rolling, okay time to go so I'm going to present to you? Basically, my research on crack by construction Casper.

C

You know which I've done over the last few months with a lot of think, with a little help and kind of guidance from Greg Meredith I can't see him right now with 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.

C

So there's a lot to get through I'm going to do it really fast. So for here's, my little that's a table of contents. Who cares right? So what are consensus protocols, because it's protocols basically are something that nodes used to make the same decision about something? This is like kind of traditional definition of consensus protocols. That really has this concept of decision as like at its core and the consensus.

C

Protein consensus basically means that we have the protocol in a state where all of the protocol following nodes are guaranteed to make the same decision and then basically, these protocol following nodes. Are the protocols called safe if they're? If, when they make a decision, they will always make the same decision? It's called called live if there it's definitely the case that they will make a decision eventually, and so 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.

C

So so there's like some basic concepts of liveness and safety that, let's review them quickly again, so safety is the property that one knows decide. They all decide. The same thing live, and this is the property that nodes will eventually decide.

C

Asynchronous networks are basically this like topic and consents protocols that it 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, 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, you know it's caused by a message. A I can't arrive like before message.

C

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 and usually with asynchronous networks. We assume that the network that the messages get arrive event arrive eventually, but we just we can't ever say in what order so asynchronous consensus is kind of difficult, and we kind of know this, because, as aflp impossibility results 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.

C

Basically, if, if any of these communications can fail, you can kind of show that in an asynchronous Network 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 the reason for this we're working on we're going to see through the course of this talk, but but this this kind of gets at the point that asynchronous consensus is really challenging, because 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.

C

There needs to be some messages that flow the happy 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, this kind of decision will be made safely. uh And now we talked a little bit about business in fault, content, Byzantine faults, you've, probably heard of visiting fault tolerance. It's all the rage.

C

These days, and basically normally what we say is that any node that isn't following the protocol is Byzantine and we normally also say that knows behave in arbitrary ways. um We also have results that basically kind of also say that this is kind of hard stuff like a base bit. There's like limits to what can be done normally well, there's like two results.

C

One is that in an asynchronous network, you can't have more than a third Byzantine fault, tolerance and in us in it you know where you have like safety right where I we have this property that if noes decide they will all beside the same thing. And thus we have a similar result for synchronous networks. Where, like you, can't tolerate half the notes being faulty and also have all the nodes that are following the protocol be guaranteed to make the same decision.

C

So I'm kind of just asking you to like accept this at this point, because we've got to go and get to the rest of the presentation, 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 my Kasper research, especially in the last couple of months.

C

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 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 whatever? What I'm really going to be presenting is a correct by construction, asynchronous Kaspar, consensus protocol that agrees on a bit so like it agrees on like zero or one, and it's going to be Byzantine fault, tolerant and and correct.

C

My construction so Network assumptions we can tolerate like Byzantine behavior, but we only will only agree on a bit and still I think that's worth presenting. So basically, so here's kind of the the approach that I'm taking rather than thinking about this safety of decisions, I'm gonna I'm, going to think about estimates right. So estimates are these things that kind of are sometimes divided in some consensus protocols, but I always define really in like the ball chain. World estimate is like a non finalized decision.

C

It's like is it's like a disproportion 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 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 use estimates, and you know so you and then a main finality.

C

So, basically, we're going to define a notion of safety on estimates, Bay 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.

C

As an estimate in order and eighth anniversary succeeds, then that estimate will be we unsafe, because in that particular Network context, for example, it's possible for that estimate to change and basically the the reason why we're doing this is because an estimate is a kind of a very personal thing, whereas the say and the safety of an estimate, meaning like oh, my estimate.

C

Can't change is it's much easier to determine on a local view, then the safety of a consensus protocol which has to do with the decisions at different nodes make across the network and so I think it's just easier to reason about so and if we have this result, which you know I'm going to show that we do or I may I'm sure somewhere that we do.

C

For you know, if I don't show you today that, if nodes calculate that their estimates are safe, then they both will have the same estimate so, and this is actually going to guarantee our direct decision rule. Basically, nodes are going to calculate it. The rest of it is safe and if it's safe, then they can decide, and that's going to be like the correct by construction approach, where the the the decisions are all going to be the same.

C

Ie we're gonna have 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, like it's cool for me, to make this decision, because I know that that there'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, this is the main data structure that we're gonna be dealing with these bets.

C

Are they have three things, an estimate, a justification and a sender. The estimate is basically a bit in this case covers doing binary consensus. The justification is a set of bets or the empty set, and the 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 because ties aren't annoying edge case. So we have this. Other data structure called a view.

C

It a view is just a set of bits, so we have bet which are have estimates justifications which are sets of bets and senders. We have.

C

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 and it's worth noting that the bet structure is a dag and you can represent it kind of like this, where I'm going to line up validators right.

C

So so 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 bats, one with s0, 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.

C

Sometimes sometimes there could be new stuff in terms of like this data structure that we just have that or that I just define and which basically is like the model. Not everything is going to sit on. So um a bet is independency of another bet if it's in the justification or if it's in the dependency of anything in the justification, so the recursive definition, but there's a really pretty picture.

C

The read bet is in the dependency of the blue bets, basically because it is upstream from them in the end, these arrows, 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.

C

So basically they represent kind of a bet made with the justification that like ignored the fact that they previously had made a bet, there's no way to make two bets and have neither them be in the adjusting 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. So here are some examples of quotations. The colored bets are equivocations the two red ones. You know the two blue ones. They don't include each other in the dependencies. There's no like there's.

C

No, you know arrow saying that the one knows about the zero or that, like the one up, there does better the other one. So these are equivocations and equivocations correspond to something important when we put when we talk about Byzantine faults and kind of our ideal adversary. So the latest bets 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 bets.

C

They don't have any nodes with an arrow point pointing out so there's no arrows pointing out of these out of these bets into another bet from the same validator. So there so like those two bets on the left. Are the latest nodes latest bets from validator? One note that they're an equivocation validator to validator 3 also have some latest bets there. It kind of has an intuitive thing rights like the latest bet that we've observed from them, and we have these like little arrows to help us find the way so in pet is invalid.

C

If the estimate of the bed 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. You know every validator has a weight. Every validator has the latest bet and I'm going to say: okay, look if these validators have a estimate one and the latest bet those validators have enough zero, but these ones have more weight than like. My bet.

C

Having all that stuff in is desiccation 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 only valid bets around who are always going to choose them the maximum weight estimates. So then we have these definition of Byzantine validator. So this is something where normally people would define Byzantine validator Oh.

C

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, 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.

C

If you're not following the protocol, then your Byzantine, because we haven't even constructed the protocol yet right so we're gonna say, is that no Tsar 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, no, that's always producing valid bets or you've done some craziness and you're lying basically you're like telling what some node one thing telling another node, the other thing or you're producing invalid bets and those are coming.

C

We can identify in our bet structure and is like bad right 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 node has two latest bets, you just like drop their way to zero. If I know I made an invalid bet, you drop their way to zero.

C

Here are some invalid bets they're, just like not majority estimates given the weights that were observed below I'm just going to power through, because we've got a lot to cover. So basically, an estimate is safe in view.

C

Basically, if there there is no possible future of on of the view, which means like additions of bets, that view where the estimate is changed 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. Ie, like any causally, consistent sequence for of message passing, is cool.

C

There is other the estimate is the same, or there is no possible future where the sum is different, then it's that it's safe, but this is kind of not a constructive definition, so that won't do for our correct by construction kind of thing when you do instead is calculate safety by producing this adversary that tries to kind of make the network condition happen.

C

That changes the estimate, so here's an example of an adversary that, like shows this bet from from validator 3 to validator, in order to induce validator 2 to produce a new bet, because now I validate or to seize a different max weight estimate and that changes the overall mass weight estimate that we see from the the view as a whole so like that first view is like not safe and and basically we have a slight issue when we try to calculate this this this adversary, because we have side effects.

C

So so what we're gonna 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 go with and if they don't, the attacker will ignore. So this attacker that's kind of stronger than normal. So if this attacker fails, then definitely your thing is safe.

C

So basically the way that to can do the construct construction for a that ideal. The ideal attacker for asynchronous network is basically to only allow bets that have the the the don't have the victim estimate in there to travel and only allow bets that don't have the Vechten. The victim is an estimate there to be made so the adversary, just like stops all bets that disagree with his estimate from traveling across the network and like that's the kind of ideal network adversary for an asynchronous Network.

C

And then the decision rule in a singer's network is oh, once I calculate that might estimate can't change under this ideal adversary, I decide and that's correct by construction, because you know that the there is no way for to knows in the same in it in the network to disagree about whether there's a possible future of that network, where they have different estimates because they're there, because they're both modeling. This asynchronous network is a little bit of a subtle argument.

C

Basically, because 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. The one of the estimates to the other, but we're really running out of time so with equivocation.

C

We also do this thing where only the bets with the wrong the wrong hasn't fly around, but you also get some additional flexibility about where you can add bets, because if you don't all have to only add them in 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.

C

So, 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, senses ie when to make this final decision right. So it's very related to like finality in that whole discussion right, so I'm gonna try to quickly relate this to existing research.

C

Basically, the only stuff that I've talked about here has been expose kind of safety measure where we don't actually look, though you didn't talk about liveness at all, and so we don't violate FL paint possibility at all.

C

We have Byzantine fault, tolerance and safety and asynchronicity we don't have liveness, that's great, and basically we can see why we don't have liveness because like if we or 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 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.

C

It we can actually become safe from a position where we aren't safe in a way, that's approvable and so like we haven't violated FLP at all, so basically we, it was cool that we did it only this expose measurement of safety rather than reasoning about liveness at all, because it's not only not usually what happens so like there exist views in this ex-post world, where you have extremely high levels of fault.

C

Tolerance where, like all the one note would be faulty in your estimates, still won't change because, like any of these faults will be detected by everyone and those weights of those knows 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. So it's not live.

C

We don't actually have a guarantee that we'll get there from a point where we don't have it. This is like point where we're safe, so I think it provides kind of an interesting view into business default, tolerance in general and I hope. We can extend this research into liveness and also to find everything in terms of the same data 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.

C

So what I just said? Liveness I want to make a conservative attacker that minimizes the amount of equivocation that needs to happen by weight. This will improve the combinational complexity of stopping in in a Byzantine fault context. We need to move from because that's not a bit two cassettes on the EVM. We need to do validated rotation, we to add economics, so we can look around in public and we need to do like complexity and performance. Optimization and, basically, you know improve. Like the theory.

C

The specifications documentation the implementation by the way I do have an implementation of the correct by correct by construction thing, I mean mostly I, have the ideal adversary implemented in like Python for equivocating faults. So, like that's, cool, an asynchronous Network, my time is almost up and my slides are done. Thanks for listening, excellent.

A

Thank you, lad good job.