Bounding Rounding Errors in Integer Maths

Transcript

I'm going to speak about u rounding errors and um especially I'm going to speak about how to find the the the bounds like how bad can we round um can we round down or up. So yes. So uh oh yeah first of all my name is Jianis. I'm security engineer at chain security. Um I audited a few projects but anyway today we're going to disc so first to discuss rounding errors. We're first going to discuss um some common patterns like what's happening, what's going to be the limit, what where is it going, where is it going. Then we're going to discuss the volture pattern that we can see in 4626

uh volts. And then I'm going to show how to prove that we cannot uh be more far off uh than expected. And to do this, we're going to use Z3, which we're also going to see what this is. Um so first why why do we actually care about rounding errors? Uh well for me I care because it uh happens on all EVM chains um and uh where where on EVM chains we can mostly only see integer math uh natively and this always means that we are rounding down.

Um and um well this also is um often quite hard to uh guess. You can see some formulas, you see some math as you saw previously, but it's hard to say like oh we're going to round down but then we multiply then we do something else then stuff happens and we actually don't know um how far we're going to be because when we think we always think this is going to happen in real values. So when we when we imagine like three over two, we can easily imagine 1.5 or we can imagine some stuff but it's not what's actually going to happen. So if later you multiply then you're actually really far off. So we're going to see how we can a bit uh understand things um that happen on chain and also um usually this kind of issue they wouldn't be flagged

by any tools or even I think AI is quite bad at finding these type of issues. So it's good if we can reason a bit about those and oh yeah and last reason uh it happens quite often that there is a lot of money which is uh leaked by this um tiny rounding errors. So um yeah so what we're going to see is like this kind of patterns so simple of some at the beginning somewhat simple expressions um and the the goal is going to be trying to figure out how far can we be from the real value. So we're going to like see this value in solidity where when we divide like for example if we do like a is 10 and then we divide by three well we should get 3.333 something but

instead we get just three and then we multiply so then we're again like uh way way further away depending on how big C is. Um so this is what we're going to try to assess the difference between those two. Um, and the first one we're going to be looking at is the most basic one we are going to see today. And we're going to ramp up the complexity. So if we have a time time a divided by b, uh, then you probably all know that um the further we can be away is almost one. Like the worst case we can have is we were trying to reach maybe 3.99999 something. Well, we'll get only three. So the further we can be away is um is is three. Um, which is sometimes quite bad, sometimes quite

good. This we can easily reason about we know it's going to truncate just the the fractional part of the number. Um now when we have like the expression we saw before um this one maybe you also know how it it works. Um in solidity if you just write this code of course it's going to be first a divided by b and then the times c comes later. So as we said before the the a divided by b we can be at most we can have an error of uh of of one. So then we multiply by c um and this error also gets multiplicated. So we can be at most um c away from the real value the the the value that we have in mind that we

expect. Um so for example uh if we were supposed to get 3.99999 something then imagine C is is um C is four well we expect to get like something like 12 but instead we will get just nine. So then we get uh a bit uh further away. So basically anytime you see like a division um be careful because you might want to actually maybe do the multiplication before instead and uh like reorder the operations to get more precision. Uh but you also have to be careful about overflows and stuff. So there is things now imagine we have this and we d um um we could like try to guess if it does

anything. Um it actually doesn't. So like if we add stuff and everything we don't actually change there is it's not going to amplify the rounding error. It's just going to shift it a bit but it's really multiplication and division we should be uh careful about uh in this rounding errors. So now one which is a bit more complex um and uh and on on this one I'm going to spend a bit more time uh because people usually guess actually the wrong answer for this one. Um it's maybe not an expression we see every day. Uh we're going to see some expression that we see a bit more later. But so basically um in this one we have a over b and then we have

something a bit similar to before where we had a over b * c but now instead of the time c we have time c over d. And in this case we have c is smaller than d. So we cannot really amplify the error as before because before we had C uh which could be big and then we really amplify the error in this one. Um C over D is simply smaller than one. So you could guess um you could guess it's not going to amplify the error at all. And uh also there is no like issue with the parenthesis. We're going to do a divided by b then we do all this time c and then we divide everything by d. Otherwise C*

D would C divided by D would already be zero and then uh this is all zero right so there is no brackets error um and um interestingly so then most people say this this should actually round um down but we're going to be at most one off because we cannot amplify we have an error of one and then we multiply by something smaller than one so we just don't amplify the R well actually turns out we can actually be two um two ways off And this we can see um in this example. So in this example we have like uh a which is five and we divide by three and we get one. Then we multiply by uh c which is two and we get

two and then we divide by d with which is three and we get zero. Uh so this is actually a bit more uh further away than it's like further it's more than one off from what we uh expected. It's actually 1.1111, right? Uh so we we can actually be really further away than what we expect. Um yeah, so this is the kind of uh things we should worry about when we uh check the math in a smart contract uh because it goes a bit against our intuitions sometimes and this is also why later I will show how we can prove this kind of a formula. Um next we have the case where C is greater than D. Uh so in that case we a bit come

back closer to uh to what we have we had with just time C because now C is greater than D. So we can again amplify the error. So, it's good to think about like where we are in the like if we can figure out how big the numbers are going to be relative to each other, it can help us actually figure out how far the entire formula is going to be from a from the real valued formula. Um, yes. And then it turns out that the maximum error that you can get is sealing the C over D plus one, which you can somewhat maybe uh it's a bit similar to what we had before.

uh right times C. So this is the stealing of C over D and then the plus one also comes from the fact that we could have uh two ways of error in the previous formula. Um yes so now what I want to talk about quickly is because for now we've been talking only about absolute error. So we're one way off two ways off C ways off. So we can be we can be like a certain number of units of but what's actually interesting also is the how far we can be in like in terms of percentage. So like for example if we have a correct result like the real value is eight but we have a computed result of six then the then the absolute error is is two right the difference between the two but if we have like a if

we speak in terms of relative error we have like maybe eight and six and then like the the the the difference is like we're off by 25% compared to where we should be. So sometimes we do actually care about one way. We cannot be one way off or we want to do something if we're one way off. And sometimes we don't care if we are less than 1% off. Maybe 1% off is fine. Uh maybe maybe not. Um and now I want to talk about this formula that we often see. Um and this is the formula which comes from uh the 4626 volt from open zeppelin. So we have like this formula to convert from share to asset.

And basically it boils down back to this uh formula. And this formula we're actually going to compare this time because if we were to compare it to the real valued formula, right? We're back to the position a * b divided by c. And this is not really interesting. So we're actually going to compare this formula with the plus one to the a * b / c without the plus one. So what does rounding does do for us when we don't have the plus one? Um so the goal is going to be to compare the real value target of a * b divided by c uh compared to uh the open zeppelin uh formula with integer. So what we would have onchain against what we would

have if we if if we just think of a 4626 volt we usually have in mind this simple formula of a * b divided by c we have a share of the vault that's what we own and that's it. But that's not actually what's happening on chain and it's actually quite uh important to understand this kind of formula and how far can we be off from what we expect. Um and so the first question I want to ask is um like what is the maximum possible value of the difference? So the absolute error compared to those two formula and of course it can be quite big in absolute like if you have 256 bits of integer the the difference can be quite big. So um so I'm going to present like a small uh difference. This

is actually the biggest that you can get um with uh a b and c being smaller than a thousand. So it's like we have number smaller than a th00and and we already have an absolute error of uh 512. So, so for example, if you take a being 512, b3 c1, this might not be numbers that you see every day in a vault, but this is what you can have. Um, then the real value is going to be um 1536 and the open zeppelin formula gives us,024. So that's a difference of 512.

So if you just think I have a vault, I have a * b divided by c, you might be far off. So it's it's actually quite important. And if you think about relative error bounds, it's even worse because um you can actually be 100% off if you take small numbers. Of course, because if you have a being one, b being one, and c being four, um the real value is 1/4, right? We just have one * 1 divided by four, it's 1/4. The open formula is going to give you zero because you do 1* four and then you divide 1* 1 and then you divide by four, then you get zero. It's going to round down, right? So you can be 100% off for small number and you can be really far

for for big numbers. Um and now the question is those two we actually round down right because we divide so we round down. This is what you initially think and um the question is are we correct? Like the real value was 1,500 and we go to just a thousand. This one was supposed to be 1/4. We go to zero. So we round down. But is it always the case? Can we go higher? We have we have a division where we run down but we do have some plus ones. So can we go higher than the real value and the answer is actually yes you can go higher. So this is a bit unexpected when you think about uh we just run down but no actually we have plus ones. So

for example you take a being the numbers are a bit less nice. So uh but yeah you can verify the math right? If you take a being 189, b1 c20, the real value you should get is 9.45 and the open zip pin version gives you 18. So this is actually nearly twice as high. It's it's really far from what you would expect. Um now [snorts] now now uh what I want to show is quickly how we can prove uh those simple formula like prove that um we cannot reach a difference of three or we cannot reach a difference of d we cannot be that far from the real value and to do this we're going to use a z3 which is an smt

solver. So this is basically um a tool which allows us either to find a counter example if there is one or to say there is no uh counter example which exists. So we will say SAT for satisfiable or unsat um and uh yes this is uh basically like fuzzing where you would um try to find a counter example but in this case uh we know if we cannot find one we know that there is no uh counter example. So we know this cannot be satisfied. So the so what it's going to look like is like a small piece of code like this.

Actually this is all the code you need to prove uh a divided by b* c and to prove that we cannot be further away than c from the real value. Um and I'm going to walk through you through the code quickly. Um and basically the way it works like you just import z3 right then you have a bc you define your integers the the ones we have and you can make some bounds. So in my case, I just want them to be bigger than than one. That's that's enough. And then I just uh put the two things I want to the two formulas I want to compare. So the computed one on chain where I don't do anything. It's going to do integer math by default. And the real one where I convert from like two real values to get the actual real um the real value result

and then I can compute the error and the absolute error. Um and then I can add a new condition. So basically what I do is I add I have this solver which is the solver from these three and we're going to solve for all these um inequalities or conditions. Um so now we have like two condition like or four conditions right we have those four and we also want the absolute error to be um greater or equal than C um where the absolute error is defined like this. So you just can put some Python math. You put your variables, a bit of Python math what you want to look at and that's it. Then it's going to tell you, you can call the function check and it's going to tell you is it satisfiable like can we have A, B and C which are going to satisfy

all those conditions or can we simply not and if it says you cannot then it means that there is not a single A, B and C um which are going to satisfy this. So in our case we this is asking can the absolute error be greater or equal than c um and if you run the program it's going to say uh unsat this means that there is not a single a b and c which are going to give you an absolute error bigger than c. So you can be sure and this is for a simple formula right but you can imagine that if you have a bit more complex math or if you have operations in a different order it makes it really easy to say um yeah which number you cannot reach and

if this is fine for you um and now like to be sure it works like because you now you don't see a counter example you don't see anything you just see unsat like can you really believe it maybe I made a mistake in the Python script maybe there is something wrong well maybe your intuition is like you can be maybe like 999 of C. So you just do the same thing, but you replace um C by 0.999 of C. And now instead of saying unsat, it's actually going to say SAT, and it's going to give you a counter example. So you can be at 0.999 of C with uh this ABC.

So makes it quite easy to to check your formulas. Um let's look really quickly at a more complex one, but basically this is the O formula. we just saw before and the goal is to prove we cannot be because I said we can be higher than the this for formula compared to we can be higher than a * b divided by c and so we have the same setup right we have the same computed wheel where I put this and now I want to show that we cannot be um 100% off so we can be twice the real value this is going to show again um unsat we cannot find ab such that we are twice as high as what we should But we can find a b and c such that we

are times 1.99999 the real value. Um so we can be nearly as twice. So twice is like the bound how far we can be off in terms of uh rounding errors. Um yes and this is actually all I wanted to say today. [applause] Thank you Jianis. Uh do we have one question for Yiannis? >> Yeah. Um my guess is that if you have a very complex problem with a lot of operations probably solving this is empty hard. So

I assume that you cannot have really big problems. So could you could you share how far you can go with with this solver? Have you do you have some experience? >> Um uh no this is actually quite hard question. How far can we solve? Right? It depends of the power that you have.