Specification and Model-checking of the ZKsync Governance Protocol

Transcript

okay thanks a lot thank you for the introduction and having me here so what I want to talk about here is specification and model checking of the ZK governance uh the cas governance protocol that's actually the work by danis colleague of uh of metr laabs and myself and I want to say that danis wrote a large part of this specification and I helped him with a choice of proper abstractions right in the protocol invariance and mod checking experiments so it doesn't click okay uh so before we start uh talking about the specification let's just have a brief look at what ZK sin

guance is about basically in the casing governance we have four entities the largest one is the token assembly that consists of the token holders and the delegates who can propose uh some uh contract upgrades and the other three entities have to ensure that these upgrades do not do anything bad essentially so the talking assembly can propose these upgrade proposals and other three entities can vote on accepting them or rejecting them in addition uh these entities can also uh do some kind of uh emergency upgrade proposals and execute emergency upgrades and in addition to that the

security Council can freeze and freeze Layer Two which is quite important in this case so that's the k s gance in very brief the I lot of happy P scenarios the simplest one here is that this emergency upgrade board executes the emergency upgrade very simple essentially one call all done how about more complicated uh scenarios well I shall click okay so actually if you come to to this protocol as as I did as an external external person how do you find this happy paath scenarios one way is just to talk to the developers but another way

as I did is asking the model Checker in this case I'm just challenging the model Checker and tell it look it's impossible to find a proposal that has been executed and it was approved by the Guardians and the model Checker comes back and says no it's not true he's a counter example of five states how does it look like I'm not going to give you the actual counter example here but I'm going to give you this graphical picture that is much nicer and the counter example looks like this you have the security Council that starts an upgrade then some time passes there is this magic period of 72 hours then the Guardians approve this upgrade another period passes of 800 something hours and

then someone executes this proposal right a lot of scenarios like that it's not just two scenarios right and for this reason uh we want to have this protocol specified and also to have the invance specified in in this work I'm using the language called Quint it's a relatively new language it's actually quite old because it's backed up by the tempal logic of actions that was proposed by uh Les Lampard long time ago but it's a new syntax that uh makes it more friendly for the engineers right and treat properties and the specifications what I find very useful about Quint that we have essentially

three tools here one of them is a randomized simulator think about it as property based testing stateful property based testing or a simple form of fing as you can see in Foundry for instance and what you see here are these yellow Lightnings on the radar these are basically concrete executions the simulator tries it might find bux it might miss buxs as always right there is a randomized symbolic executor that covers largest sectors of this radar picture and it can find more bugs but it can also miss them and there is a bounded model Checker that covers the whole Rider up to some rench and it's not going to miss bugs up to this rench

but it can miss bugs up to larger longer ranges uh the tool the tool set requires very minimal setup it's written typescript basically need nodejs and vs code or maybe Java if you want to run the model check so that was way too fast let's talk about U protocol specification basically how do we go from the solidity code to the specification written in Quint or any other language actually um where is the cat here so Quint or CH plus uh they are not tuned to solidity they're not tuned to ethereum Virtual Machine they have no idea about blockchains these are General specification languages it's kind of a bad thing because you cannot use uh the

standard Primitives there are no standard Primitives like this but it's also a feature it's very easy to add additional reason capabilities to your specification so at a very high level what we have here we have the protocol specified as a state machine the circles are basically states of the evm and the arrows are the transitions between the states these transitions corresponds to transactions or what we call actions and you have uh this computation tree that progressively changes the states what's important here that actions may have nondeterminism which corresponds to choice of different transactions and

choice of different inputs so okay since I told you that there is no buil-in evm State we have to model it how do we model it in the case of this protocol we just add all the necessary features that are required uh in in this protocol for instance we add the block timestamp because it's important here we add the states of all the contracts we are modeling here in addition to that we add the abstract states of L2 only the information we need from L2 and we had some history variables because we use this history variables in the

invariance so it's very simple just a record no magic how do we specify the contracts again there is no solidity so a contract for us is just a record that has uh fields that basically corresponds correspond to the fields in the contract there is no Constructors so we Define an operator which is basically a function from the arguments to the result and the result can be okay which gives you a state of the the next state of the contract the new state of the contract or it gives you an error is an error message so that's basically how we construct the contracts how do we specify the behavior again nothing

complicated we just have pure functional definitions here which take as a input the estate of the evm plus the states of the contract as you have seen it it takes uh the definition takes the input parameters it does something some comput computations no side effects no exceptions just straightforward functional computation if you like and it either returns an error again with an error message or it returns okay with a new state and basically we capture the behavior of the smart contracts by doing these functional specifications so once we have done uh with the behavior of individual functions we combine them

into actions and the difference between operators and actions is that actions can contain nondeterminism so nondeterminism means we can pick input data nondeterministically you see that on top uh the choice of sender from the set of all senders so just pick non terministic uh then we execute some operators which are purely functional as I told you once we have executed them if everything is okay we updated the state variables our state machine progresses that's one of the actions you have many of them and again we basically say that the single step of the state machine is a Cho is a nistic choice of different steps who makes this choice we

don't know right but that's your state machine so that's basically the protocol specifications there are a lot of definitions like that there are a lot of actions like that I would say probably 40 actions or something like that uh how do we specify the invs this is a bit more interesting because here we don't have have any solidity code we have only English right how do we go from English to to this specification for instance this is one of the requirements we have got from the developers which is saying unfreeze may be called from any address after the freezing period has been reached how do we specify it actually in Quint we can just write a state inv

varant which basically says that if the current state satisfy these conditions that the block time St is greater than this freezing period and the current freeze status is in freeze uh soft freeze or hard freeze then we can execute this functional operator and it should return us okay since there are no side effects we just executed and check the status very simple that's a state invariant we can check it in any state of the evm and that's it right so that's a very simple invariant we have plenty of of those there are also more complex en variants for instance this is a this is one of the requirements from the

governance procedures that are actually written in an actual document right once Frozen an emergency upgrade may be executed in order to remove the freeze and or initiate a subsequent freeze how does you specify that there are some formal methods people in the room they would tell me it's temper logic but I'm not going to use temper logic here actually we can specify this stuff as as a state en variant again what we do we go all over all possible parameters here we execute some operators we check some preconditions here and then we do something interesting I can actually execute one of these functions check

that it was okay and then based on the state this function has compute like evm 3 here we can execute other functions compute new States but since it's all free of side effects we can actually compare alternative feutures we can say that from evm 3 you could go could go to evm 4 and execute uh execute soft freeze and it should be okay or from evm 3 we could go to evm 5 execute a hard freeze and it should be also okay this is very interesting I have never seen anything like that before actually can talk about alternative Futures inside the state in

variance so that's a very neat modeling trick if you want to reason about things like that uh and basically we don't use any Temple logic here which is a bit surprising so by applying these tricks we basically specify a lot of uh invance from the governance procedures we have like 45 envir uh some of them are more complex some of them are simple and so on so forth so how do we check this invariance I told you that there are three different techniques uh what's the difference basically if you look at the actions if you look at this step and if you look at the definitions of each actions you will notice that there are two key constructs

here one of them is called any and that's basically saying I choose one of the actions non deterministically that's what we call control nism and in another construct is this nonde new time stamp blah blah blah oneof one off is data non determinism basically either you choose an action or you choose a piece of data both are nistic how do we resolve this non termism and the difference between these three tools that we have is that they resolve this non- termism differently in three different ways so when we are talking about the randomized simulator

it picks everything at random it picks actions at random it picks data at random very easy very simple to understand maybe not so powerful when we talk about randomized symbolic execution it Peaks actions at random or transactions if you like and it offloads the task of picking the right inputs to the smt solver to Z3 and this is done in the model Checker called apalach and the third way we actually of load the task of choosing the proper actions and choosing the proper inputs to the smt solver completely that basically gives us the bounded mod Checker which analyzes computations up to some bound

so these are three different tools actually the two tools below are the same tool just uh implementing different exploration techniques and what I want to stress here is basically they're not doing complete verification with these three tools what we do we do somehow progressively uh more complex more expensive analysis we start with a randomized simulation which is essentially cheap it probably doesn't have this good bu coverage then we go to random randomized symbolic execution it's more expensive but it gives you a bit better back coverage then we go to back bounded model checken it's in some sense

exhaustive because it analyzes all executions up to certain depths but it can miss long execution executions and in the very top you have this golden grail of formal verification we are not kind of trying to achieve that but we are trying to uh analyze uh the bugs to find bugs faster and this somehow resonates with this recent talk by Mike dos of gala where he says we should try to make our favorite formal verification methods cheaper and move them to the left that's how you can move them to the left basically basically um okay so that's basically about the techniques and now I want to give you some some ideas of how long it

takes to check all of these enires so for instance is it here there keep keep clicking it um so for instance when we check one of these invariance uh we have specified We R 100,000 randomized runs up to 30 transactions each and it just takes 3 hours it's actually not a lot right it's very fast in some sense you could run 1 million random runs and it would take well 30 hours I would say one day would we find all bugs we'll find a lot of bugs actually in not in this case but in in other cases we would find some bugs um will we find all bugs actually

not when we run the randomized symbolic execution takes longer even for 1,000 symbolic runs up to 30 transactions it may cover uncover more bugs and in our uh in our activity of right in the specification and invariance we actually found a lot of bugs in the specification itself and in the invariance we rising and finally bounded model Checker it's kind of slow right it takes 5 days uh to analyze all runs up to nine transactions but it's all runs even though slow and this figure gives you an idea basically uh when the r bounded model Checker up to six transactions it was run for half a day

not not so slow but actually it has uncovered four problems in the envirment luckily these were not problems in the protocol itself they were problems in how we wrote uh the invariance but it still has found some bugs which actually surprised me because we did a lot of randomized stuff we did a lot of randomized symbolic execution we did a lot of randomized simulation and still the bound mod Checker has found some issues then we ran the bound model Checker up to nine transactions some of of these experiments hav timed out it took 10 days really really a lot right and it has found no further issues so we're kind of convinced it should Dr more L right um so there are some kind

of questions of how you do more advanced modeling if you want to check it I'll give you a link to slides I I don't have time to discuss it one thing that I want to stress also so that there were other code audits done in parallel to this work and there were some submissions saying this issue can happen or that issue can happen what we could do we could first of all reproduce these issues in the protocol and after fixing the protocol we can check that these issues are gone which is quite useful if you have a protocol specification and the inance and writing a new invariant once you have written like 40 of them is not even hard okay so that basically finishes my talk

um if I can go to the last slide basically that's a summary what I want to stress here that understanding the protocol is essential it's not only about the lowlevel problems like overflows or some problems calling uh a strange address which is of course important but also understanding the logic of your protocol is important and we believe that protocol specifications help you to write in vars because because looking at the code it's a bit hard to write in variance also I want to stress that we should use all the tools available like randomize simulation I was kind of skeptical coming from formal verification I was like it's randomized it finds nothing sometimes it finds bux very fast but sometimes it misses bugs

so we have to use different tools that have different strengths uh of course this work doesn't replace code dos there have some code digits done in parallel uh and they focus on different things finally if you want to check all these things here's a QR code uh you can check my website uh we have a blog post that summarizes all this experience you can write it read it in detail and you can check the tools we were using thanks a lot that finishes my talk thank you so much eigor we have time for one question one question for the audience there is

question the lady in the back um thank you for that talk what scenarios would ZK sync freeze the protocol for what that I couldn't hear what scenarios would there be that would cause zky to call the freeze could you hear that well I I mean that's basically the security Council can invoke freeze and there like different different ways you could do freeze you could do this soft freeze hard freeze and there were also some issues when when basically what you could

do why you could do hard freeze and and without execution emergency upgrade you can uh unfreeze and do hard freeze again for instance the scenarios like that you have seen and they were basically fixed they were basically found in parallels I cannot claim they were found by us right but we could repu them okay okay thank you so much eager uh and