Liveness in CBC Casper

Transcript

I guess you know coronavirus combined with like boring tech topics and only one hour only one hour long you know you can always catch me after for more detail because we don't have that much time to go into it so today we're gonna talk about CBC Casper liveness more you know liveness in CBC Casper CBC Casper is a consensus protocol that I've been working on for better part of like three or four years and today is like the first time that I'm really sharing in public in detail the basic strategy and

philosophy behind the CBC Casper liveness proposals or solutions at least behind my favorite CBC Casper liveness solutions has been a number of these solutions that aren't I'm not sharing today I'm just sharing specifically like my favorite liveness solutions here's kind of roughly the outline of the talk did you have a future working conclusion section that's not mentioned here basically I'm gonna talk a little bit about liveness and consensus protocols and like what is it that what is this problem that we're trying to solve or that we've solved and kind of how is it defined how would you prove such a thing and then I'm gonna give CBC Casper aliveness kind of live series Casper

specification in synchrony and in partial synchrony and with any luck we'll be able to get through all of it and they're both very similar and so probably I'll rush through the second one if we don't if we don't have that much time so let's talk about liveness what is liveness well liveness basically refers to something eventually happening in a consensus protocol this something is a decision so this protocol is live if it eventually makes a decision in the blockchain world that means that it eventually finalizes a new

in binary consensus protocol it means that it eventually decides on a bit and decisions in these contact and the consent of all contexts are kind of at least I'm assuming and are assumed here to be kind of final and so the only real requirement for liveness is that in all protocol execution traces there is a finite position in which there is a decision so if you consider every possible protocol execution trace every single way that the protocol could evolve and for every single one there's an index in that trace where there's a decision and then it's live and

specifically I'm not talking about incomplete protocol execution traces specific complete ones so a complete protocol execution trace has either two ways that they can look either as an infinite trace or it terminates in a state with no transitions available from it so complete protocol execution traces are like protocol occlusion traces that have either that are either kind of infinite or terminating so if you look at a protocols complete traces if every single one of them at a finite index has a decision then it's live that's like the definition of liveness in our in our context here empty slide just in case hopefully there wasn't anything on there so basically if there's a single trace

without a decision then the protocol is not live so live this is is really strong the property talks about every single protocol execution trace even a single counter example will kind of throw a wrench in your gears so this is key theorem it called a Filipina possibility that shows that for deterministic or non probabilistic non-deterministic consensus protocols it's impossible to have non-trivial ad consistency in liveness in an asynchronous network with a single faulty node this is kind of like a super-famous impossibility result in consensus and people were basically if people fall out like oh the consensus is

impossible this is kind of like the way it was branded just to talk a little bit about these terms non-trivial ad means that the consensus protocol can decide on mutually exclusive outcomes so for binary consensus protocol that means like there is a trace where it decides zero and there is a trace where it decides one consistency means that in a single trace the different nodes all make the same decision or that they don't make inconsistent decisions in the single trace so it's impossible according to this theorem to have all three non triviality consistency and liveness and and in an asynchronous network

what that means is basically that any message that's sent he's eventually received so if you look at a complete trace any message that sent you know has been received but if you think I'd say a partial trace and there's a message that's been sent but hasn't been received yet you know in an asynchronous Network you're guaranteed that it'll eventually be received although you may not know you know in what amount of steps of the execution so in a complete network so in an asynchronous network in a complete trace all the sent messages are received and there's no additional kind of constraints on the order in which the messages are received or in the context of faulty nodes if they are

sent and received between correct nodes so if they're sent and received between nodes that aren't synchronization faulty then what that means is that in a complete execution trace the there will be a receive for every cent so CBC caspere's constructed to be safe in an asynchronous network with limited number of faults and so and because of the kind of non probabilistic non-deterministic nature of the protocol this means that we can't also be live in a synchrony this is what kind of a possibility means and then what we're gonna do instead is we're gonna follow a very similar design philosophy that we did for the original construction of CUC Kasper for a consistency to construct to

validate our strategies that are live in synchronous and partially synchronous networks where we don't have this impossibility result applying and we'll kind of get to see the kind of trick that we're able to do here that's impossible to do in an asynchronous Network so you know that's liveness that's the context you know like we can't really achieve live in us any synchrony so we're gonna do it in partial synchrony and synchrony which I'll describe in a moment so CBC Kasper liveness in synchrony this is like kind of like the monster section where I'm hoping to share all the kind of or you know the kind of key simple ideas that

I'm using to construct liven strategies so first we're gonna consider CBC Casper aliveness in synchrony with no faulty validators or what this specifically means for us is no synchronization faulty validators so and we kind of will define this protocol that's live in this context where there's no faults in a synchronous network so what is the synchronous network well firstly - to model this what we're gonna do is we're gonna assume that nodes have a clock the validator specifically their state has a a thing that like normally hasn't been in like traditional basic CBC Kaspar

specs but that's like a number that corresponds to the clock and there's a special state transition called tick that updates that clock so all validators have clocks and all validators have transitions that take the clock in synchronous network if a message is sent and like this particular definition of a synchronous network that I'm using here if a message is sent at time T then it's going to be received by the other validators before they take tit T plus n so by time T plus n they're going to receive these messages and here I'm assuming that no validators are faulty and so like if there's a send you

know there's going to be received by the other validators before t + n this is kind of the assumption so basically we're only considering protocol execution traces that have this property that if there's a send of time T's received by all the Valladares by people sent and specifically we're assuming here that n is a number that's known to the validators like it's it's allowed to define the validator terms in terms of this number n and kind of without loss of generality for our particular solution and for ease of simplicity we're going to assume that n is 1 so if a message is sent at time T it'll also be received before the end of time T for other validators so what kind

of separating time into these slots that are all like one time step deep this is just kind of for a conceptual simplicity if we you know let n be just some known constant it would it would work out in similar way only we'd have like number the slots differently than we're numbering the time and so this kind of ends up giving roughly the same solution so first so I'm just gonna assume that n is 1 and have this really tight synchrony bound so we can just um try to solve this lattice problem in the simplest possible case we also need something called a plan this plan is

gonna have an assignment of validator names to Heights or to time slots basically it says like these validator should make messages at these times those validator should make messages at these times and this this plan has certain properties there is some height in the plan don't have a laser pointer mmm I kind of do yeah so there's a height of the plan where the set of validators is odd which means that there is no way to split this validator set up into two evenly weighted sets and there's a and every suffix of the plan contains all validators so if I have these two properties you know well the plan the plan is like assumed to have

these two properties and I'm gonna use these properties to show liveness of like this protocol just haven't hunters in fully defined yet but we're getting there and here basically is validators are gonna make a cbc Kaspar protocol message whenever the plan says it's their time to do so so if it's time 20 and the validator set a sign for time 20 includes my name then I as a validator will produce a message at time 20 before I take the time 21 like that's the strategy real simple but you know even even with this strategy a really simple strategy you think it'd be really easy to prove liveness but in

fact if you want to really like prove it in detail it's still kind of a lot of work so here is kind of how kind of how it's gonna go we're gonna assume that the validator said it's finite this isn't always something we do in CBC cash Berlin but it kind of I mean it is in practice and for liveness is actually necessary because if used in the developer said it's finite then we can prove this theorem which says that every validators clock eventually ticks basically and we do this by showing that all possible state transitions except for that particular clock tick that we're interested in will be exhausted so we'll get to a point where

we have no possible transitions left except for the transition that takes the clock for this validator I and and that kind of proves and forces us to take validator I so let's just like suppose that we have a whole bunch of validators and we want to prove that one of the validator i's clock will eventually tick then what we're going to consider is the state transitions of the overall system and we'll try to do all of the other transitions in an attempt to never do this tick transition and what happens is basically you know all validators have to wait for validator I to make a message and the next time validator shows up in the plan for them to go beyond that point in the plan so all of

all the validators are kind of at some point gonna be waiting for validator I to produce a message and you know I at that point you know there might still be some messages that have been received yet and we could we could propagate all those around but eventually all the messages that haven't been received by any of the validator so far you know except for the messages that validate or I has to take forward to receive been received and so you kind of exhaust all the sent messages all of the you know all all the sends all the receives all of the clock ticks until at some point we're basically gonna get to a point where everyone is block on validator I because every one to tick past a place where validator is in the

plan needs to receive this message from validator I'm and validator I maybe isn't even at that point in the plan yet but to get there they're gonna have to take their clock so you can actually have this really detailed argument about to just show that every validators clock eventually takes in a synchronous network where no one is faulting and it's like you know actually quite laborious to show that you know usually we take it for granted furthermore you know everybody Alan is Clark eventually ticks and so everyone's kind of eventually always ticking and every validator has a next message in the plan and that's my definition of the

plan which has a every validator set in every suffix and so eventually each validator makes their next plan message and you know each validator eventually receives this message because everyone's clock eventually takes past that point and as soon as you take past that point you have to receive the message it so basically every validator eventually sends and receives the messages that are planned for and so any prefix of the plan is eventually executed because every message is going to be eventually sent and eventually received and

everyone's going to eventually move through this process of going executing this plan and so any prefix any length the prefix of the plan is going to be eventually executed now it's possible that we have a tie at the start like half zeros half ones and then like the tie continues but there's going to be some height by definition of our plan that's odd where it's impossible to have a time and at that point the tie will be broken and at all future Heights at all future heights the messages will have the same estimate and then since every validator is in every suffix of the plan what's going to happen is if you do enough of a prefix you'll get all the validators set repeating enough times to get a decision on this value so

and that kind of satisfies our decision criteria finality detector safety Oracle construction kind of needs to see everyone agree and have like layers of agreement without any disagreeing messages in between and so kind of there it is though now like basically by showing that I have an arbitrary section of this plan and you know and eventually it gets passed this tie and then I have it like an arbitrary period out for that where I can have like an arbitrary number of layers I can just in that that's kind of sufficient to show that there's a decision so this is a rogue slide excuse me

so that was that that was great so that so that was how we're gonna you know it's like a simple strategy for doing it for achieving and proving liveness in a synchronous network with no faulty validators relatively simple you know fixed plan with certain properties and then making the validator send messages when it's their turn to do so in the plan the plan has properties that like guarantee that all the validators show up over and over again and that ties are broken so that they're showing up over and over again agreeing later so that was great and even you know you might think too easy although if you really think about it like the the proofs the proof aliveness is still kind of

laborious you kind of have to show that all the messages in the plan are sent and received by everyone and therefore that the whole plan is executed or at least at an arbitrary point eventually so you know liveness in general is actually quite a laborious thing to reason about and to specify to to work with basically because you have to make this kind of argument that you run out of options except for progressing so now I'm gonna move into talking about synchronous faults and a synchronous network or like synchronization faults in a synchronous in this ignorance Network and specifically we're gonna be detecting

these faults because this forms the basis of who's gonna form the basis of our liveness strategy in the context of faults so let's first get a definition of what it means to have a limited number of synchrony faults in or a limited living limited number of synchronization faulty validators in this consensus protocol basically we're gonna assume that the amount of faulty validators is limited by some number t sr nor f of weight of validators and these are the ones that are kind of we're considering some less

than f of them by weight are gonna be faulty so what does this mean well basically messages sent by non synchronization faulty validators you know time T are guaranteed to be received by time T plus n but between singers agent faulty validators and other validators they may not be received by time T plus n they may not be received at all they weren't be received later so within between non-singer ization faulting validators we have the normal synchronization conditions between a synchronization quality validator and another one we may not have this message arrive before T plus n so if you look at a complete protocol execution trace you

can actually see which pairs of validators are synchronization faulty you can like see like you know who's sent a message that didn't arrive with an N of the time it was sent and and so you the complete execution traces and look at pairs of validators and see actually by inspecting the trace whether or not there was a synchronization Fault between those pairs so basically we can draw a graph between validators who go with nodes as validated names and edges between them for validators who haven't experienced through the execution trace

any synchronization faults so this kind of graph I call a connectivity graph it's it's kind of it it's it draws the reliable connections between the validators and so kind of if we have a limited number of crash faults or these synchronization faults then what's gonna happen is like there's gonna be some less than F total weight number of nodes that we can remove from this graph to reveal a totally connected graph like a fully connected graph and this fully connected graph could we could imagine be the graph of non synchronization faulty validators who did that each other won't ever have synchronization faults and so basically if you look at a

complete protocol execution trace and construct the connectivity graph and the connectivity graph has the property that you can remove less than F weight of nodes from them and B were left without a fully connected graph then that trace is it protocol excision trace with limited synchronisation faults specifically less than F weight of faulty validators so by looking at the connectivity graph from execution trace we can tell whether or not a particular execution trace is this satisfies this definition of having less than F faulty weight of validators you know and this may not necessarily be efficient to do and we don't actually need to do this but we need to kind of but this is the

way that I'm expressing an understanding the assumption that there are limited number of faulty weight validators basically that means is that at least for total weight minus F for the validators there is a fully connected click meaning that the validators in that click haven't ever had a synchronization failure between them and in a synchronous network that's you know mm reasonable kind of assertion so this is so basically I'm gonna define this synchronous network as basically having execution traces with this connectivity graph you know has this property that if I remove less than fo

nodes i can left with a fully connected one like that's the definition of a synchronous network with limited faults in my context and there's there's like really good reasons why I do this instead of having say for example on a validator that I consider to have Byzantine behavior but you know we can talk about type fault tolerance analysis versus Byzantine fault tolerance analysis a little later so so now we're going to give a protocol that in some way learns this connectivity graph own basically it's a really it's a really

simple protocol um basically every validator when they produce a message how commits to the next time they'll produce a message it's called the next message time sometimes just nmt for short and it has to be later than the current time that they're sending a message from so nmt is like a next message time is that it's a commitment for when you'll send a message in the future and this is going to be used by validators to tell whether or not there's been a synchronization fault okay if you tell me you're gonna make a messages slot 10 and I don't hear from you by the end of slot 10 then I'm you know then we've had some kind of synchronization fault between us and so

each each validator can maintain in their protocol state of a fault attribution map or basically they like consider their peers as faulty or not based on whether or not they've conceived had a synchronization failure with them and if you don't receive a message from a validator by the end of their next message time then you mark them as faulty and the next message time is unconstrained except for that has to be in the future and just from this kind of construction mmm we're gonna get some pretty kind of powerful stuff so notably if you take the if you if you take a protocol state of a validator you

can tell who they've marked faulty and if you look at the latest message and their latest message you can also tell with a mark faulty so if you look at the latest messages from a bunch of validators you guys to kind of build the connectivity graph for the network by seeing which pairs of validators haven't marked each other as faulty so and then this is key theorem basically we're in a synchronous network of limited phones then these fault attributions eventually stop changing so in all protocol executions there is an index after which point the false attributions stopped changing where basically you know all the faults that have been expressed all the faults that will be expressed have been expressed could be because all the

possible thoughts have been expressed but it could be because just the attacker is gonna stop at that point only having shown certain faults but no matter what in all protocol execution traces eventually the phone contributions stopped changing and this is kind of like a cornerstone kind of thing basically because what this means is that or or let me just restate this kind of for the connectivity graph you know the connect just like the fault attributions stop changing the connectivity graph also stops changing because you know a faulty node can on

any point say disconnects from I know they're connected to but they can never reconnect and so the they're kind of spending and never getting back their budget of faults to display and so at the end of the day eventually the connectivity graph and fault attributions become stable so for this really simple next message time protocol with font attribution very very simple protocol we have this property that's not it's not liveness but it says that eventually if you go far enough than these execution traces we're gonna have the connectivity graph and fault attributions stop changing so that's like an intermediate protocol which we're gonna use in order to come up with

a protocol that's live in synchrony for CBC Kasper but since we're doing pretty good on time I guess I'll stop stop for any questions if anything is not clear so so far I've covered two very simple protocols one of them you have like a validators assigned to particular time slots this and that's when they make their messages and they all make it according to plan and there then we have liveness because the plan at some point has a tie breaker and then you have this other protocol which is this next message time protocol where validators commits to when they're gonna make new messages and mark each other is faulty when they don't receive messages from each other in time and where we have this property that eventually the fault attribution the connectivity graph stopped changing hopefully that's pretty

clear really really simple protocols and here's kind of the link or like the kind of combining the pieces together to come up with a fault tolerant live liveness strategy basically you know it turns out that like a stable falls attribution or a stable connectivity graph is kind of similar in some ways to network without faults because along those edges where they're connected the synchronization faults don't occur eventually because eventually this thing is stable which means that eventually synchronization

faults stop occurring which means that's very similar to just a regular network with no faults but here maybe we can't really have a fixed plan because you know if we had a fixed plan then we might end up with like some an executable plan because like some validators that are relying on being our plan and are being faulty in so instead we have something called a planner what a planner does is it takes connectivity graph specifically the largest connected component of that connectivity graph and returns a plan for the validators in that connected component and it's similar to the plans that we discussed earlier only instead

of having I know I set somewhere we have to have an on-set in every suffix because now we don't really know at what point this plan will start being executed we know that eventually you know eventually we're gonna have magic happen but like it could be then at the start things don't get executed according to plan and so we need to have an odd set of validators later on and and and here's another additional requirement for the plan that kind of existed before but only implicitly that validators with adjacent positions in the plan are connected meaning that they haven't experienced each other have synchronization faults and you know once we get to the stable condition they won't in the future experience each

other as having execution faults sorry synchronization faults so three properties of the plan at this stage every every suffix contains every validator in the largest component of the connectivity graph every suffix contains an onset of validators and the validators in adjacent positions in the plan are connected in the connectivity graph so these three things together with the following constraint namely that sorry I'm only a second so so if yeah

okay so so basically if if your validator name appears in the future of the plan then your next message time has to be the time at which your name appears in the plan so basically like the next message time in the next message Time Protocol was completely unconstrained now here I'm insisting that if your name is in the plan going forward that you choose your next message time to be exactly you know the time at which you're included in the plan and what this basically does is it will kind of it serves as like a refinement of our next message time strategy that specifically says where people should put their message when people should make messages and specifically according to this plan so

basically the the next message time and false attribution system guarantees that we're gonna have an eventually stable connectivity graph and at that from that point on all non synchronization faulty validators will have the same connectivity graph because they're connected to each other and so they're and they're learning the connectivity graph like through the connections and so each one of these validators are learning the same connected component and so all the correct validators end up having the same plan because the planner takes just that connection component as input and so all the non simulation faulty validators learn the same connectivity graph or the same connected component of it and then they give that to the planner and they all come up with

same plan and you know after they make their next message they're gonna be synched up with this plan in a sense that like their next master time is going to be exactly in the same plan that they all have and basically and and you know adjacent validators in the plan are connected in the connectivity graph and so they're able to build messages on top of each other because basically otherwise there would be a synchronization fault which would be a contradiction of our assumption that we have this eventually stable or that we've reached the stability point of the connectivity graph and so you know if you assume that you've got to the stable connectivity graph point then what we're gonna guarantee and like pretty soon easily

like so you get to the stable connectivity we're at four point pretty soon after that all the correct validators or non single Asian faulty validators have the same connectivity graph local component which gives them the same plan and after their next message they're all synchronized to that plan and so after that point that plan is going to be executed exactly correctly for arbitrary suffix after that point and so you know or like a you know arbitrary prefix of the suffix after that point and so you know very very similar argument to the previous plan about why this is live right we have enough validators in this connected

component because it contains at least all the non synchronous faulty ones and eventually there's a nod height and eventually after that we get any number of layers of the validators see each other agree with the results of that tiebreaking and there it is that's basically the story about how you we can basically combine these two ideas of like you know a plan and this eventually stable connectivity graph in order to come up with something so that all of the non faulty validators can coordinate around exactly what they're what they're

planning to do and produce like this blockchain or this shape of messages which is guaranteed to image they have a decision and kind of all of this was basically is basically thanks to synchronous synchronicity which guarantees that correct validators are able to synchronize and and therefore that they're able to execute these plans like they're able to produce messages after each other so i hope that makes sense but again that's like recap next message time protocol leads to eventually stable connectivity graph the planner takes the largest kind of component of the connectivity graph and returns a plan all of the non-synchronous faulty validators again

we connect them to the same component so they have the same plan and the connectivity graph eventually is not going to change which means they'll be able to synchronize properly with the their adjacent nodes in this in the synchronization graph sorry in the connectivity graph which are exactly the nodes that they might be neighbors to in the plan so the plan is going to execute correctly because the plan is basically along the edges of the connectivity graph and so we get an arbitrary amount of the plan executing um but here rather than having the plan be like defined from the start the plan is defined as a function of the connectivity graph and that's ends up being fine because all of the correct validators are like the non

synchronous faulty ones observe the same connected component and that's basically because they're connected to each other and so they're they get to kind of learn that just by sharing with each other this information about their their their local area so I hope that's helped that's pretty clear hands up if this makes sense do you understand the protocol mmm you know pretty good alright and if you don't understand you have a question questions anyone we can do more questions later but uh this is all going way faster than I expected I have so many slides but they don't take

much time all right well I'm gonna assume that you're shy oh there we go the lights nice you guys are on spawn light now let's still no questions okay well we can move on for now and and if you have a question I'm not sure if I just didn't see your question okay well you can also hit me up later so live as impartial synchrony what is this gonna be like well it's it's kind of similar but partial synchrony isn't exactly like synchrony let's define Dove define it it's kind of similar you know messages sent by time sent at

time T will be received by the end of time T plus n but in the case instead of his end being known to the validators and is it's not known there's just no known bound on n that any of these protocol nodes could ever use and it's basically like not something that they get a touch the PERT that validators don't get to know and you know partial synchrony in some way is like is like synchrony with an unknown bound on the message delays so because it's unknown you you never really get to know when you receive a message out of too late if it's if it's above the bound or not so we have a

solution here with a couple of parameters we have an increasing sequence here I call F it's not the best name this is a sequence of waiting times so this validators gonna have the strategy of waiting longer and longer in order to you know do this trick that I'm gonna explain in a second so validator and then we keep this number or which is the number of times that we've received messages later than expected and basically f of n n IJ is going to be like the amount of time that validator I waits for validator J after their next message time so you know this this this increasing function is basically the

increasing delay times that you're waiting for to receive messages and the plan is a very similar to before and basically every suffix has every validator and an odd set of validators previously because we were able to perfectly execute everything in a synchronous network we only needed one on position but because now we want to have some kinds of faults at first we need to always have an odd one later so and and and furthermore I kind of have this constraint where every validator

kind of appears once for every time it appears once so like between every two instances of the same validator you know all of the other validators fall in between there or parallel like in between or in parallel and so so basically between every validator there's no validator appearing twice this is kind of a constraint that I have so that I can calculate my next message times well we will talk about that in a second maybe but the plan here is a little more restricted than before before I was like totally cool with like a validator producing 50 messages a hundred messages before any other

validator produces any now I'm kind of constricting it and saying like everyone will definitely make one while all the other Valladares making one and there was like another option that I had other than doing this which is like to give the validators the ability to submit multiple next message times but this it's a little bit technical so let's kind of skip that conversation for now so basically the next message time is gonna be chosen as the maximum of the next message times of the validators in the preceding step of the plan plus the amount of delay that you're waiting for them so imagine if I'm validator 12 and I'm waiting for validator you know nine ten and eleven and who are making

messages in the previous lot and they have next message time nine that's much time ten next much time 11 and I'm waiting for them you know and like twelve ten twelve nine and twelve eleven so like the next mister x plus the waiting times is like how much I'm gonna wait for individual one of them and the one that is latest it's basically how long I'm gonna wait for all of them so my next message time is going to be set up so that if everything goes well if people versus if I get messages before these timeouts that I'll be able to produce my message in the plan having received messages from everyone previously in the plan so the next message times are calculated using the

next message times of the validators previous in the previous slot at the plan and this is kind of why I wanted to have all of validators only have one message each for each message each because if you had like 50 messages there and I only know your one next message time I might not actually know the next message time that you have like right before my slot and so to calculate this next message time I'm using this restriction that I know the next message time of each of the validators right before my next slot and I know that because like there's no way from basically because there's no way for them to appear in the plan if so sorry I know that because I have their next message time basically I got a

little confused because it started think about the faulty context right now we weren't we don't have any faults and basically what happens is you you're gonna increment this number every time you fail to receive a message by the expected time and so what that'll do is it'll increase the amount of time you're waiting for messages from that validator you know from F NIJ to F and IJ plus one and so this incrementing of this of this of this number will increases the amount of time we're waiting for messages and so basically we can start to show liveness by basically showing that

eventually validators stop receiving messages beyond their waiting times so we basically stop having the synchronization failures that occur because of perfect synchrony there's basically two ways for these things to end one of them is this F at NIJ ends up being bigger than n which means that the amount of time that we're waiting is enough like there's this unknown bound and how long messages are gonna take and we're waiting more than that eventually because if it fails enough this is increasing a waiting time is eventually going to get over that fixed unknown constant N and at that point we're gonna be waiting long enough to receive these

messages or the other alternative is maybe we never get over that end but still nonetheless messages always arrive before our waiting time also possible also possible to have that and so you know but but um you know but there's no intermediate kind of thing where we keep always getting more delays and more more synchronization failures so eventually what happens is they're stopped being synchronization failures eventually validators that are waiting for messages from these other validators will receive them before they make their next message and without lead is to the correct execution of this plan for an arbitrary period of time and kind of very similar to before this is going to

lead to liveness because eventually hit this odd thing that breaks the tie and eventually you get any number of layers of agreement afterwards so you know it's partial synchrony with no faults is quite different than partial synchrony than synchrony with no faults because in synchrony with no faults were able to like perfectly reliably execute a plan in partial synchrony with no faults we can't really do that we're still gonna have faults in some extent even though we don't have faulty validators per se like we don't synchronization faulty validators we just have faults that occur because messages take longer than expected because we have no known bound on how long they might take so in

partial synchrony it was impossible for us at the get-go to prevent these synchronization failures even when all nodes are considered to be honest but in but but eventually we will have exactly the same scenario because eventually the art timeouts get long enough or we just stop receiving messages beyond them so that we don't have anymore synchronization faults and then and so basically partial synchrony eventually kind of feels like synchrony because eventually we wait long enough I mean because the main difference between purchasing creating synchrony is whether this bound on message arrival time is known great so I hope that makes sense and you know

I know you guys don't like questions so I'm gonna keep moving so so now basically we're talking or we're gonna doing be doing is analogous to the fault detection thing that we were doing before only now we're doing it in a partially synchronous increment network we can't really be certain when we receive a message later than this time out whether they are faulty the sender whether the center was faulty or whether just the partial synchrony bound is higher than our current estimate and waiting time there's no way to know and this is kind of the tricky thing about partial synchrony it's like we don't really know what happened Mike was the guy faulty or was the network just is

just what the network is like so but however if we do assume that our bound is high enough then we know for sure that it was a faulty validator like if we know that our bond is high enough then the only way that we could have missed this synchronization is with the faulty validator and so basically if you and if you stop receiving that if you don't receive a message in time from someone you're gonna increase your effort in so so your increased or your at the amount of time you wait and so eventually you're either gonna stop receiving messages from them that are

late or you're gonna increase above this bound but in either of those cases you basically are no longer having synchronization failure with that node if they're correct or if they're not if they're not faulting so basically what we basically have is the following eventually non synchronization faulty validators stop receiving each other's messages later than expected so well that's one thing right so so non synchronization and faulty validators eventually we'll just start always receiving each other's messages and so eventually you're going to get to a point where the only message

you're not receiving faithfully from our from non faulty validators because eventually all that all the sorry I meant from faulty validation so so eventually all the quote from all the correct validators everyone's receiving and sending messages in time and only the non correct validators are showing faults and then we could because it because because eventually this bound gets high enough or these messages stopping deliver stop being delivered late and so basically what we're gonna do is something like this we're gonna have previously we kind of had this as a state we're basically we were connected

to a validator and then we marked them as faulty whenever we had a synchronization failure and now now that this was kind of our synchronous fault detection scheme now because we don't really know when we marked them as faulty whether that was a correct thing to do we have to have this forgiveness it direction or basically we will unmarked them as faulty after some time and so here's kind of the strategy basically where we're gonna be connected with the validator we're gonna wait some amount and then if the message comes in too late where we marked them as faulty and the mention you forgive them and we wait longer every time we disconnect from them we wait longer and longer and then eventually you four correct validators quick Valladares will permanently stop

moving from connected to faulty because correct validators eventually this increased this time is going to be high enough or they just stopped sending delayed messages and so eventually for all correct validators you'll always stay in the left state there um you know it's question is there a question I thought I saw something sorry I can't hear you can you speak up a little bit comfortable slashing sorry one second

possibly a dumb question but after the the forgiveness period is over is there some sort of like punishment for slashing or something along those lines um so at this point this is just like a consensus protocol specification like there's no market design Center design stuff here but you know the fault detection model in some way was like you know conceived of in the context of proof of stake and you know I think it lends itself to this kind of thing you know so definitely like you know mmm I don't see it likely that being marked faulting is gonna be consequence of free however you know a kind of not really the scope of this talk this is just

about distributed systems consensus protocols I'm not really proof of stake so but so so the idea here is you know correct validators eventually start like staying the connected one only because you never you stop having accidental disconnections from them and then faulty validators can go back and forth between faulty and connected by just showing a fault and then waiting to be forgiven but because of the increasing forgiveness times and faulty validators spend more and more time there and so there's more and more time where this thing is kind of stable so non-sync relation faulty validators eventually

stop marking each other's faulting and they eventually forgive each other and so here's kind of like our key theorem for this this one eventually we have a stable connectivity graph for long enough so imagine we have a same similar concept construct for connectivity graph or basically draw an edge between nodes if they're marking each other is correct and you know you could imagine that because of this pattern that I described earlier where eventually correct notes stop mark each other's faulty and faulty notes get marked as faulty for long or and longer as it takes longer long and forgive them eventually we'll have a connectivity graph that's stable for an arbitrarily long period of time so in in a synchronous network we had

like a permanently stable connectivity graph now in a partially synchronous never we have a slightly weaker result but it's stable for for some time so so this is eventually stable for arbitrary long connectivity graph is going to provide our basis for liveness and partial synchrony in the context of faulty nodes along very similar lines to our previous strategy in the synchronous network only instead of having like a permanently stable connectivity graph we're gonna have like a stable for long enough graph so similarly to before we're gonna have like a planner instead of a plan because our plan is gonna have to change as a function of the

connectivity graph which before was kind of you know all fully connected because we kind of do that everyone was correct and now which is now the connectivity graph is gonna change and you know the the planner is gonna return again as a function of the largest connected component of the connectivity graph so we have similar properties for the for the validator but instead of having you know every suffix have an odd one now we kind of need any long enough period inside to have one so that like if we have like a long enough period at some

point we'll be able to make a decision so the planner the planner has like slightly different criteria next message time is calculated exactly in the same way as in the partial synchronous thing you look at the people in the previous slot in the plan ask what their next message times R plus the amount of time you're waiting for them the maximum of those is the next message time and similarly basically between non synchronization faulty validators their stops being failure is only failure between singer station an on synchronization faulty validators and so this thing is going to be basically stable and and the validators are connected while it's stable are able

to send messages back and forth and and because this is stable for arbitrary long period of time we get to execute an arbitrarily long section of the plan which leads to this odd thing hitting and then whatever number of layers of agreement that we need for a decision and so very very analogous to our original kind of setup we have liveness in partial synchrony great so now I'm going to go to just quickly look over some some future work that we need to do so this stuff the synchronous stuff has been formally specified fair form verification is still kind of ongoing formal specification of the a of the partially synchronous one hasn't been

specified now we just have informal verification of both of these at the moment we need to come up with practical planners that can basically like sketch nice things through connectivity graphs efficiently I hit all the validators and which have these properties we need to have basically reasonable increasing wait waiting times and forgiveness times and this is all for the binary consensus as all kind of can naturally be extended to blockchain and other kind of consistent protocols and it kind of needs to be we also are really interested in kind of weaker notions of partial synchrony where we have like clock drift and you know there's multiple notions of portal synchrony and

kind of we are curious and like to come up with solutions for different ones and the weaker the assumptions the more kind of broad of aquatics we have liveness in and you know in this context we kind of have a solution you know on sketch paper like not clear if it's understand correct but basically it's just like a more the the bound calculation is tricky because like you have to translate clocks and from like the remote clocks the local clocks in order to figure out your next message time but it's kind of very similar story we also want to worry about performance like you know making sure that the overhead and leniency aren't affected by faults like all of this showed is that like you know the faults can't stop a

decision forever it doesn't say anything about how long it'll take to make a decision and it'll be good to have some notion that we have robust performance so basically we were able to come up with liveness life Lyman strategies and synchronous and partially synchronous networks and somehow similarly to how we did it for consistency using equivocation fault detection this time we used we use synchronization fault detection either you know perfectly reliable or eventually reliable fault detectors and with these fault detectives we can build this connectivity graph which show us where there aren't faults and therefore where

we can successfully send messages back and forth and we use that to plan where how the message is going to be sent in order to have and you know kind of liveness through the execution of a pattern of locks or messages that leads to agreement so you know a network with a stable connectivity graph is a lot like one without faults and you know that's it so and that's kind of like the key kind of mmm those were some of the key kind of ideas that went into this research well thanks a lot for listening and please come for my crypto law talk tomorrow

really appreciate it [Applause] if you have any questions no says here have a minute and a half I don't know jack actually you talked about it in a conclusion when you say clock drift but how do you handle cases where you receive messages from the future because of clock drifts like how could you have yeah so the idea with clock drift is like you know you translate other people's clocks into your clock and so you know imagine if if the clocks are all kind of big ole linear on each other

then you can kind of have like a linear transformation between like their clock and your clock so you interpret their time in your time and if you sample basically messages from them in a watt over time like they say they sent a message of time 10 20 30 and 40 and you received it at 15 30 45 and 60 you kind of have some notion that your clock is running 50% faster mmm so we're using the differences between their message times on their local clock and when you received them you can kind of do a translation of the rates of the clocks and that ends up being you know a lot of the puzzle for for doing that kind of coordination okay

what about the all the way around like really when you receive a message that like in the time that hasn't happened yet for you even if you translate it you know exactly yeah so I mean in some extent these are gonna be estimates and you know if if the estimate of when this was sent is in the future I mean I don't know I don't know if that's I don't know how I don't know how relevant that is exactly but these things gonna happen is like you're gonna you know if the message comes too late then you mark them as faulty and wait longer here it's coming it's coming too early so I don't know I mean that's a good question I'm

knowing I started off my head sorry it's okay I have a hard one for you sure sorry well how about the Byzantine failures like what if you start getting yeah yeah so we have this like I think that I'm amazing theorem that I would love to share basically that like kind of relates and shows how we can relate Byzantine fault our analysis to this typed photo analysis that I'm doing here and basically like you know for validating protocols protocols that can like only receive messages that are like valid in some sense they can only take traces that are valid in some sense and so we can look at the Byzantine cases just in terms of the valid traces and

those and the faults that are observed they're basically of particular types like for example synchronization faults and equivocation faults and you know we can kind of show that like okay all if by if I can look at all of the traces that like the whatever Byzantine faulty traces are definitely in there because if I'm looking at everything whatever undefined behavior you give me will also lend me some somewhere in that everything and so I can kind of I can I can I have like a foundational theorem that will kind of that tells me like why I don't need to worry about on type fault tolerance analysis and why looking at the type faults is kind of enough yeah it's cool come find me after okay

thanks thank thanks guys [Applause]