DeFi Invariants: Examples and Challenges

Transcript

uh hello my name is Anton I'm from chain security yes we are started in 2017 and keep going as a like and yeah we are quite long in the game so to say and uh team rotation is surprisingly low so we are almost all the same people keep doing Audits and securing the easy room I mean we are I think at this moment still somewhere fifth place on the yeah zero Foundation bug Bounty leaderboard and yeah we are trying to secure whoever comes to us for our advice and

also of trying to find bugs in our like so to say free time uh you know maybe some people know about read-only re-entrances this was kind of discovered by one engineer of ours and yes uh I mean the previous speaker told like it's really hard to navigate this field in terms right and here I want you to tell about this kind of um mental model like we are sort of we're initially a spin-off of eth tour University it's name is uh finally looking but it means like something like Federal University of uh Switzerland but uh basically one of the

things that I believe like developers and Auditors no matter what you do I mean I think anybody who is more or less involved with code can profit a lot is this kind of mental models how to deal with complexity how to deal with uh codes that is hard to reason about and one of them is like invariance so I mean in nutshell like what you see is like a definition of invariant it's just some property of a uh you know case program but it's a smart contract that is always true right so one of the sites kind of really intuitive properties that you might maybe see first time is that maybe total supply of your C20 token if

you have experience with your C20 tokens is equal to sum of balances right this kind of makes sense to do because you don't want to have like tokens imbalances but not accounted in total Supply right so here I want to use a bit more complex example like it's compound compound V2 I think actually it's I would say not so popular nowadays I really don't know how they're doing but uh like we started long ago and when honestly we started in 2017 uh most of the audience most of the contracts we reviewed this was like here c20s this was big complexity in most places and then like this time like when people

sort uh sort about this composibility of tokens they started to think how we can create systems has utilize this underlying simple uh Primitives like here C20 tokens what we can do with them and yes exactly compound is a thing that you can do with uh primitive here C20 tokens it's basically lending and borrowing platform so you have here uh die this is like a stable coin I'm going to use this as an example of that's kind of a token that compound will be using and then C die is basically a token that compounds creates internally

when you want to when you are landing uh the die to compound right I'm going to show later why they are doing so like uh but so to say you can say that dye is some external token and CDI is a token native to compound itself and of course like there's going to be either it's a native token uh yeah you're as well gonna see why we use it okay now like once we saw like these three basic blocks let's first go into the first part of our uh like compounds dive in right and I'm going to just explain the system and then like after I explain like your steps I'm gonna try to show you how you can kind of abstract the

complexity out of this complex quite a complex Behavior with quite small and simple formulas that's easy to understand uh okay first it's in compound I told you it's Landing boring platform what is landing Landing it's uh you can say a process right when a party some lender it could be you with your Ledger wallet or metamask or whatever you're using you have some Diet tokens lying around and you basically uh want to give them give them to give the get the yields right I mean if you know the to this this is exactly why people are landing they either pull putting it into some liquidity pools or something to make the

kind of capital work right and like if you see it's usually if you put them inside so this is we're gonna call like Supply this kind of Step if you're supplying tokens in exchange you're getting C die right this is like a virtual talking so to say that represents your like position inside this compound system right and after a while time goes and you actually want to get your gains from the compound right USA yes I'm done with the farming compound so like I won't actually need dye because die you can use for many other things like withdrawing from exchanges centralized

ones and actually like buying pizzas and this time how compound works why you actually incentivize to give your tokens to compound is because you'll get more right you see here you get like 105 tokens and not the initial hungry that you have to put like so this time uh like when you be withdrawing this is processor the code you will get more and this is would say one of the simplest invariants that you can kind of check when you are doing audits or as a developer when you're writing a code right and like a bit more complex example but in the same

nature of invariant is that price of diet to see that this time should be monotonically increasing right so there should not be moments like when CDI is not like let's say I put a hunger die and I give I Got Back 40 CDI there should not be a withdrawal where I'm actually getting less a die right I mean is this is compound invariant it's not doesn't hold for all kind of protocols you're going to deal with I mean even for example I know certware who versus other in their case there is some potential like rebasing that actually

permits this balance to go down but in general as a general rule like this shouldn't happen in most landing borrowing platforms and this like exchange rate of uh you can say diet or C die like or any other token to like internal share that represents the stocking should always go up uh now we're gonna go on other side of this compound it's borrowing borrowers are exactly the parties who want to get uh like the collectors the tokens that you have deposited and they are expected to return more for like ability to use uh to use your tokens right in this case we basically

cannot use die again like to get to borrow from compound we need to use another type of collateral in this case uh we're going to choose like a native either right and as example here borrower can supply collateral is easier as I told and get back he can get a die like a token that I told you that's more usable than maybe for his needs the easier right and his either is not burned it's not he he didn't lose his either when he deposited the borrower he actually later can repay and repay with some extra fee right extra percent on top and get his

collateral back right so this is like a replay uh in this case uh you can see like we are returning a bit more die right and this basically just to spoiler you like and people who know this it's like quite obvious profits of lenders I come from borrowers right this is uh like system itself doesn't print new diet right it's only can kind of redistribute what lenders uh of what borrowers kind of have to put on top right and invariant for this is quite simple as well it's a repaid amount it should be more than borrowed amount

right it's like you want to you want to borrowers to pay for ability to use your your die right other type of collateral that lenders had put into the system uh yeah and uh like if you just paraphrase this what we wrote here like this is actually the same exact equation uh but we just are adding extra components there because uh there exists actually a certain term like prices right you don't want to give hundred either if collateral if either only costs uh 50 die in if you use some other exchange right it will be really bad

deal for a compound as a protocol right you don't want to kind of distribute assets without uh like proper backing so that's you want to be sure that borrower at least puts enough funds for like incentive to repay right and the result like uh the previous repayment was a borrower amount basically results that uh like collateral uh multipliable price would be more than you're boring right this is like invariant for like repayment and actually like uh yeah I touched the business so I could repay you should be incentivized to repay and exactly uh

what happens if let's say we have at this moment uh I don't know this I can I have not introduced full variables so people who know maybe says it's not a possible situation like like die is usually one-to-one with a US dollar right and for let's say one either I can get hungry die right at this limit of a situation and exactly if price becomes Hotel reason 50 right it's much less than actually uh actually the amount of dye currently borrower owns borrower has no incentivized to repay so he will be actually not repaying right and this is um like not good for protocol right because as we supper previously we want

lenders to be sure that their money are working they are like accumulating fees and so on we don't want them to be like uh not happy and lose their tokens right that's why basically there exists another party called Liquidators and Liquidators are like a party that can repay adapt uh at like assuming like prices they are like developing um developing with some uh like how to go it's a function over time right you at some moment know that's like the borrower doesn't have enough uh like

enough collateral to repay the depth right and this moment like in compounds something starts something some process starts that is called like uh liquidation auction and it allows Liquidators to like basically liquidate uh the borrowers position by repaying die you see like he needs to return what borrower has borrowed at some like smaller price and as a return he gets a collateral collateral that potentially can worse more right [Music] and the and like uh invariant that you want to establish in this case it's like to make

sure that Liquidator is uh has all the incentive to uh like liquidate position is that basically uh the like I couldn't read formula it's quite big collateral amount multiplied by price of collateral uh multiply like color authorization ratio I'm gonna tell us a bit later it's more than border the mountains price so in our case collateralization ratio it's the factors that resulted in uh borrowers amount here not to be hungry but to be 80. uh while it's 80 it's because you exactly want to have a safe Gap save Gap like in time in which Liquidator can come and liquidate your

position and for that exact reason for 100 USD tokens you're not getting hungry this examples that we had before they're technically like no protocol works like that I think characterization ratio of one is a thing but it's quite a rare thing in most cases you will get something like 0.8 in this case which basically means that borrower cannot fully utilize uh value of his collateral he can only do it partially but as a result particle gets sort of like a guarantee you can say that if price of collateral drops below the kind of collateralization ratio time

price of collateral times the amount of collateral then basically third parties like Liquidators can come and replace the depth they are really motivated to do so because they actually you can see getting like either is 99 right but we think I have a type of there because you could they should only repay 80 die and not 99 yeah sorry about that because you're not paying full price you can actually like pay only what the borrower holds yes and like prices can be different there is an on-train off chain but more or less it's always like some function over time and this is great security

considerations needs to be put into what exact price each protocol needs to put but more or less like you can say the heuristics is such that you want to be able for Liquidators to be fast enough to liquidate the positions what if they don't liquidate there is a like bad adapt as a term exists that exactly if like for example borrower has borrowed 99 die but Liquidator repaid only nine Thai right this nine die will be considered as like a bad debt it's basically protocols users really have like a special pools to protect from Bad

depths like they are basically funneling parts of their like protocol feeds into the special pool that in case if they like accumulate that depth they can repay certain risks right but in general they never want to have any bad depths on any of their borrowing or lending positions right and there is a huge effort put into like analyzing what exact culturalization ratios needs to be in each system if it's more not so Security in like defy sense but it's still security and devices but it's more like economic parameters and not like software code that can be broken right

okay and yes for like this desired invariants that you would like to hold is that culturalize them out multiplied by price of collateral price in this case you can say it's like indoors right and multiplied by characterization ratio should be borrowed them out and press this is the old formula that you saw and basically what it like really means is that uh like intuition behind it it's it's kind of one of the things hard to get is you all see this formulas and uh with time intuition starts to build up and here intuition is that basically what borrower puts in should be less valuable

than what he gets out right and yeah this is I think uh enough for boring we can now go for connecting both pieces of the puzzle together it's lending and boring so there's lenders who come and who die there is borrowers who come and um like get die and put another a set as a collateral and later they repay and their repayments go and basically result in profits of lenders right and yeah this invariant if you like sum up stuff on the left side on the right side

on the left side it should be equal right because the inflow of a system assumes there is no like protocol fees uh it should be like Net Zero and it is like borrowed Supply Plus board repaid borrows uh should be equal to uh provided Supply Plus collected fees right so this is what I told you working the very beginning that's value doesn't appear from nowhere right compound doesn't mint either compound doesn't mean time and it's like basically a barrel where some people put their assets some people take it but Barrel is full only because some people put it

there and Barrel is not empty because people have not taken everything out right so this is how you can have like an intuition behind like what this formula means right um okay why you need to know about all this invariants and uh like what do they actually have to do with like writing code or like auditing code or many things and this is exactly that you need to utilize these things for first testing second like even if you just writing code or looking at code you need to consider the things for each function it and it's honestly speeds up a lot of the process work instead of looking like okay what's

uh can happen with the system which is basically formalize this invariant and just you go function by function and check like does this function [Music] break invariant or it's actually a good and maintains it right and in this case in in many cases like invariants are like some things that you can test only if you do the top of the pyramid it's like if you do like system-wide test in rare cases like you can do like invariant testing for and test like even unit testing I think there was a much of good talks like you know by Trello bits who

told like about this tests and that you need to go for not only 400 statement coverage but also to go for like meaningful tests that tests and one thing of you can do meaningful is testing variance of your system um yes there's also a bunch of other more fancy ways than like regular tests to test the invariance one of the ways is what I'm personally like fun of is like property-based testing yeah I showed some examples how that of libraries and like Builder tools that can help you with like writing such tests I mean python is brownie Foundry is like where you can write test

directly in solidity uh truffle it's a bit harder there's like only first check exist so far as I know but nevertheless like property best tests are really good I'm going to tell you later what exactly that is but stateful testing is another variant of property-based testing but where you like maintain a state and formal verification and monitoring is kind of uh super Advanced kind of testing technique but it gives you the most guarantees and if you want to go the Last Mile and basically be sure that you're safe it's maybe like exactly what as a protocol

developer you want to do monitoring is like more if something bad happens you have a way to basically pull the like stop and like prevent system from being like abused but it's not most likely the way you want to deal with the kind of problems in your system because this is like a lost Resort kind of system uh okay and regarding property of its testing I kind of mentioned it but actually I have I should have reordered sites uh that's basically if you consider a unit test for like something like deposit function usually you just run one value through it and

you just see if it's like passes or fails maybe you have after deposit you're actually doing some query sense like us asking smart contract if the state is okay right if like if I want to deposit I want to see that something total collateral in the system has increased right and this is basically your properties that you're testing property based testing is pretty much the same but uh you are for like bombard charging your uh like unit test with many many random inputs right and you're still checking all the same properties but just not on one input but on many many different inputs it's still

like a good uh I think it's not from Turtle Beach though like to limit basically if you're using really big integer values or really small integer wherever there is this basically Corner cases that you want to capture but in the in the in general this is like really good uh testing technique and yields in my like experience a lot of results surprisingly with little time invested sort of especially like for us Audis are 10 pounds and it's always trade-off between like testing the clients code and like looking at code ourselves yeah I think I'm done you know if I'm on time uh yeah I guess questions if anybody has

36 there is a question thank you for the talk um I was wondering about the property based testing how do you choose do Corpus that is used for injecting uh sir sir what do you choose the Corpus like in on the next slide you have like 110 and I was wondering about the Corpus and also the seeds that generate maybe yes okay um so this is like really depends on Library um I mean you can for example tell you about black brownie it's basically uh you're writing tested like in Python and there is a like about established library in Python code like hypothesis

that basically uh allows you to annotate certain input argument of your test as uh parameterize test with a certain strategy the strategy you can specify minimum value maximum value you see it that's exactly like where it can be specified and then this test will be basically run multiple times and it will be every time like a random value from this parameters of your strategy picked yeah I mean I I guess it really depends on like libraries right I don't know what's Foundry honestly doing zero I can only like speak about brownies just because I looked really into internals but more or

less I think there is a standard this is the way of how things you are doing is the same like you basically have a special way to write the in like testing library that certain tests needs to be needs to receive random inputs yeah sensors yes I was wondering about how to optimize actually the good choice of corpuses oh this is like really really good question okay good uh so like in my experience it's um like you know for a given function that this function somehow mutates the state right and this uh like mutations of States they are usually and you can

end up in a bunch of new other states but for example if you have let's say in our case whatever like deposit function you can have deposits that would say makes your cauterization ratio healthy again right or it makes your cultural Insurance here unhealthy like if you maybe like withdrawing right so you basically in my experience it's best to look a given function and see what can be possible results right and then maybe even if I can Target the various such a way that you say okay please I want to deposit exactly enough assets

with some random parameterization around it so my characterization ratio becomes one right something like that and then you kind of sort of uh you can say trying to fuzz around edge cases right you you most likely from like system you know like edge cases let's say like even transfer functions like you know maybe critical Parts is like when you're trying to transfer more assets than somebody or like the somebody has right or you're trying to Mint really really big value right this is where usually problems can happen right and yeah it's really like protocol specific yeah you can

[Music] had like really one hard property we've had too fast and they're like exactly was I could say uh uni swap will be free kind of system where you could uh when you're swapping you can swap and cross the tick or you can swap and like not cross the tick right and then you were exactly trying to uh give all this values as a pool of arguments to get from right and we've basically wrote a property that we're testing that okay if I'm crossing the tick liquidity should drop if I'm not crossing city click it should stay the same right and this is like basically helped us to kind of find some hi um on the previous slide where it

said um formal verification how does that differ from the others or is it like an umbrella term did you mean something more specific oh yes sir I guess yeah I mean it's it's really like a white term but what it results is um you are having usually like high level specification of your programming system right it's maybe like I want to create a token and in token you can like mint and burn right this is like in playing English I have a specification and Next Step you do you are formalizing this planing specification into formulas there's usually some like special languages how you can express your

properties exactly like for example for tokens you can a single extra toward you talk like you can have this kind of rules that tell you if user a transfers hundreds like X tokens to user B balance of user a should be decreased by tokens and balance of user B should be increased right so this kind of formalization happens and then afterwards uh there is like different ways how you can basically uh create a model of your contracts right it's basically you can say Mass formulas instead of the real uh real bytecode right and your former verification basically checks that your specification

together with code is something that makes sense right because it's really like for modifications the strongest of them all because in all previous values and like here we are still poking dots in our like State pace of all possible input values that you can put into this deposits right it's like you ain't it's two to 256 sorry it's like too much you're never gonna have it like you know count to it if like University collapses and so on right basically formal verifications is kind of tool that allows you to kind of really know that your function depends good on all widths of your arguments or to say right

how it does it because they're using like symbols and formulas instead of the real values thank you what are the difference between the first testing and the property testing which testing stateful and property or property testing and first testing what are the different fast testing it's actually almost the same there is like I think uh like there are many people who kind of especially like in science who are

really let's say Zeal is about the terms so fasting usually in their terms means like you are doing Black Box fuzzing meaning that you don't have idea about internal representation you don't have idea about internal properties property testing is basically fuzzing but you have idea about what exactly system is built off I guess I told you like you have idea about possible Transitions and you try to like basically guide your fuzzing into this edge cases right this is basically it is in most cases people use them interchangeably and I think if you open like Foundry documentation they basically have fast

testing and then the next but the HTML link has property best testing results kind of synonyms I would say in crypto community thank you thanks for the talk could you please discuss the applicability and acceptability of monitoring and also what exists in terms of tools for this uh yeah I mean we had the experience with some monitoring uh I think we are like worked with Forte a bit and like try to see how that works I mean the only problem with monitoring

in my opinion is that hackers are really proficient about the ways how you can like deploy transactions right or you can execute code in many cases there is like Mev Services it can be used to basically execute transaction such a way that you see it only if it's already happened right this in most cases too late but in some cases if protocol especially designed with a ways where like for example you are limiting throughput of tokens from like from optimism to main networks for example maker has said for their like teleporter

contract and then in this case if you see if you monitor like some properties that what amount of tokens has been moved you may have like some like alerts to save you but things happen but in most cases uh like people don't in my experience don't Design Systems where they have this pulls the clock kind of uh safeguards right and as well like in in some cases like you can see people okay we have monitoring tools hack happen and they say okay we detected the hack right but in reality it's like a bit too late so yeah it's it's really uh Works only if you design

your system around monitoring right if you really put a lot of like this let's say rate limiting uh things around or you pull put this kind of circuit breakers then like if you detect you can circuit break basically this is my take on it thank you