VLSMs—analyzing faulty distributed systems

Testing, testing. Hi, everyone. Hi, hi. Yeah, I'll take this mic, actually. Thank you for coming to this early morning talk.

It's going to be a talk on formal verification and like some basic methods in distributed systems and reasoning about faulty distributed systems. All of the, everything presented here has been formally verified by the team at Runtime Verification and is, like, available to, like, click and check. And you can look at the proofs in the talk, but this talk is not going to be focused on the proofs, more just definitions and theorems and not really walking through the proofs. But you can check them out. And there's a...

So I've separated a bunch of sections, a section on validation theory, a section on equivocation theory, and then on relating and reducing Byzantine faults to equivocation faults in the context of validators. So let's kick it off. So let's talk about validation. And so here's the slides where I guess you'll... So this is the name of the paper.

Validating labeled state transition message production systems. So it's for modeling distributed systems, faulty distributed systems, and all these amazing people worked on it for a long time. Here you can scan this QR code and pull up the PDF if you like. I'll show this also again later. So here's the validation theory section outline.

Basically, we're going to go through the definition of this model, its compositions, and then the definition of validator, and then move on to the equivocation section. So here's the first definition here. So a VLSM is a tuple, you know, as we often like to define these things. It's sort of like a state transition system like you're normally used to, except for it has a few other things, like a label, which is also not too unconventional. But it has a first order message set in the definition.

It has initial states and initial messages. And then there's a transition function that takes labels, states, and messages, optional messages, and gives us states and optional messages. This is like the state transition slash message receipt and production function that describes for a particular VLSM, sort of what's happening computationally, you can imagine. And then they're also equipped with another thing, which is why they're called validating, this beta, which is a validity condition. And it basically says, it's going to be valid to transition on a label from a state given a message.

So when you're in a particular state and you receive a message and you might want to transition, there might be multiple possible transitions each identified by a label. And some of them might be basically banned. Even though they're defined by the transition, the validity condition won't let you take that transition. So this is like a state transition system with native messages, with initial state messages, and with a transition function that's totally defined over this domain. And then we sort of restrict it, effectively making it partial with this validity condition.

This is like the validation condition. Basically, we're going to imagine that these things don't transition, even though the transition is defined, when the validation condition is not satisfied. And so that's the definition, but actually, I haven't told you how to get the states and messages, but it's sort of what you would expect. You start at the initial states and the initial messages, and then we build up this fixed point by taking the union of all the states that you get from the transitions and all the messages that you get from the transitions and transitioning from those states using those messages. So basically starting from the initial states and messages, transitioning and sending all the messages that are produced from there and receiving them and doing it over and over again, basically, until you even get stuff like a node in an early state receiving a message from some other state.

This really is a big fix point. And so there is an interesting thing that can sort of happen, which is the validity condition can be satisfied even when an input message is invalid. So we have to slightly distinguish between just the validity condition being satisfied and the actual trace being valid. The trace is valid only if all the input messages are also valid. So, you know, no garbage in sort of allowed in a valid message.

So that's basically the definition of VLSM. And then they have a pretty natural way to compose them. And so, now I'm going to go through that definition. Unless someone has, like, a question now before the composition. Okay.

So, basically, what we're going to do is we're going to take a disjoint sum of the components for the label. So we identify the label, which component it is. The state is a tuple of the component states. The initial states is a tuple of the initial states. And then we have like a union of the messages for the initial messages.

And then here, actually, we're composing of VLSMs that have the same message type. This is just so that all our transitions are defined and everything. And to let them send messages to and from each other, so they're not just independently. Like if that was a disjoint union, they wouldn't be communicating. So we have a disjoint union for the labels, tuple for the state, and then a regular union for the messages.

And then in the free composition, we have a transition that basically just affects only one component exactly according to the transition that would have had before the composition and checks the validity condition only of that component exactly like it was before. So very little, basically nothing being done by the composition except for transitioning the individual components and checking their individual composition, sorry, their individual validity conditions individually. There's no composition-wise constraints, but they can message each other in this thing. And then, you know, note also that this is also VLSM, and that's why it's like sort of a composable model, you know, same type of definition and everything. Yeah?

So the split up of the transition functions and the validity where they are purely mathematical? So the question is, is the split up between the transition and the validity purely mathematical? I mean, I guess it's for the sake of convenience when dealing with the math and... So, but, I mean, more more traditionally in math you'd use like a partial function I guess whereas here we're about to get into this conversation about validation and distributed systems and what can happen in a distributed systems that you might not be able to tell locally about and so it gets there's there there is a reason why we are thinking about the validation at different levels. And actually, and that actually does sort of spell it out.

Basically, there's going to be, actually, the next slide, we're going to apply, we're going to talk about constraint compositions where there's an additional constraint on the, so basically, like, this constraint composition just basically conjuncts a constraint on top of the, uh, validity, on top of the validity constraint of the free composition, which just is the individual constraints applied independently. So this, this, this composition constraint, um, you know, lets us sort of analyze, uh, things a little bit more conveniently than just a partial function approach. I guess you want to be able to see that a transition would be possible, but it's not there. Yes, so the question is if we're doing this to try to see if a transaction is possible but not valid. And yeah, you're very much going in the right direction.

And we're getting there to try to see if a transaction is possible but not valid, and yeah, you're very much going in the right direction. And we're getting there with this definition here. So, this is the definition of validator. It's a very natural, simple definition of validator, which is kind of useful in many different contexts. So, in a...

And so, the components are a validator for the composition basically they're checking if they're truly a part of that composition and they're sort of you know only transitioning as if they are a part of that composition even though they don't know it per se so let me just go through this definition so basically a component in a constrained composition is a validator. If any transition that that component can make can be lifted to a valid transition in that composition. So if the component has a valid transition, then if a validator has a transition, which it can take, then there's also a transition in the composite system where that validator can take that transition. It sounds kind of... It sounds weird, but basically it's not.

The local condition lifts to a distributed one. And so basically, this local component is checking about a condition that's distributed across the whole composition. And that's sort of non-trivial because of information disparity between the nodes. So there's a message here being received, and this is the message being sent, and this is the label, and this is a constrained transition, which doesn't necessarily mean that M is valid. However, it's lifted to a valid transition with M being received.

So basically, the validity condition of the component is enough to guarantee the validity of the message received in the composition. So basically the component locally is able to verify whether the message has this distributed property. And that's why it's called the validator. Because it's basically able to check something that's outside of its scope. And it's again defined here with respect to a particular composition and a particular constraint on that composition.

So you might have different validators for lots of different distributed settings. But we're specifically going to be interested and focused on equivocation for a reason that I've already talked about, but it sort of reveals at the end why equivocation is so particularly interesting to look at. So the equivocation theory section, talk about evidence, and then using evidence to describe compensation constraints that limit and validity conditions that limit equivocation. And then we'll talk about models of equivocation. And then all this will tie in nicely when we start talking about Byzantine faults.

So this is sort of what we're used to seeing in blockchains when it comes to slashing conditions. This is a starting point, or was a starting point in our proof of stake research. Basically, when messages have the same sender, they've been, they're like collected by the same node, or like in the same smart contract, you can imagine. And they basically could not have possibly been produced by the sender in a single round of the protocol. So if you run a trace of these things, there isn't a single trace where those two messages are produced by that node.

And so this is evidence of equivocation this is somehow we have two messages that couldn't have been produced by their sender and we have them sort of in the same state this is sort of a sort of faulty behavior and this is a local evidence and here's an interesting definition. Yeah, yeah, of course. Sorry. If we don't have a history, how do we check that? What?

Yes. So that's a good question. I mean, I think it's undecidable in general, but the question is whether it could not have been possibly produced. So basically you need to sort of quantify where all traces and say there is no trace where these two messages can be produced. So in practice, you know, we have lots of simplifying assumptions like you're guessing, you know, we have lots of simplifying assumptions like you're guessing, you know?

But the definition doesn't say how, you know, how we can come to this decision about whether a message could have been produced. You know, it's okay. That's actually another nice thing about having the validity conditions as sort of like predicates. You can have undefined, sorry, undecidable conditions, whereas, you know, if you're using partial functions, that would be an issue. So there's global evidence is a little bit more interesting and a little bit more, maybe a little more decidable, right?

Because you, in this, we have like a sort of global view of the trace. So, we can basically check that So... Yeah, so... So this is getting into some later content that I was hoping to, I think I've slightly misordered this. But anyways, if you have a God's eye view of a VLSM trace, and you have a message that wasn't sent by a component, but it was received by some component, that's an equivocation.

Sorry. Denise, can you go ahead? No? But I think it would be like a equivocation or a thought-form equivocation. Mm-hmm.

Yeah. So here's a theorem, right? That the local equivocation is always going to be less than the global equivocation. And all these are checked in the theorem provers, but you can sort of imagine why that is. And basically, we can use these global and local definitions of equivocations to limit the equivocations to create basically a composition constraint where the faults are limited.

We can easily just say, okay, well, there shouldn't be any equivocation and talk about DSM traces where there aren't any equivocations. And we also use the full node assumption to reduce the amount of equivocations because then you can only sort of get an equivocation from the sender of a message because you've already received all of its dependencies. We can limit equivocations to just a subset. And we can also assign weights to the nodes and then limit the equivocations by their total weight. These are, like, example conditions in composition constraints or a local constraint.

So this is a composition constraint for a validator on a global constraint that looks like this. And so, like, in this particular example, this validator is just checking the local equivocation weight and if it's less than T when the composition constraint is checking the global equivocation. And the validator property is basically that from the local one, there should be a state where the global one is also satisfied. Basically, the lifting property of the valid state from the local to the distributed property. So, you know, this was talking about basically what equivocation looks like and how to detect it and therefore how to talk about, you know, non-constructively traces that have limited equivocation.

But we do have a very nice constructive sort of approach to where we can describe equivocators and basically there's two models for equivocation. There's a state equivocator, which basically splits its current state up or has many states for the same validator. And it can do that by forking or by starting new machines. And it also has... And there's also the message equivocation model, where instead of the state splitting and having multiple copies of a validator, validators can receive messages that haven't been sent.

And sort of this sort of is what we're observing in that definition of global equivocation. And it turns out that these two things are equivalent, actually. The traces that you can get from the state equivocations and the message equivocations are the same. Whether you are receiving messages that haven't been sent or splitting up states, if you project down to those equivoc up states, if you, like, project down to those equivocator states, we get exactly the same traces. And it's kind of interesting, basically, like, splitting a timeline and communicating across timelines end up producing exactly the same states.

And so, these two are models of the same phenomenon equivocation. And that's why we have those two definitions there where one of them seems a little bit different than the other. You know, somehow two messages that couldn't have been produced in a single trace evokes a state equivocation, and a message that hasn't been sent yet to being received evokes the message equivocation. But they are equivalent. So that's a pretty cool result that's going to be useful later.

But basically, to repeat it, the models of equivocation that split the state and models of equivocation that allow communication from other traces lead to the same traces for validators for a limited equivocation. So that means that when you have evidence of equivocation being produced, you can produce that evidence either with state equivocation or message equivocation, and you get exactly the same state, exactly the same evidence. Great. So that's the first two sections. Any questions before the next one?

Excuse me. So here we go. Yeah, please. Your microphone is off, sir. Can you try it?

I guess in the previous discussion, you kind of assumed finite branching, which means that you cannot make infinitely many copies at the same time. No, we have an unbounded, we have like a, a list, like, unbounded list of copies. Okay, but still finite, right? Yeah, finite, but finite unbounded, yeah. Yeah, because when it comes to infinite messages and states...

Yeah, that's a good question. I think we have possibly infinite... traces, but not states and messages? At the moment. Yeah, I guess so.

Sorry about that. Yeah. We'll get there. Yeah, so now basically we're gonna do, yeah, go ahead. Yeah, please use the mic here.

Microphone, microphone. Yeah, please use the mic here. Microphone, microphone. Just hold it closer. Oh, no, never mind.

Sorry. Hi. Can you hear me? Yeah, that's great. This is great.

Sorry. I think the states can be infinite but not reachable. It's a matter of which are the reachable states. But it matters how many labels you have and that gives you how many moves you can do. But in reality, yes, it's bounded and, yeah.

Great. So, let's move to the Byzantine faults. So, basically, we can model Byzantine faults in VLSM by replacing a node with a node that basically has a free behavior that uses labels to send and receive any message at any time. The important behavior is that it can send any message at any time, basically modeling someone that can send any sort of malformed and invalid message at any point. And we do have a little bit of constraints, which is that we don't let them forge messages on other nodes, and we do have a full node assumption.

But, you know, they can send any message, you know, signed by them from them, basically, without forged messages inside. And so, we can replace equivocation limited validators with Byzantine components and find that they have exactly the same traces. The ones that aren't replaced have the same traces. So if you have a trace in the equivocation-limited composition, where some set B of validators is Byzantine, they have the same traces as if they're composed with equivocators instead. And basically that's because of the validator property.

So if you have a validator property on receiving a message from a Byzantine sender, that means that there is a composite state where that sender, as an equivocator, can validly send that message. Because here we're validating for a limited equivocation setting, so some amount of equivocation is valid in that setting. And so we can replace these Byzantine nodes with equivocating nodes. And then look at the traces of the validators that aren't equivocating and show that they have exactly the same traces. Denise, do you have a question?

Okay. And the same result also holds for weight-limited equivocation model. So it's not just for a fixed set, but for under T-limited equivocation weight. All the behaviors of non-equivocating components due to equivocating components is exactly replicated by Byzantine behavior with the same T limit. And so that basically means that under the limited less than T weight equivocation, we get all of the same traces for the validators as limited less than T-weight Byzantine faults.

So that's sort of the sort of magical way that we can not use Byzantine fault tolerance. Basically, for these equivocation-limited validators, equivocation faults are exactly as expressive as Byzantine faults because by validating for that limited faulty setting, you know, they're restricting their transitions a lot. And if a Byzantine fault, a Byzantine node can send some malformed message that they receive, that means that that transition can be lifted to a valid state in the composition under the limited T equivocation condition, which means that there are nodes in the composition distributed that satisfy that less than T threshold, but, you know, aren't Byzantine nodes, but equivocation nodes. And then, you know, like putting those transitions together to get traces, we can rebuild exactly the same traces. And so basically this forms an alternative for analyzing faulty distributed systems to Byzantine fault tolerance.

And quite simply, you know, by studying equivocation limiting and equivocation faults instead of, and equivocation faults instead of Byzantine faults. So somehow equivocation faults are like a special kind of fault where if you validate for limiting equivocation, that's just as good as validating for limited Byzantine faults. Oh, sorry. That's just as good as, sorry, that actually lets you throw out Byzantine fault tolerance analysis altogether when thinking about, like, what traces you could go to. You can sort of just go to the protocol-defined ones, and it doesn't really matter what the Byzantine nodes do.

They're basically just protocol- equivocators as far as the analyst is concerned. And so instead of having misbehaving nodes, they just have either like a state replicator or a message passer that sort of crosses timelines. Which is sort of much more tamed types and well defined behavior. So later we're gonna relax the full node assumption and treat synchronization faults. I'm out of time.

Thank you so much. Thanks for coming. Really appreciate it. If you have any questions you can find me outside later. Thank you.