Validation, Equivocation and Byzantine Fault Tolerance

Transcript

hey everyone um so i'm gonna give a talk today short 20-minute talk about validation equivocation and byzantine fault tolerance it's really a talk about how to avoid doing byzantine fault tolerance in certain certain contexts um byzantine fault tolerance analysis is a kind of analysis of distributed systems when you know you have an assumption that some of the terms might be corrupted in some unknown way so i'm going to give a talk um basically about my approach to doing byzantine fault tolerance that i've developed in cbc casper for over the last years um and um it was originally planned on being

highly technical talk and now i made it into a tech intuition talk and so it's going to be somewhat technical but i'm going to try to keep it about the intuitions and i'm not going to write almost any math so um the kind of so hopefully by the end of this talk you'll have an idea of how you can avoid doing byzantine fault tolerance um when you're analyzing distributed systems so first thing i want to talk about is state transition systems um i'm going to build up a kind of language in which we can talk about validation and equivocation in terms of state transition systems so let's start with um just a normal traditional kind of state transition system

so in a normal state transition system we have some kind of set of states um some kind of set of set of states and and i'm going to call them here i'm going a little hat which means they're they're protostates so these are this is like our our big set of states this is kind of where the protocols live they have states and then there's something called the state transition function so denote here is tau and it takes states and gives you states so this is a state transition function and you can imagine inside this set we have all sorts of different states and then each state

has a transition let's use the arrow tool each state has a transition to each to another state um and these this is basically just given by the um this transition function so the transition function tells us kind of which states map to which states and so we can kind of understand in some way um any a trace of a protocol in terms of in terms of the in terms of the of of kind of following these arrows so

like this is a partial trace of the protocol this is a partial trace of the protocol or of this transition system and and so but not we're not going to be really interested in all traces we're only going to be interested in in some of them um specifically some states are going to be initial states so i'm going to circle the initial states here in blue some of them are initial states and we're only really concerned about traces that start in the initial states and so and so like normally we're going to consider you know for example this trace might be a protocol trace and this trace is a protocol trace these are kind of um the execution of the protocol starting from

the initial states so so so given this this state the set s hat of states we have a transition function that maps all the states to one another inside the inside here and then um and then we can think about the initial states and then which and then which which of these um which traces start from the initial states so that's all good um but the problem here is that this is a deterministic system you know every point only has one arrow going out of it um and and that and and that won't really do us too good

because uh oh sorry i did scrub the drawing there because i had two arrows out of that point to actually get more than one arrow we this function won't do um and we're gonna need something else um so now i'm going to tell you a little bit about a labeled state transition system where instead of just having a state mapping to a state we have a label and a state mapping to a state so this is a labeled transition system it's kind of similar to the previous one only now we get to have the option of having two arrows from a particular out of a particular state um this kind of corresponds to a non-deterministic transition you know you can kind of go from one of these states to either one of

those two and they will maybe have a different label this one maybe has like a label l1 and the other one maybe has a label l2 um anyways my fault is a little big here but you can kind of get it um basically with one function you know you map states to states and you only get one state for every state with a label we get for each label we'll have a state um from each state and then it might be possible from some states to have more than a couple of future states based on this um this is this kind of label

um so the the label for one of these one of these transitions will be different than the other so that's good now we can express kind of non-deterministic protocols um still you know we're kind of assuming that there are some initial states uh and then we talk about traces starting from the initial states and now we have kind of choices we can go kind of this way or we can go this way uh all from the same initial state whereas previously we're kind of stuck on a single path from any initial state so that's cool so so so this is this is neat i mean we can use label say transition systems to talk about all sorts of different computational phenomena um and you know it's a it's a it's a pretty cool system however um

you know there's it's all very serial there's no currency there's only one program term here and this in this state and so we'd like actually to have something a little bit a little bit more um specifically we want to have messages being sent and received so that we can have a bunch of these running in parallel kind of talking to each other so i'm going to um get to find something else now here so so so rather than just a label transition system now i'm going to i'm going to talk about a labeled transition system with messages so so our transitions now we're going to have a label still and a state like before but now we also

have a message and then we also will produce a state and a message um with with each one of these uh transitions so the transition rather than being um just labeled with a label they're also going to have a couple of other labels so every transition is going to have um um basically uh so let me try let me try to make this text over here so you have a label

and then a message in and a message out great so every state so every transition is not only going to have a label as before but it also has a message that comes in and a message that comes out so this is cool because um it lets us understand not only states but also this somehow we have this notion of messages now and so what i'm going to try to do now is we're going to now we're going to have we're going to consider multiple of these kinds of transition

systems in kind of composed so now we might this is getting closer to what we might understand in a distributed system so we have initial states and transitions for each of the components and then the components have these messages that they can receive and send with with certain transitions by the way i want to mention that these messages are optional so you know not you could imagine that not every message not every transition receives a message and not every transition sends a message but you know some of them do and then you can imagine that the messages that are received actually um can't be just any message uh but they have to actually have been produced by one of these terms so you know you can't just receive any

message you can't just transition as with the label label transition on any label that we want to transition on this delay on this on this arrow here we actually have to receive the message m so in this in this setup we have basically in some way you can imagine a a very loose but i mean and now i'm stating it kind of loosely but actually when we do this formula it's very tight but a very loose kind of description of distributed systems in terms of different state transitions available to different nodes um and and and we kind of will observe that in some way these executions won't be independent possibly because

they might receive messages from each other so for example uh let me just create this with a line perhaps um so maybe you know perhaps maybe this message here is received here maybe a message is sent on that transition and is received in this transition and therefore kind of allows that transition to take place so and then you know similarly maybe it's also it's also it also is received here by this by this node um so so so so basically you know this kind of describes a

distributed system where we have these components with known states and messages and labels that we have but when we're talking about byzantine fault tolerance we kind of have another case we have a case where basically we have some other terms maybe say these two terms here rather than being the terms that we would kind of expect um we have we have we have um we have kind of unknown terms here we basically have some some terms here which we don't know anything about actually we have we have we have these these terms which have unknown states produce unknown messages have undefined

behavior and these are kind of called byzantine byzantine nodes and byzantine nodes are um they're undescribable you know you can't really say what a byzantine is doing because it can be doing anything that's kind of the definition of the business you know it's untyped and and and similarly or interestingly byzantine nodes can send messages to correct nodes and and change the way that they transition and so now all of a sudden our analysis of how we'll send those to each other and all of a sudden the the analysis of how of how these um how the protocol evolves starts to become a little more

interesting and questionable because you know in some way you can imagine this these byzantines can send any message and so the amount of transitions that are available here are much greater than previously where we only allowed say only messages that were produced by these other terms so how do we deal with this what is what are we going to do uh to understand the behavior of our protocol in the context of these unknown terms that can basically do and send anything um well i'll tell you what we're going to do we're going to introduce this additional kind of thing on top of this on top of this transition system um

which which is which is a validity oops a validity condition so so a validity condition you can think of as a subset of l cross s hat cross m so this is basically it says oh look so the idea with the validity condition is um before transitioning on a particular um before before transitioning at a particular particular arrow we have to check the validity condition for the label state and message that were we're transitioning about transition to uh because it'll be kind of invalid um to to to make that transition otherwise so we

we augment our transition system with this additional thing called the validity condition or um you know the uh coloring on the transitions for which ones are valid so then we go back here and now rather than um you know now we're kind of assuming we have this valid thing um it's not going to be the case that the byzantine nodes can i mean they can still send any message but it might be that sending that for some of them it's invalid actually for the protocol following node to receive and so for those messages um the for those messages the ones that are invalid to receive um it's gonna be the the byzantine node

isn't going to be able to use that message to make another transition so um so then we're going to do another trick actually um so let's imagine back that imagine that we were here where we were initially where we were we're not considering any byzantine nodes and only considering these protocol following nodes um what we're gonna what we can do is we can think about okay what traces here are actually a protocol like some of them are going to be protocol in the sense that they are reached from the initial states by these terms when they're composed with other with these other correct terms of them so some of these traces are going to be reachable

and and when they're reachable we call them protocol so they're start from initial states and you can get to it by protocol transitions that are not just valid but um so originally we weren't talking about bloody but now we are so we're gonna you know these ones by virtually reachable are valid um but they're they're reachable specifically using messages received from these other terms and so and so we can look at these traces and say okay these are somehow the ones that we should be we should be reaching um but which and so we can say like let's try to make our our valid condition only allow our terms to reach these states and and then what that will do is it'll

restrict the ability of the byzantine nodes to push our protocol nodes off of these paths so our protocol nodes will specifically only ever transition on valid paths and so these big bad unknown byzantine nodes will will not be able to push our terms off of the valid traces specifically because you know the term will when receiving a message that isn't that it isn't possible for it to receive in a normal execution will just reject that message because it's not valid so you know this kind of corresponds pretty normally to the notion of validation that we have in the

blockchain space like you receive a block you like check if it's a valid block and if it's not a valid block you don't transition with that block pretty simple but somehow what i'm pointing out here is that this is going to restrict the way that the byzantine nodes can actually cause these terms to transition um great and so and so and so in some way this is the beginning of our strategy for [Music] avoiding byzantine fault tolerance analysis because now although these un these undefined terms can send any message over only valid messages will cause transitions and as a result is almost as if byzantine nodes are restricted to only

sending valid messages so that's that's good and we might feel like we're done but actually there's there's this interesting thing called equivocation um where um this byzantine node might send two messages here one to one term and one to the other m1 and m2 which although they're each valid messages um there's no trace for a correct node that produces both m1 and m2 so for example m1 might be a note a a message that says hey i'm deciding on zero and m2 might be a message that says hey i'm deciding on one

these messages both kind of have to exist or you know consensus protocol in some way um and it's pos so they're valid and it has to be possible for notes to receive them but um but the the thing that will happen here is that one of these nodes will go down one transition and the other one will go down a different one in a way that wouldn't be possible actually normally and in the original trace that we were talking about so it may be in the previous system that the the terms always went the same trace because they're all kind of coordinating together and there wasn't this equivocation and so um the traces that they took were kind of consistent with each other

you know the one node decides zero the other one should decide zero two but in the context of this kind of equivocation behavior it might be that even though there's only valid messages these terms can rest can can basically end up having inconsistent decisions or traces that don't behave in the same way as they do without byzantine notes um because basically you know the these these messages that they're receiving these equivocations are valid messages and therefore they get through our validation filter but it somehow impossible in a normal protocol execution for this doesn't for a correct note to send both these messages m1 and m2

they're kind of you know uh they're they're kind of inconsistent messages i don't know how to describe that they're kind of inconsistent messages they can't really both be sent from the same trace and and and that kind of makes it gives it it makes it quite problematic for us uh because you know we were trying to restrict the traces in order in a way that stops um these protocol following nodes from exhibiting behavior that we um where we have to consider this byzantine behavior um but now actually we do we have actually restricted byzantinos quite a lot already by having them uh only send valid

messages and so we have i kind of came up with this neat trick which kind of lets me just forget entirely about these byzantine nodes and instead consider just these kinds of follow correct protocol following notes by kind of bending a little bit one of the assumptions that i made earlier implicitly i kind of made this assumption that um to receive a message in one of these terms it had to have been sent by one of these previous terms and or by one of these other terms previously in the same execution but

actually it turns out that that assumption is is it if we weaken that assumption if we if we if we get rid of the assumption that the messages that messages that are received by these terms had to have been previously sent by these terms and instead we can it too had to have been sent by one of these nodes in some trace not necessarily this trace but in any trace of the protocol that's possible um not necessarily the one that we've experienced here but one that's kind of you could think in an alternate universe like initially you can imagine all these star all these terms start with these initial states and there's different ways that it could evolve and one of those paths and one is produced and then the other

m2 is produced well if we just allow m2 to be produced in the path that includes m1 then we're kind of exactly allowing this equivocation behavior and so the the story here basically is that by allowing messages to be received not just from within the execution trace of this composite protocol but also from between execution traces of the same protocol we can kind of introduce all of these equivocations all of these all of this kind of bad behavior that the byzantine node was able to exhibit to correct nodes

but which um uh it kind of got through the validation filter um it is now going to be expressed in just in terms of these well-defined terms with this additional weird property that they get to send traces to each other sorry they get to send messages to each other on traces that are on different timelines so if in one timeline you know we decide zero and another timeline we decide one when when i'm composing them in this new special way i'm going to allow messages to be received on the first timeline even if they were just sent on the second timeline um so so this kind of trick it basically allows me to receive all possible messages from all possible

terms not just the ones that were experienced on this trace but ones that were experienced on any trace and so then so then similarly to before how we said okay let's consider these six things together and what terms they touch and then we kind of make those validating so we make the protocol validating by restricting the validity condition to make it invalid to transition to any term that isn't reached by these six terms when they're together now what we're gonna do is something slightly more basically exactly the same but slightly different because uh rather than assuming that messages that have been received have to have

been sent we can receive messages that weren't even sent in this trace but were sent in some other parallel universe but also by these six terms and so and so we can do exactly the same thing with a different message model that allows these equivocations to be sent kind of between timelines and and and do exactly the same process of considering only the traces that um [Music] considering only the traces that um are reachable in this composition of these terms where they're allowed to send messages to each other also from across timelines and so what that will let us do is is is give it'll give us the

all these traces um for for the for these terms that are that are valid and those traces are going to include all the everything that can be reached by receiving equivocation um and so um sorry one second um yeah and so and so and so basically um um what this so and so basically what this what this is gonna let's do is we're gonna be able to see all the traces that are a result of receiving all equivocations in all possible ways and