Formal Specification and Verification of the Distributed Validator Technology protocol

foreign [Music] thank you for making it today um as the title says I'll be presenting on our work on formally specifying and formally verifying the distributed validator technology protocol and the way I'm going to do so is by answering to four key questions why do we need a distributed validator in the first place why do we need to formally specify and formally verify the distributed by data technology protocol how does our formula specification look like and finally what they've actually achieved so far and what is left to do but before diving into answering to these questions some do acknowledgments this work has been carried out by consensus r d as I received a grant co-founded by the ethereum foundation oval and SSV Network also I'm here presenting the work but this was done together with tanaitran who is one of my colleagues in the distributed system formal verification team at consensus everybody I think so at least I can start answering to the first quick questions why do we need a distributable validator now if you are here before the talk by Colin Eisen you may already know about why but I'll briefly go over it actually the way I go over it it will be by answering to another question what can go wrong with an ethereumable data well there are two things at least that can go wrong with an ethereum validator the first one is that your ethereum no ethereum validator might fail and let's see what this means now you know you have your slots in some of the slots you have to propose another you are a tester and your ethereum validator is working what this means is that it produces blocks you get you get Rewards produces attestations you get Rewards but now suppose that your node fails but what's going to happen is you start missing uh your duties so if you miss the blog you don't receive rewards if you miss an attestation you don't receive the rules you also get penalized what this means basically with what can happen with a node failure is that you Minister rewards and you also can incorp penalties the second thing that can go wrong is that the validator key might be compromised and let's see what this means assuming your Assyrian validator with your validator signing key now in malicious note is somehow able to steal it what these Mauritius Now can do can actually produce for example two at the station slashable attestation sign with your validator signing key and package all of this into a slash improve signed with a malicious note signing key and propose a block submit it to the network what's going to happen is that of course you're going to get slashed and some of your funds get actually um kind of transfer to the malicious note so while this while the malicious note doesn't have the withdrawal key they can still somehow get some of your funds and this is very bad it's bad for you as a Staker it's bad for the network because it means that Malaysians get can get more and more power more and more stake and we don't want this a way to fix this is not a straightforward as one might think just thinking about the first issue which is if you want the simplest one might think well let's just run more than one ethereum validator and well we know from the early day of the big contain this is perfect recipe for getting yourself slash too yeah we know we don't can't do that this is why by the female Foundation car and come up with the concept of distributed by data technology protocol which is um simplified here so what you need essentially is you need a coordination layer between the different nodes you need this coordination layer because you need to ensure that whatever attestations are submitted potentially by more than one no they are not slashable and this relies on a consensus protocol that so basically have a middleware between the beacon notes and the remote signer and this middleware which is called distributable editor client runs underneath a consensus protocol plus another layer on top that ensures that we must ensure that you never get slashed this is a protocol that allows basically splitting the distributed validator signing key into different key shares and it's a remote signer as its own key share so none of the remote signer as the full key this is what uh ensures protection and against uh a little signing key staining okay now we know why it's important well why do we need to formally specify and verify such a protocol we have removed any single point of failure and so we have higher resiliency however you know there is no such a thing as a free lunch we have increased the complexity of the system now we have a distributed system in place of a single piece of code and so we have higher senses of bugs and this is where firmware verification can really help us and to give you an idea of how it can really help us I want just to draw a comparison to testing and the key concept here is that formal verification is exhaustive and testing is not to give you an idea with formal verification we can consider networks of any size you pick a number we can deal with it you can do that with testing yep only small Network sizes and it's very important when it comes to Byzantine Behavior because with formal verification we can really consider any any Byzantine Behavior Uh with testing even with fuzzing you have already you can only consider limited set of Byzantine behaviors perhaps you know it doesn't respond but you can't really exhaustively consider all of them also if you want to make sure that a property is insured well and and this property actually does in thought so there is a bug in the protocol well with formal verification it can be detected with testing maybe yes maybe no it depends uh it's not exhaustive so you might get lucky moreover if a property is actually true well with phone notification we can prove that is true when we're testing we cannot do it because again it's not exhaustive so this is the benefit this is why formal verification is very well suited for this protocol now I want to give you an idea of what formal verification consists of you have a formal specification which essentially is a mathematical definition of how the protocol is supposed to behave which says basically when you receive message X you need to send message y then you have a property definition which is a mathematical definition of the properties that the protocol is expecting to guarantee something like never commit a slashable offense although this is kind of packaged together in a formal proof which is a mathematical proof that the protocol specification ensures the properties now what we do we take this a step further and we work with machine checkable proofs it means that our proofs are very checked by a computer and this provides higher guarantee that the proofs actually correct okay now we know why we need to do that and now we can have a look how the specification actually looks like now the specification is not a piece it's not a single piece it's modular we need to specify the different things we need to specify how the single node you know the DVC the middle layer behaves but you also need to specify how the Byzantine node behaves and actually what we need to do is specify what it cannot do so there are things the percent I know it cannot do cannot for Signature also it cannot change the state of another node so all these things need to be coded in the specification we also have a specification for the consensus protocol this is because the DVT protocol is agnostic of the consensus protocol used and so what we need to do we need to specify the behavior that we expect from the consensus protocol we also need to specify how the network is supposed to behave for example which sequencing of messages in my event I'll go over on this one in more detail later and all of this is put together is linked together in the distributed validator specification what we have actually we also have an actually uh executable reference implementation that implements the single node specification and all of this is written for this project in Daphne which is a programming language um it says a python JavaScript like syntax and it's a formally verification aware language and so I'm going to go over with the spec by starting from the bottom has been a bit say vague abstract I want to give you some practical code to look at so I start from the executable reference implementation what I want to show here this is the method that is called when the consensus protocol decides on a new attestation what I want to show here is that um the code is pretty easy I would say to understand it's a really I think that any developer would be able to read it um it's really a mix of JavaScript and python you have some form of some statements that are required for formal verification those are the top if you are just interested in say look in the reference implementation and having your own implementation you can just ignore them there are also some specific syntax like this one at the bottom which is kind of the equivalent in some sense of exception propagation in in some of the common languages but aside from this is pretty simple and this is one of the reason we have chosen definitely for this project to to to to to basically make it easier as easy as possible to for the developer development Community to really use and this product protocol but now let's go up how does the actual specification looks like so what the specification does really defines how the system transition from one state to the next and the system State includes the state of all the various nodes uh the state of the network the state of the adversary the state of the consensus so all these things is encapsulated in the in different fields so let's say of the system state now the transition says well on a given event which can be a new set of Duties time to execute the next Duty message I received you move from one state to the next slide from the yellow state to the Green State one very important characteristic of the way this specification is written which is commonly also to our Kelly plus way of writing specification in TNA plus we allow non-deterministic Behavior now what you have on the and explain why this is important what you have on the left hand side is not really non-deterministic but close to it so what can happen is that from one state you might have more than one event that can move you to two different states so so for example a node might receive a message from node 2 or perhaps on Note 3. and this this is what allows to capture okay Network asynchrony so and this is one of the important differences to testing we can really reason on any possible sequences of messages any that you can imagine this is coded in the other point I want to make is really about the non-deterministic behavior so from one state the same event can get you to two different states and now why this can happen mainly because of that adversary so if you have a given state the adversity can behave in multiple ways on an event and this is a what allows us to capture this while I speak about this I want to draw a comparison to model checking which is a different technique and with model checking you have the problem of State explosion and it's very it will take it's very hard for model Checker to really being able to check a property considering Byzantine Behavior because it will take a lot of time and with formal verification takes a lot of time to put together the proof but once the proof is put together it's quite quick to be run through now looking I want to show a bit code again how actually the formal specification is Brittany Daphne um let's let's focus on the top top of the slide so let's assume you have this transition from the yellow state to the green and purple State when the gray event is received the way we code it we essentially have a function that takes a source date an event and the destination State and returns a Boolean now the way that the transition is encoded is that the function if the function returns true on a given Source event and destination state it means that the system can transition from source to destination given the event if it returns Force there is no such transition so in this example for example is true for a yellow gray green and purple but not false for any other combination and this is you can see at the bottom is coded in this is how it's coded in definitely now this is essentially a simplification of this um but it's it's a um this is expressed using first order logic you know this is something we don't see often in standard uh programming languages but it's not much of a stretch to say what you can see here this is essentially an end of different state transition and here we have the state transition for the honest node and you can see here we say basically this much true for hollowness nodes that's what the photo does and then we put this in a coin end with the state transition for Network adversary and consensus you know what you can see here is this exists is what gives us the non-determinism because we're saying this function returns true as long as there exists a set of messages received messages sent and decided value says that they satisfy all the various constraints and the end expression at the bottom now before going into what we actually achieved I need to make sort of disclosure uh that are part of this say system that needs to be trusted so these are the parts that need to be trusted and um and these are the parts that actually we don't trust now if you look at this it seems the area it's quite of the trusted and non-trusted but you know the error doesn't really represent the value of complexity also it's not really a problem of formal verification it's a sort of existential problem you you need to assume how the adversary will behave in your system even if you just buy software you do you write tests whatever you do you need to assume that you have a consensus that or a library that works correctly you have a network you assume how the network will behave um saying things for properties you assume that you have a set of properties that are those that you are really interested into so this it's it's just something that yes a formal verification doesn't doesn't solve but it solves a good chunk of problems in ensuring that well your single node as it is specified will does we guarantee those properties also there are things one can do to increase the chances that the trusted path is correct one is to keep the trusted specification as simple as possible one is to have a peer review uh also for the tool it's important to use formal verification tools that have good support we use Daphne Daphne is very active bugs get fixed very quickly also uh in distribute the system usually you have two types of properties safety properties which say something bad will never happen and you have liveness property where they say something good will eventually happen now being if you formally prove that a specification guarantees both it's very it it really increases the chances that the trusted part is correct it's quite hard to put together a specification guarantees both both properties it is incorrect so now we can go over what you actually achieved so far and what is left to do so on the right hand side you have what we've been able to prove on the left hand side you have the assumption to have been able to prove is that slashable attestation signed by the distributable data signing key the one that is shared they can never be created in other words the account associated with the distributed validator signing key can never get slashed because of attestation signing and this is done under the the assumptions you see on the left hand side and assumption is as again we have any we allow for any message delay we don't constrain this at all we had allow messages to be lost we also allow the biker nodes okay typical notes here to be actually out of sync for this proof we don't require them to be in sync they could be serving completely different duties and they prove still old and then we have some assumption on the um number of nodes that can that are either Byzantine or with a compromise key to be less than one thought and this is um theoretical bound on consensus protocols as well we assume that signatures cannot be forged and they are unique and also that you have a sound two third signature scheme and then these assumptions we've been able to prove the property we've also been able to prove that the reference implementation adhes to the specification now what this means is that it is that if you deploy a system uh running the reference implementation of the of the distributable data client node what you get is a system that ensures the non-slashable attestation and so looking that what is left to do so we put together this proof we have the specification we have the reference implementation and it's all open sourced on the on the GitHub repo that you can see here what is left to do is to extend the specification and the reference implementation to distribute the block proposing and block header signing to extend the funnel proof of noise lash about the station to no slashable blocks and then to add the proof of liveness as I mentioned before so proving that a distributed validator will always eventually create a valid attestation valid blocks and valid header signatures and this is all for my for me thank you for listening um what techniques were used to prove that reference implementation adheres to the specification so um okay so we have used the refinement technique so we proved through a refinement basically yeah showing that if there is a relationship between the uh rest implementation State and the specification state that and on a transition that is maintained how far away do you think we are from being able to use validator pools for either eth2 or other protocols I probably this is a question I need to to the fair to someone else sorry I yeah it's only this is about implementation so yeah I I don't have that answer how difficult is the learning curve to kind of become someone who can contribute to this uh you know formal verification things and be able to to start working on that it's a reasonably say steep not too much though I mean nowadays with tools like Daphne I think it's much simpler than having to learn something like Isabel or this pyramid proves that are a bit not more you say abstract syntax and um way of proving things so things are improving but that is that is a bit in terms of contributing to the specifications say or reference implementation I think it's not my view not as much harder as contributed to a python specification so it won't contribute just to the specification you know necessarily to the proof how big is your team and how long have you been working on this proof to get it to this point now so well uh the the theme consists of four people um but on this one I've been working just myself and tanai and we've been working on this on this uh on the we've been working initially in the specification so on specifically on the proof I say since June roughly just for the proof there was a bit of fixing up of the specification before that so why Daphne and not other languages like cocoa or Isabel as you said yeah one of the reason is that is for the said the fact that we think it's easier for developers to understand Daphne compared to or lean or Isabel that that's one of the of the reason also I mean you can compile uh if they I think or Isabel but it the way you write it is far more complex yeah yeah I'm not pretty sure like we definitely can kind of um use a as a construct that is as the concept of classes and state so it's very similar to programming and you can have some give some of the things unimplemented and open for external implementation