Common DeFi Invariants Every Protocol Must Respect

Transcript

Thank you very much. My name is Anton and I think my topic resonate with the previous previous speaker quite a lot because quite often you are having a new code base you are having a new protocol and you need to know what can go wrong and sometimes like you don't know where to start. And uh I here exactly want to again say that very important thing you need to identify in each protocol is the auditor or the developer is invariant. In this case I think bottom part is the most interesting you need to look at it's looks complex but it's basically formalization of transfer, right? You say that transfers needs to change the

balances unless you sending to the same address, right? Which I think like if you were being to sir tour talks it's quite often they show an example, right? But this quite often is very system specific and the hard to identify and uh yeah, I mean it's uh good to have invariant but it's hard to come up with one and developers not always coming up with them at all when they developing they coming up with like user stories they coming up with a business specific logics but they are not really thinking about invariants.

But good thing about them is that they are very useful for sort experiments even if you don't use any formal verification technique they are very good for fuzzing they are very good for formal verification if you get that deep into security and uh yeah, let's uh dive into what kind of smaller invariants you can use to identify bugs. I kind of have internal classification but to be honest it's all kind of the same. First is very important it's solvency. We have heard this maybe term before but what's mean solvency you can pay your debts.

What's debts of your of a contract? Most cases you have LPs like liquidity providers who lock their tokens inside the protocol. You need to be able to pay them back, right? And yeah, I I think it's very useful to think about this. There are many questions you can ask like can system wind down to zero euros? It's very important and very and quite often you have a violation of that because turns out somehow system locks the assets of the last user, right? Does system profit from all the actions of a user?

Yeah, this is a kind of seems like system profits, but in reality system profits in favor of majority, which is most likely people who still staying within the protocol, right? Uh another thing is uh data integrity. Uh it's uh hard to identify, but quite often you have variables that are weekly connected like meaning weekly that's uh you have a transitions within the smart contract that modify both variables, but you don't uh really have any sort of check between them, right? And you really need to think as the auditor as a developer uh are they always consistent on any function change that I have within the code, right? So, it'll be very bad if

you can mean token mean shares with zero tokens, right? And uh yeah. Okay. And now we're entering more interesting uh properties. Uh for example, I really like this invariant. It works for many protocols, especially for for 6 to 6 volts. So, like do undo. You pretty much deposit and you burn. Are you going to arrive to the same to the same state? Quite often you'll be surprised that if rounding is go goes any wrong direction, you're not going to be in the same state. Another thing, uh that's what I call like symmetry invariant. Uh you have mint and deposit at the same action. You just maybe or you uh specify swap specifying amount in or swap specifying amount out. Is it the

same thing? For balancer, for example, exactly balancer case, you there's always different routing if you have different specifications, right? So, such things are very important. Uh another thing is I mean it's it's interesting it's called shared resource. Uh it's where you have some kind of a shared variable that you maybe multiple users use and you need to be careful not to exhaust it. You want to go in more interesting stuff? Still have time? Uh it's compositional invariant. This is very cool invariant because X and Y here you see like we basically break big big action like deposit into smaller sub-deposits, right? And ideally you're reviving in the same state or like in a state that's somewhat

different by a fraction of a percent, right? But X and Y can be small or big as you want, right? So, be sure like if you make X as one way, you still need to arrive in a similar state, right? And the rounding quite often is a problem. Uh more advanced version of it is something like a version where you can arrive to the same state in multiple cases, right? Here I can just exchange one token into another or I can add liquidity and remove it with one token, right? It's technically in a firm pool perspective you should arrive at the same state, but quite often you don't see it. Okay, I'm done. I think my time is gone, so who's the next speaker?

>> Thank you so much, Anton. >> [applause] >> Can't wait to write some invariants now? Um if you've ever if you've ever read a good