Dynamic Restaking Security

DeFi Security Summit 2024 · 9 Nov 2024 · 24:06

Tarun Chitra of Gauntlet models restaking networks as matching markets between validators and services, and uses that view to define threat models and the minimum security a network holds. He shows how a cascading attack can follow when one slashed operator opens a profitable attack on the next service. An empirical look at live networks compares real parameters with theoretical bounds, and argues that operators who rebalance their stake after a slashing event limit how long cascades can run.

Speakers

Topics

From DeFi Security Summit 2024, hosted by DeFi Security Summit.

Transcript

perfect thank you uh hey everyone uh thanks for uh coming uh I know it's early in the morning and some of us are also jet lags so I I very much appreciate it um so we're going to talk a little bit about reaking security um I think obviously as these networks are going live there's tons of capital in them it becomes more Paramount to think about what a a security model is B what threat models are and C how to model them um I think I'm GNA in this talk I'm going to sort of be more high level but almost all of the results you see or are mentioned are in papers online and you can find me to find

them so we're going to kind of talk about three things to to understand reaking first we're going to kind of Define reaking in a uh sort of more combinatorial and algorithmic Game Theory sense as a matching Market um then we're going to talk about different threat models how those threat models affect how you should assess risk in these systems and third uh we'll talk about what the notion of the minimum amount of security is uh that needs to be uh in these networks so first we'll talk about matching markets so restak networks are effectively matching markets between validators who are already operating ethereum for instance or or salana and the jeto case and services services are

extra new protocol extensions such as rollups oracles Etc that um are are trying to to utilize the the security of these from these valers In classical matching markets you know this is sort of one where you're looking at sort of dating preferences and you can kind of see hey the the set of edges represents the set of all possible viable matches uh in the thing on the left there's a feasible maximal matching in the right there's a a contention so matching markets are sort of everywhere um I think you know people won the Nobel Prize for them but the main difference about matching markets and sort of things like auctions that you see in me uh are you generally have

inhomogeneous Goods that have some shared property on the supply side so this in um this in the case of avss is is validators so some validators might be running B Hardware can run your extra service that needs a bunch of gpus some validators are running on Raspberry Pi they can't run all avss so there's some sense in which all of them share the fact that they're running ethereum consensus but they all have slightly different uh properties um a natural place where where you see matching markets outside of uh these types of settings is is kidney exchange and in kidney exchange you have this notion of Supply like everyone has kidneys a lot of people can donate them but there's

all these constraints blood type size um kind of you know how old a kidney is whether it's it's had dial Etc right so you can kind of think of each validator as a different kidney in this case uh I'm sure those with Rasberry pies are the ones with the worst kidneys unfortunately uh uh on the demand side you have services so that's oracles uh co-processors uh GPU networks Etc that are sort of demanding uh being operated so one important thing to understand about matching markets versus auctions you might say hey couldn't the validators just run an auction and say okay like you service Oracle like you

have to bid for us to run your Oracle site light client or side client one important thing is auctions focus on generally maximizing revenue or maximizing welfare for the the buyer and the seller matching markets are focused on stability which basically means when I match validators to Services there should be no one who's unhappy in the sense that they would rather have switched and been matched with someone else and in crypto we've seen uh especially over the last two years the micro structure move from a lot of auctions so me auctions uh poke pair chain auctions things like that to much more matching like things like intense and and reaking uh the natural way to represent matching markets uh is of course uh via

graphs and the idea is you have a bipartite graph that represents the supply side and the demand side those are the two portions of bipartition uh where one side is the supply so the validators and one side is the demand the services one important thing to note is that in most matching markets that are studied outside of crypto the this graph is static so it doesn't change so the set of people who could donate a kidney is not changing uh and there's usually a central planner so the central planner chooses the matching but in decentralized matching markets like reaking that's just not true okay so the first claim I made is is reaking is a a decentralized matching market so when we want to analyze the

security of matching markets uh they're a lot harder to analyze than sort of the the classical ones that we know of one of the reasons is a permissionless means you can be matched and unmatched at will B without a central planner the only way to to construct matches is by correct incentives and C you have to actually have an explicit adversarial model so well then we'll see some examples of this but you know for instance if I ask you the following question ethereum has a billion dollars of stake let's say hypothetically what amount of Economic Security does it actually have right you would actually have a hard time answering that if you said it has 333

million for double spends that's a valid answer but that's not really the notion of Economic Security for these other services so for an oracle Oracle manipulation might actually cost less because I only have to bid in Block building auctions for a certain number of time and so there's sort of some notion in which the types of attacks you're modeling can Define what it means to have a certain dollar amount of Economic Security and as you can see no one on the internet agrees uh so maybe we'll take a a tiny detour to try to talk about what the notion of Economic Security is uh I I think you know you can you can you know exercise left to the reader to to go find all the million

tweets about people fighting and being inconsistent so as I said earlier you know what does it mean to have $333 million of Economic Security so there's sort of a sense of which this concept of nebulous concept of Economic Security in an absolute sense is very hard to Define you have to choose what asset you're measuring in you have to enumerate the attack space you know double spends are not necessarily the only attack anyone cares about in 2024 you have to consider competitive pressures for stake why would I lock up my Capital if I can get yield elsewhere that's higher and you also have to think about how much the the opportunity cost for capital is of doing an attack and also

how long it takes to execute an attack but generally the the kind of attack cost is linear in the amount of stake somehow so you're writing this in in formulas you know we kind of say the cost of attack is lower bounded by a price P of times the amount of stake times some notion of compounding or opportunity cost based on how long it takes to execute an attack times some notion of a minimum threshold of stake needed to execute the attack so this is sort of just a generic way of saying this is what a lower bound on economic security is within POS for different attacks what does that look like for

reaking well reaking actually has two sort of competing pressures when you try to quantify what its Economic Security is the first is participants purchase stake uh to capture excess yield so if more people are buying ethereum to restake they're actually causing the economic security and dollar terms to go up so in some sense you can argue that reaking can improve if if a lot of new participants are purchasing on the other hand if people get slashed that reduces the overall network security right because I've basically burnt a bunch of stake that was locked and now effectively the total amount that can be slashed in the worst case event has gone

down so how would we represent this it's not so different from the last formula uh we have a notion of a a stake that's the capital Sigma we have a notion of a price numerator terms we have a notion of how much people increase the value which is this one plus Delta turn and then we have a notion of a risk measure which is how much stake is burnt what percentage of the stake should I expect in an average case or worst case scenario is slashed and then I have a notion of a price impact function so what this is is if there is demand for Delta times the stake uh that is there how much does that actually push the price up and then cause the actual cost of attack to go up

so if we zoom out one of the reasons for to trying to formalize this is you're really trying to measure some notion of cost to attack oops I guess that one was there so one question is when is reaking safe uh and so one one very simple definition is the cost of attack when reaking is present is always higher than the cost without reaking and that's what this inequality is if we write that out we get this formula and if we write this out we get a formula that says the amount the risk the maximum amount of stake that can be slided has to be as a percentage so this is from 0 to one has to satisfy this type of formula G is a a value greater than

one and so one important thing to note is that this this has this dependence of like the risk the slashing risk on the actual price impact of people participating in reaking which is UN is not great right because from a say formal verification standpoint or for from a fuzzing standpoint I can't really check this condition I can't make this a a a valid condition that needs to be met so the natural question is can we model this without needing the price or staking demands Dynamics can we kind of have a static model for what it means to for reaking to be secure and then you can construct formal conditions that you could verify so to do that we will have to do some

math so the the main object of study uh Within These systems is what's what is called a reaking graph um a restak graph consists of five components first is the set of node operators so these are the validators who are operating the network uh that's the set V second is the stake so for each operator you can think as a Vertex label for each operator of how much stake they have third is the services so this is the avss so this is your Oracle this is your co-processor this is your da layer Etc third is a notion of the maxim imum profit from corrupting a service so in this model you sort of assume there's

sort of a maximum Honeypot prize that if you were able to corrupt a service you get to get this amount of reward so that's what pi is the fifth component is a corruption threshold so in say a bft protocol it might be 1/3 which is the sort of double spend and proof of stake in a longest chain protocol it might be one half which is the sort of attack a a longest chain protocol um and one important difference between reaking and normal staking which is extremely crucial to the security model is that I can use the same stake to validate multiple services so this node operator V intersection uh is actually operating both Services S1 and

S2 with the same stake so they're putting up 100 eth they're validating both of those Services if they get slashed by either one of the services it's as if they got slashed on both Services that's a crucial point that you have to keep in mind I'm thinking about this okay so now you might say hey is this graph real like are you bullshitting me and like you just wanted to do some math for fun this is the igen lay reaking graph um over time green are edges being added uh the right side is uh the services the left side is the operators sorry am I getting it backwards yeah left side is the operator sorry right side is services but you can see that this graph is changing as

people are adjusting incentives over time and that as you saw earlier affects the security of this system so how do we how do we formalize in a sort of formal verification sense what an attack means so there are two conditions first is profitability profitability is give me a subset a of services and give me a subset B of validators who are colluding to attack that set of services and you need the profit to be greater than the slashing penalty so what this means is the maximum profit I can extract from attacking those Services is greater than the amount of stake I lose right so that's a positive uh profit attack the second thing is

feasibility so what this says is for every service I'm attacking this cartel this set of validators has at least the minimum amount of stake needed so this so for instance if one service is a bft protocol the attacking Services have at least onethird of the stake in symbols this is what this looks like given the variables we saw earlier on the left hand side you see the total profit from attacking the set is greater than the total stake on the left side you see the stake held by the cartel at each service is greater than the threshold so the first place are defined appendix B of the IG lay white paper the second place where was cleaned up and formalized which you know a lot of the results that follow are Dural and rough Garden uh

this paper from this year okay note that these are properties you can validate of a live reaking system right because a live reaking system is defined by this graph this graph is public all of the data here is registered on E theem if you go look at the igen Pod contract you can get all of these uh numbers on every block now what does a attack look like so in this graph each individual service is actually over collateralized so service one the maximum profit you can get is four but there's six stake so if all the stake is slashed you have at best a minus two profit and the same for uh service 2 but if everyone colludes to

attack both Services simultaneously it is a positive profit because I can get eight units of profit and I only have to expend seven units of stake and the real reason for this is because the middle node operator is sharing their stake so by slashing them once you slashed them everywhere so this naturally leads to what's known as a cascading attack so a cascading attack on a recking network is imagine that some fraction of stake is lost maybe that's a operator that got dosed and is down maybe that is an operator who was malicious and and and sent an invalid block and got slashed for some reason they've their stake has

disappeared once they've disappeared what they do is they create a profitable attack so in this case the middle operator can attack the first service once the first uh operator is gone and once that attack occurs they've opened up an attack for the second service to be attacked by the last operator so what this shows is that you can have these sequences of profitable and feasible attacks until you continue to lose stake and in this case you've lost 100% of Stak so this says R in the formula we had earlier is one which is bad because that means the reaking network has slashed all the stake of the underlying L1 which is obviously the

worst case this is the proof of stake version of a lending liquidation Cascade so how do we formalize this so we Define a valid attack sequence as a sequence of pairs of sets of services and sets of operators such that each attack AI bi is profitable under the definition we had and feasible and we Define a quantity r s of G which is very similar to the r earlier we talked about which is like the percentage of stake that is burnt uh expected as the worst case uh percentage given an attack if I lose size Stak so

imagine the network has a shock and it loses s Stak s could be say 10% uh then this says what percentage is the longest Cascade attack uh going to lose in symbols uh it's written like this just so you can see it's between zero and one so there's no hiding anything there okay so this actually helps us answer this question how much stake do we actually need how much Economic Security does our single AVS actually need to be secure we choose an RI threshold that we're we're happy with so hey we're willing to tolerate a shock of 10% at most and if ouri is only 5% given a 10% shock then we're willing to

tolerate that it lets you it lets you have some bounds on how much the worst case attack is so are we done uh not exactly so so this paper shows that there exists an infinite family of graphs with n validators where the entire graph is slashed which is very bad uh it's actually nice to see in pictures so in pictures each of these dots is a validator each of the boxes is a service so we have six Services we have the the red L-shaped services so there's four of those each with three validators each we have the blue box Services which have six validators and what you see is first uh operator is

taken out you move to the right and then when you go down uh a row you see that that opens up an attack against the first service which opens up attack against the bottom row which opens up attack against the other services and then all the stake is gone and because this is a tiling there's an infinite number of them so the same paper showed sort of a maybe a a blessing in disguise which is if you're actually over collateralized then you can actually bound this amount of stake you lose great we might be done however uh and sort of you can think of this as like the proof of stake analog of a decentralized stable coin

needs to be over collateralized to avoid cascading depex the problem is this over collateralization condition which we won't exactly Define is actually really strong so it actually says if I have a bunch of services I may have to have as much stake as the sum of all of the profits overall services in Translation imagine you have a reaking network that only has two Services where one service you can attack and get at most one ether profit the other service you can attack you get a million e of profit under this over collateralization condition you need a million and one e for the one eth of attack uh service to be safe which is obviously ludicrous at that point I

would just start my own POS Network right why would I pay for 1 million e to secure one e of aack profit so is this a dead end of course I'm getting this talk so the answer is no uh uh so one thing that this whole model doesn't consider is the incentives like how much are people being paid and how do we include that when we think about profitability for an attack so if we think about how reaking went from Zer to 15 billion it came out of people paying incentives it wasn't sort of like a a free lunch that people were running validators and so we actually have to think about each service offering an

incentive either a token incentive or points uh so we add one term here which is this term R which sort of represents how much each service is paying and in response to the rewards we assume the validators aren't Sitting Ducks they can adjust uh where they uh Place their stake and what this means is validators after a slashing event in this model can rebalance and they can in some ways halt these Cascades by pure economic incentive where you know someone gets slashed if if it was profitable for them it is profitable for me to join and so I will join and prevent the Cascade which

is what this yellow box is uh which is basically after a slashing event someone from the top row joins the bottom row prevents uh Cascades so in this model we assume the adversary is somewhat weaker uh in that the adversary has liquidity and cost to attack constraints uh and then we assume the node operators are they can adjust in response to these incentives and what we what you show is that basically the maximum Cascade length actually decreases as the number of services gets large and that you can compute this efficiently so basically what this says is if you have enough rewards you can actually and node

operators are not idiots you basically can reduce this Cascade risk that we saw earlier again adversaries face costs no operator smarter avss pay rewards you don't have as many of these attacks so what do how do we reduce this in practice so you might say hey IG Lay's live like what how do they actually do this so they they actually proposed a new mechanism uh called unique stake which is a notion that every service can say some fraction of the stake allocated to me is only slash by Me by my service like no no one else can slash it so in all of the Cascades you saw the reason they were were bad

risks was another service could slash stake delegated to my service and then I lost Economic Security the point of unique stake is I'm I'm able to say actually some portion of the stake is only slash by me and so each service is able to reserve a percentage of stake uh which caps the maximum overlap between Services of how much stake is shared and so it's sort of a trade-off between capital offici of these systems versus security and the key thing is when you have this unique stake you can actually provide very verifi efficiently verifiable guarantees even before the network is live some sort of uh like formal verification guarantees of taking

all these constraints I've talked about earlier and verifying them ahead of time and you sort of have this verifiable collateral requirement and with that I think that's it [Applause]