Optimizing Code Without Getting REKT

Transcript

I will share the session uh so our first speaker is natano from sertora and he's going to tell us about everything nice you can do with formal verification to avoid getting wrecked [Applause] the title of my talk is uh much more modest just improving the security of defy mat libraries it is back for preventing easy specs for preventing complex bugs um so let me explain the plan for the talk I'm going to be talking about four

things the first is kind of an intro to define exploiting the trade function the second is a prbmat library bug we announced a few days ago the third topic would be how did we find it and the fourth would be one form of edification is easy so okay let's begin so I assume that a lot of people have seen this kind of slides before but I'm just going to like talk about them a little to touch base um okay so what is an automated Market maker so I should first say what is liquidity well assets have as well as like a wharf they have their tradability

which is the reason that you probably like uh thank you so you can't really buy lunch in the cafeteria with an antique 17th century piano and if you want to do that that's probably means you're in a bad situation um so assets needs to be basically what market makers do in classical Finance there are people who are willing to trade one asset for another we're providing this ability to like convert two types of assets to each other in defy this is done by an automated Market maker um often and we have liquidity providers which could be anyone they give in the most basic model of this we give a pair of tokens token

in token B and we get back an LP token which you can think about as a receipt to certain percentage of the amount of the amount of tokens in the pool and we have Traders Traders given some amounts of token a and we get back some amount of token B right um any questions so far this is familiar great okay so of course the main question you should ask is how does the mm know how many B tokens an a token is worth right and the answer is we don't need any kind of like Oracle or anything else because in essence a market itself is a price Discovery mechanism and for a mathematical perspective virtually every kind of like uh

automated Market maker that's currently in existence I think on the chain is an example of a constant function Market maker which means its trade behavior is dictated by a function that has these four variables and it Maps into real numbers and these numbers are X is the reserves of a tokens why is the reserves a b token Delta X is how much the trader wishes to like give and Delta why how much he wishes to receive and the key point is here is trade is executed if and only if the enemy believes it's profiting which means it should be that this C of X Y Delta X Delta Y is bigger than c x y zero zero which means if trade was not carried out

so any questions here maybe I should give an example which is very this is much more familiar right this is the classical case right everybody's happy um you have cxy Delta X Delta y uh equal X Plus Delta x times y minus Delta Y what does it mean it basically means we want to preserve the product of the reserves to be an equal number right it's x times y equals K that's everybody's favorite the idea was Martin cooperman evitalik buterin and it was first implemented by uniswap in 2018 a lot of people since then so this is an example of a trade function there's nothing magical about this x y

equals K formula and there are many other kinds of trade functions some of them are quite involved mathematically and different trading functions optimize the underlying properties of different token pairs okay so what happens if there is some kind of a bug in the computation of the trade function so in arithmetic flow in the trade function would allow an attacker to basically Force DMM to systematically accept unfavorable trait maybe just a little but consistently the key Point easier with his money has to come from somewhere so this is kind

of somewhat of a subtle attack because the number of LP tokens each liquidity provider is holding Remains the Same in the end of the attack what basically the attacker is doing here is kind of draining them of their Wharf a rough analogy to this is inflation okay it's a rough analogy uh the liquidity provider still has the same amount of currency in their account but it just can buy a lot less with it okay so the key Point here is with computational errors in the trade function would enable an attacker to drain the funds the liquidity providers deposited into the pool um

okay I should probably say this is not really restricted these type of attacks to amms I took this example because I felt it would be very familiar to everybody it's also true for you know for landing and borrowing markets right we know from erc4626 we're telling you that oh yeah you should definitely make sure that the rounding direction is in specific opposing directions to make sure you're never violating this like trading it's called the trade function the mm invariant or the CFM invariant in different places in the literature so how much damage can a simple rounding error cause that's like famous last words

there's been a bunch of like attacks where was the alpha more hack where was the SPL token lending bank which was stopped by the developers and so in a program Library there was the ELD HDL HDL distribution bug and I think two recent ones 100 Finance the second minus Capital exploit okay so any questions so far okay so I should speak about that bag it was such Discovery is a critical of our built in a non-life code of a leading D5 protocol and upon further inspection we realized that it's the root cause was actually a public library function well they've signed it laid dormant for almost two years

it's present in every version from 1.05 to 4.0 and it's temporarily fixed in 4.01 where there is a warning if you can see in the net spec of it says that this is wrong and we'll get to it in a moment and the long-term solution is going to be part of a roadmap to support multiple rounding modes in prb mat so since I'm mentioning prbmatt I should probably just say a few words about it in case you guys familiar with it it's a solidity mat library for advanced fixed Point computation it was written by Paul Rosenberg and it's based on work of remote on the algorithmic side um it's popular it's fairly complicated it's very very gas efficient it makes

heavy use of fuel it has a lot of like buy tacking tricks it has a lot of matte magic and a bunch of number theory in it it's well written documented it's actively maintained it has a lot of commits a lot of unit tests it's really very good um and I think this is to the best of my knowledge the first uh Library bug that was found by a semi-automatic tool maybe I'm wrong I don't know um so okay now let me explain the bug okay so I'm slightly simplifying the algorithm here for the purpose of presentation so the goal of this function is to compute the floor of X Y divided by D

with full Precision without losing any precision so you separate the signs of the absolute values that's the first and when you compute the absolute value by call you basically reduce to the unsight case by calling Maldive which is a function of the compute floor of X Y divided by D on the absolute values and then you compute the overall sign by taking zor on these signs so to give an example you take X you take x y equals minus 20 minus 13 7 so you get 20 30 and 7 1 1 0 and the absolute result is the floor of 85.714 it's 85 a compute the overall sign and you get the right result the problem is

the second step is logically wrong when the absolute value is smaller than zero rounding taking a minus a flow a CO is an example if you take minus 180 114 you will see that like the absolute value is 12 and what you get is minus 12 but if you compute the right number it would be -13 so for example you know it's possible you should have gotten 0 and you would return -1 okay that's the bug and it's in how did we find it okay um so formal verification process what is formal verification well very

roughly speaking you have a bunch of invariants any bunch of code and you put it into a big machine called as a store approver and it throws out either proof but every behavior is correct to the spec a timeout over the behavior vials the invariance this is not a fuzzer basically you convert the entire code into a bunch of logic equations and you try to prove that the behavior is correct like try to prove basically a theorem I should probably say any questions so far okay so the other point that I want to make here is it's basically spec writing in general is hard work okay and therefore it's kind of expensive um this is

like security researchers you know they have to do their work purchased on a pile of gold just a fact they do the best work this way but this is not always true encoding integer equations is really easy and for automatic libraries basically this formal specification just right themselves okay here's the example of the of this is the entire like uh spec we detected this bug it's basically automatic um the only thing that you're seeing here is basically I call multifind Computing code I can put the code result I compute I compute the result in logic and I ask Arvest the same the only thing that I need to write is this thing now this

looks like solidity feels like solidity it's not solidity it's we worked really hard to make it look like solidity this is smt basically okay what you're seeing it to Matt int are unbounded integers we're not U into 256 will represent the logical numbers in Z okay very present arithmetic integers okay and the other thing is like well when you run on this type of like arithmetic libraries you also get really nice counter examples like the counter example I gave basically just came directly from like the prover just spit out this counter example so you get x y and d and you can just put this thing into remix for example and just check where things go wrong

so yeah this is actually all the spec you need to detect this problem um you don't need anything else um and you don't need even access really to the prover you can there's a pay if you go option you can just like you know just run this script just pay for the minutes and just find it it's a bit surprising like uh that this is found by such like an easy spec we were surprised mat libraries are the foundation basically of D5 but were not easy to get right I think

that's maybe the takeaway these are things that Auditors usually don't like looking at I didn't include here the code of how the entire computation looks like but it looks there's a lot of like low level stuff there is a whole bunch of like number of favorites easy to get lost and to miss with the point is like the entire logic is actually incorrect um so rating specification helps ensure that nothing slips between the cracks so this is a very very very well written Library um and it has unit tests it has everything but because if you make often you do like frequent commits but sometimes you refactor a function and you forget to put some kind of unit test to that specific function that is the

function that you find a plugin so I think even just the process of like you know touching a base and checking in the end writing a formal specification about everything in the program is supposed to do sometimes can find bugs even without any automatic tool and the other interesting part is I think the specification really easy to write um I should say that this bug is very common it could have probably been found by a father like easily but in general we also found some other bugs there that are I think less interesting that you can't really Express I think using a fuzzer the point is like it's almost automatic in this kind of mathematical functions to write what the spec should be and to express it and you can't

really write it in solidity because if you could write it in solid you would not need a matte library to extend solidity's functions to make it right um again I think in the conclusion is in retrospect kind of obvious so if you have mathematics or economy like this kind of like core parts or just do computations any form of edification that's like a really good match you have some function you don't know what it does you just throw it into the prover and it either tells you if it works or it doesn't um it makes sense I think a lot of sense in this case to utilize semi-automatic tools for increasing security okay thank you uh questions [Applause] uh thanks uh so the question how did you

come to the idea that round and down for negatives means pushing further away from zero not closer to zero I think that's the question of in the first place that defines the difference between the two approaches that you've at some point decide that you have to make the number more into negative rather than closer to zero so thank you for the question so the mathematical definition of floor floor has like a very Thor and sealer have a well-defined mathematical function they're basically right rounding towards minus infinity I mean the definition that appeared in the net spec was you need to round down okay what basically was changing version

4.01 is the observation that like it actually does not round down uh because more the Maldive is based on the co on the algorithm veteranical blueman road which takes floor but basically rounds towards zero because it is an unsigned numbers and when you modify it and you want to keep it efficient then you make it like inside numbers but then basically what you notice you can no longer it no longer gives you like floor it gives you basically rounding it towards zero which is not always what you want for example if you're raising it to some kind of a monotone function in a trading function Etc then it gives you the wrong result you're going to lose money from it I mean I don't know if it answered your question I mean the definition of floor is like rounding towards minus infinity definition of Cl is rounding towards

plus infinity I mean that's a mathematical definition maybe I did not understand your question um this is floor yes that's the yes so yes that's what's definition that's the way should I go okay um would you say there's any trade-offs between writing the specification and the CVL language versus maybe like a lower level proof assistant if there's anything that you know that you're trading off or missing from what you could get by specifying like the whole thing in a proof assistant

I mean I don't have a lot of experience with proof assistance I think the main advantage is like if I remember correctly like proof assistance like K Etc are fairly are much harder to like you know to work with and I think like you need a lot more effort to like do the verification so it might at this point like you know be actually easier to just go and do it manually I think the advantage of like CVL is that it looks like solidity and basically the specs of mathematical function are just literally okay take what's in the Nets pack throw it in and check like you don't need a special verification engineer you don't even need to put considerable amount of efforts I mean you just need to do it it's like easy hi nice talk

um you I was just curious you've been using the Satora approver to handle these math libraries but a lot of these libraries have a lot of non-linear computation um I'm just wondering which is like notoriously bad for smt I was wondering if you could just talk a little bit about like you know what you're doing to address the non-linearity maybe you can talk and how sertora approver does on on those kind of um yeah so that's an excellent that's like an excellent question I'm very happy somebody asked that thank you um so it depends so for algebraic functions like quotes Etc we have Johan's work which helps us like actually we're able you need to do some manual work but you can like summarize for example square root and you can prove separately prove that the square root is actually equals

you think about Newton graphs on iterations and loops and desktop type of stuff right and like hensel's lifting Lemma so yeah you can actually rely on for square root for example you can now Johan's work which proved it it did like amazing work for really really like transcendental function like exponent and Lan it's more complicated I think in this case you really need to like either Black Box some of the things and either do like a very very careful step-by-step verification even manual or like use a father or something else you need these things you need to Black Box out but if you're talking about algebraic functions there's like something to do we're basically out of time if it's a quick question we can take it

thanks um so the Satora approve is obviously really powerful Tool uh is it open source and if not are there any plans to open source it um so I think can I direct this to muli no um I don't know how to answer that question of like long-term plans I think this is a question for my higher-ups okay let's uh thank Nathaniel again and take this question offline