Tackling Rounding Errors with Precision Analysis by Raoul Schaffranek | Devcon Bogotá

I'm Rahul Shah Ranek and I work as a formal very very formal verification engineer for one-time verification and today I want to talk to you about rounding errors and what we can do about them. Um so, very roughly speaking and I'm really over simplifying, uh there are two things that can go wrong when we do um approximate arithmetic in contrast to exact arithmetic. The first one is our the rounding error that we do is just too big, too far away from the exact result and that is a problem in itself. But that is not the topic of today. So, I want to talk about uh the second thing that can go wrong and that is Um what can happen is that you want to approximate a value from below or you want to come from above, but you do it in the wrong direction.

Like uh In other words, you want to round down, but you rounded it up instead and that can lead to severe security vulnerabilities. I will show you some examples that you will recognize maybe and then um but I'm not going to work on these real-world examples. I'm working on a like simplified example um uh and make sure to understand like the two-way trading problem um because otherwise you won't be able to follow my talk. Everything like get to this point, stay with me until this point and then you can make sense of this talk. Um so, uh rounding errors um they are well, we need to accept them.

We cannot do uh exact arithmetic on the blockchain. It's it's not feasible. So, and we found rounding errors in Uniswap um and luckily this rounding error was fixed um before Uniswap V1 was deployed, but I leave it to your imagination um how uh the blockchain landscape would have looked like um if this bug was not caught during an audit. And then we had like uh two more examples, Solana token and the contract in Solana token stable swap. Um and there So, the um these bugs were actually caught during like while these contracts have been deployed and at a peak time there were like 3 billion assets at risk.

Um So, luckily again uh these were not exploited by the but they were found by white hackers uh before any serious damage could have could been done. Um so, uh I cannot get into detail into any of those, but like I promise you if you follow my talk, then you will be able to visit the links that I put on the slide um and you will be able to make sense of these exploits and and and like how all these vulnerabilities and how they could have been exploited if they haven't been fixed. So, um I want to show you the two-way trading problem and um I promise you this is like the most mathematical slide on my uh on my entire talk, which is strange well because I'm talking about rounding errors, right? Okay, but um I want to introduce to you to my imaginary friend Alice. She's right here.

Hi Alice. And I will demonstrate to you the two-way rounding problem uh the two-way trading problem. So, first I'm going to offer Alice a trade and we do it with exact arithmetic. And then we doing we are going to replay the the replay and then we are doing it with rounding. So, Hi Alice.

As you basic scenarios, we have two currencies. We have dollar and Gil. Gil is just a fantasy currency. Um and we have an exchange rate currently uh that says I can get like um two Gil for $1. So, exchange rate is two.

So, I'm Raul. I have one Gil in my pocket. And this is Alice. And hey Alice, do you want to trade with me? I can offer you one Gil.

How many dollars do I get for that? And Alice do the calculation. Alice says, "Raul he gives me $1. Uh he gives me one Gil. So, I need to divide by the exchange rate.

Uh so, you get one you get half a dollar back from me. So, now I have half a dollar." So, I get back to Alice and say, "Hey Alice, I don't want my half dollar anymore. Um can I get my Gil back?" And I offer Alice the uh half the dollar.

And she does the computation and now this time she needs to um to to multiply by the exchange rate and so she ends up with one Gil. Everything went fine. I started with one Gil and I ended up with one Gil, right? So, now let's do the same thing with rounding. So, and for simplicity, I'm just rounding to like uh there's there's no decimal no digit after the decimal point.

That's just for simplicity. Um so, now Alice, I'm Raul. I have one uh Gil to offer. How many dollars do I get for that? Alice do the computation and but she does a rounding error.

Um Do I have a laser pointer here? No, I don't. Um so, she does a rounding error in this computation. So, uh we divide two by one. This gives us two.

And then we want divide one by two, which gives us 0.5. And we are using uh rounding to the nearest neighbor here. So, that means we are rounding up. Um so, that means I get $1 back from Alice.

So, now I have $1. Uh, I go back to Alice and say, "Hey Alice, I don't want my dollar anymore. Can I get my gill back?" And again, Alice does the calculation. This time she's not even doing a rounding error, um, but she ends up giving me two gill.

And that is the basic problem, right? I I started with one gill. I did two trades with Alice and I ended up with two gills in my pocket. So, in other words, I just I created money out of thin air. So, let's bring this example into the blockchain context.

Um, so, the important thing here in this example was that I needed two trades. And like in in many smart contracts, you will see a pair of trading functions like a deposit and a redeem function or a deposit and withdraw, stake and unstake function, and so on. And So, what what what happened here? What went wrong? Like, now have a look at the red line.

So, I deposited one gill to Alice and then I immediately redeemed it like in the same transaction and I was able to make two gill out of that. So, I I created money out of thin air. So, um, now how can so so the we we we don't want that, right? We need to fix that. So, we need to like make a sanity check that we don't get like more money out than we put in.

Um, and this is the second line here. This is my sanity assumption that when I put one gill into the contract or um, I I should be able to get at most one gill out if if I immediately redeem. Um, and of course, this concept can be generalized. It shouldn't only hold for one gill, but it should essentially hold for for um, arbitrary amounts that I'm putting into the contract. Um, so, this is what a typical the typical implementation of um a deposit and a redeem function look looks like.

And um what you can see here is like let's walk over the deposit function real quick. So, the deposit function accepts an asset amount and then it converts this asset amount into shares just by multiplying the amount of assets with the current exchange rate. Then we are transferring the asset we are pulling in we are pulling the assets in from the from the user. Then we are minting some shares and finally we return the shares that we have minted. And the redeem function is similar.

And with what I just told you, you can see or maybe you cannot see it because well, I didn't use the you cannot see the implementation of the multiplication function. But like this contract is suffering from the exact vulnerability that that I showed you before and that was present in a like more complicated more complex setting in this in this Uniswap contract that I talked about earlier. Um So, this multiplication function and this division function is implemented as like rounding to the nearest neighbor and that is the mistake that we did here. But like how do we actually know in which direction we should round? And there's like a very simple uh very simple rule of thumb rule of thumb that I can give you and that is I call it keep the change.

That means whenever we when whenever we are rounding up oh, sorry. Whenever we have incoming assets like accept assets from the user, then we are going to round up. And whenever like we are sending assets out to the user, we are rounding down. And if you follow this this rule, that means you will approximate your values from the right direction and users won't be able to create money out of thin air and drain your contracts. That is the simple rule.

So, that means like let's revisit the example from before. So, like let's walk over the deposit function. So, instead of like just multiplying, I just now now I use now a variation of the multiplication function that always rounds down and it rounds down because I'm sending the assets out to the user. And for the redeem function here in this example, it's it's the same. Um so, now how can we actually be sure that our implementation is correct?

I mean, this example was really simple and you were maybe able to follow it like on the spot. Um but but like uh um when you're working when you're a developer and working on a like real world contract, your logic will be more complex. So, you want to have tests that ensure that you can um actually um detect counter examples and achieve a higher level of confidence. So, we are now looking at a um at a at a property test. So, um that is basically just like a unit test um but it has parameters parameters to it.

So, it has two parameters, shares per asset, which should just uh it's just the current exchange rate, and it has another very another parameter, assets. And when this test is run, um uh Foundry uh by by the way, that's a Foundry test. I don't know if I have said that. Um I s- um So, when Foundry runs this test, it will like insert call this test with a bunch of random inputs. Um like uh And that's the benefit of a unit test.

When you have a unit test um and you want to detect such a rounding error, you basically need to be lucky and like put the right numbers into the unit test and guess the counter example. Like with this Foundry test, Foundry does the guessing for you and it can it do much quicker than you ever could. Like it can run like 1,000 samples or 2,000 2,000 samples in a couple of milliseconds. Um So, and I want now to have you a look at line 14 and 15 and see that it resembles the property uh that we specified above. So, I hope that you can see in line 14 that we are like executing a deposit function and in the same transaction, we are executing the redeem function and like that is exactly what the property is above.

Uh what the property above says. So, and then then there's some boilerplate code to to that test as well. Uh that's like It's not like mandatory to understand, but like if you look at lines two to line sevens uh to line seven, uh these are just some assumptions that I make over the um inputs. And uh I put these assumptions there just to avoid arithmetic overflow and arithmetic underflow because if I ran into such a situation, my test would simply revert. And I I only want to execute like uh the happy path with this test.

Um and then like line eight to line 12 is just a basic test setup so that I that my contract is in a state that it can actually fulfill the transfer functions uh that I'm calling in line line 14. So, um Fuzzing is good and you should actually you should do it when you test for rounding errors, but like fuzzing is not enough. That's the the uh the sad message here. Like this third example from the um from the first slide that I showed you. Um This example it was the stable stable swap contract um uh suffered from this rounding direction vulnerability.

Although it was heavily fast and like this excerpt that you see here is like from the blog post that ex- explained this vulnerability. And just let it read me let it let me read it out to you. So, another interesting takeaway is that fuzzing can give you a false sense of security. Prior to our report, Saber had already deployed comprehensive fuzzers for their state for their swap implementation. A researcher looking at the code coverage alone might come to the incorrect conclusion that such extensively fast code couldn't possibly have a vulnerability.

All right. So, what else can we do to increase our confidence in in our implementation? And like one possible solution is that we could use like that we could use symbolic execution on top of fuzzing. So, if you see that table on the left-hand side, there are some like some properties that that fuzzing has and on the right-hand side on the right column you see some properties of symbolic execution. But, I don't want to you want you to think about like this slide as fuzzing versus symbolic execution.

It's like you can get the best of both worlds if you combine both of these efforts. And we recently So, we at One Time Verification, we have a symbolic execution engine that's called KEV M. That's it's a symbolic execution engine tailored to the to to the Ethereum Virtual Machine. And we recently added a feature to that that allows you to put Foundry tests into it and instead of fuzzing over the parameters, so instead of choosing random input variables for the parameters, um we do symbolic execution over the over the parameters. And that has like different trade-offs.

So, the nice thing is that, well, for Foundry and for symbolic execution with the EVM, you get to specify your tests and your specifications in Foundry itself. Uh in Solidity itself, sorry. Uh so, that's that's like easier than um than having to to to write your tests in JavaScript or TypeScript. Developers like Foundry especially because of this property. Um So, but that also means, like when it comes to Foundry, that you are somewhat limited to the expressiveness of Solidity.

And there are a bunch of like um safety properties that you simply cannot express in Solidity. And that's like one advantage of the symbolic execution um approach, like that you can actually you can escape from from the from the specification format, and you can actually use uh the K language to specify to to gain additional expressiveness and express more properties. Um So, Foundry fuzzing is extremely fast. It's like you can run 1,000 samples in a couple of milliseconds. And that is like really important for for developers who want to get instant feedback.

Um So, and compared to that, symbolic execution is slow. So, um um And there's a reason for that. So, symbolic execution can give you much more safety guarantees than than fuzzing can. Um but that also means like it's it's um computationally much more expensive than than fuzzing. Um so it's slow, but it's not too slow like uh it works.

For example, you could simply um integrate it into your CI pipeline and let the um let the prover run like on your nightly builds for example. And like this shows like the benefit of like composing both um strategies like fuzzing with Foundry and then symbolic execution with um with KEV M. Um so uh I don't want to go over every line in this table and but I want to talk about the the false positives and the false negatives. So Foundry doesn't have false positives. And what I mean by that is when Foundry um comes up with a counter example um that means that that example really works.

It breaks your code. So it doesn't come up with a with a counter example that does not break your code. So there's no false positive. But Foundry has false negatives. And that is simply if Foundry is not able to choose the right input variables um that means it fails to guess the right counter example.

And at the end Foundry will tell you that test that test actually passed. And that is like the false sense of security that you get from um using Foundry alone. So if you use symbolic execution like we cover 100% of the input domain and we will find that counter example there's no matter what. Um so there are no false negatives when you use uh when you use KEV M. Um then there's a there's another trade-off and that is Foundry is extremely easy to use.

I'd argue it's even easier to use than than Hardhat or Truffle for testing because well, the developers, the smart contract developers are already familiar with with Solidity, like the language that they use to write the contracts. And so that makes Foundry very easy to use. Uh Symbolic execution with KVM is is a little bit different, like it's very easy to try out. It's it's like if you have it installed on your machine and you have Foundry tests specified, you can just try running the KVM on that. And maybe you're lucky and maybe the KVM will tell you why your test passed or your your your your yeah, your test was proven or it was like or we found a counterexample, but in some cases um you will get like a third state that is you didn't pass, you didn't fail, but we are not sure.

Like we don't know. And if you end up in this we don't know state, um that is when a human needs to drive the proof forward. And that is actually something that needs some practice. I think I don't think it's impossible to learn. I learned it, so I'm sure you guys can.

Um but it's it's harder than just just calling Foundry test. So uh One final example of running running Foundry and running the KVM symbolic execution engine on the same test suite. So on the on the top image, I just called Forge test um and I can see the output like um that tells me, "Okay, I was running one test." Um and it passed. I tried 256 uh samples on that test.

That that means Foundry um run this test with 256 different inputs. Um and then I can use like after I've run the the Foundry test, I can run KVM Foundry compile and give it um a Foundry out directory as a parameter. And what this command will do is it will turn uh the Foundry test suite into a proof obligation um for the symbolic execution engine. Like it's a compile step. And then um when I've done that, I can actually try to discharge this proof obligation by running KVM Foundry proof.

Um and the output that you see here is the the lucky case um that uh our like symbolic execution was actually able to discharge the proof obligation. And that's why it says top top at the bottom. Um So but well, when this when a test doesn't pass, you will get a counterexample that is not as easy like to link back to the original code of the test than the um uh than the Foundry counterexample or even worse, it will give you this unknown state and like making sense of this unknown state really requires some practice. You you need to to learn to read these configurations to need to read these stuck states. Um so that's basically it with my talk.

Um I have just um one more uh couple of more notes. So I work at Runtime Verification and we have a research department and we just recently um posted some open research challenges on our website research.runtimeverification.com and if you are a researcher, go to that website, see if something interests you and we have like multiple ways to collaborate with you. Like if every if anything interests you.

All right. And then, like, one other announcement, um uh a colleague of mine, Ricard Jorge, he's in the audience somewhere. I see him. Uh he's giving uh a workshop on formal methods for the working DeFi dev tomorrow at uh at 11:00 a.m.

in workshop room number three. So, uh if you like this talk, uh go ahead and visit Ricard's talk. It it's uh I highly recommend it. All right. And that's it.

I think we have some time for questions. Do we? We have. Do we have a microphone for questions? Hello.

Uh great great presentation. Uh I have a couple of questions. Can you go back to the table that you show both uh like fuzzing and symbolic execution? I have it on the screen, but I don't have it on the projector. Um There it is.

Okay. Great. So, you you put like in the fuzzing column that it requires no inter- in human intervention, but you need someone to write the properties. Is the same for the symbolic execution? Right?

So, if you have good properties, you will catch good bugs. If you don't have good properties, you will have catch no bugs, right? And this is the same with the example that you show like fuzzing is not enough. Uh this code was fast, but perhaps they are not using the correct uh properties. So, what is what is your take on this?

Yeah, that's true. So, uh this is not like fully automatic. Like, for example, when you run a static analysis tool on your code base, then you essentially have to do nothing. You can just like hit a button and run Slither on your code base. So, for fuzzing, you need to write down the tests.

And like like getting the tests getting the the right tests is a challenge on its own. It's not like doesn't come easy. It it has to be practiced. Uh and the same is even more true when you do symbolic execution because while symbolic execution can also can also be a foot gun if you don't know how to use it appropriately. All right.

Yeah, yeah, definitely. And the other thing very quickly, you put like false negatives like on fun on fuzzing which is which I agree and you put no false negative on symbolic execution. However, you said that you could have a third state in which you don't know if it's true or it's false. That sounds like a false negative to me. Like you you don't know the answer.

The tool doesn't know the answer. So, it is it is like Yeah, but but it doesn't say I discharge this proof obligation and everything is right. It says you I'm stuck. And that is um you should interpret this as um I need to put more effort in the proof or in the code to get it to like a final state that says true or false. Yeah, but it's it's the same for for fuzzing.

When you when you say like a pass like a test that passed it's simply because you don't you didn't put enough enough time, right, to to run it. So, it's it's it's a matter of interpretation and it's it's a little misleading. You you you could try like fuzzing over um like the entire input space and then you will also have like no false no false negatives. You could try that. But like you will never terminate.

Like but but that would work, yeah. Come to my talk tomorrow cuz we'll be going over how to write properties. That's basically the next talk. Thank you. Mhm.