DeFi Security 101 2025 - Find Bugs with Stateful Fuzzing, Alex the Entreprenerd, Recon

Transcript

for security research and I'm going to literally go from using fuzzing and failing to finding bugs to then identifying a bug and then optimizing the bug into uh what I will call a non-exloit to one way to a 50,000x exploit. Uh the system under um test is going to be an oracle. And very briefly about me, I co-founded Recon, which is a audit shop that specializes in using stateful fuzzing uh for finding bugs. I've been I'm a lead security researcher at Spearbit and Code Arena. And before that, I used to uh build smart contracts for Badger where my contracts handle hundreds of millions of dollars of TVL.

I have about $500,000 in awards using these techniques uh to find bugs. And this year I'm proud to say that I prevented a critical exploit from a mutable protocol on mainnet and I saved about $20 million using exactly this type of technique. So I am a big advocate of this and at the same time I know it actually works and I hope you learned something from this session today. So very briefly I'm going to do just a few intro and then we're going to get coding. The um um advantages of foundry are that it's extremely easy to set up and extremely easy to use and uh fuzzing uh with foundry fuzz tests uh is effectively a form of a superpower test

and we'll see that very quickly. Um however there are some disadvantages and the main disadvantage is that it can lead you into a false sense of security because you're only going to test a sequence of operation for which you actually hardcode the test. That means that we're going to write some specific operation, let's say a donation, and then we're going to have some parameter that is randomized, but that doesn't actually test for trying to donate before a swap or donating after a swap. And that's what stateful fuzzing does in contrast to uh other techniques. We are simply trying a bunch of random combinations. And what we're going to do uh in this workshop is we're going to be smart about the combinations that we try. So we try to actually find an

exploit. So uh this this is really the issue that we're addressing. We start from a setup phase. We deploy the system under test and from there we give the fuzzer the ability to try various combinations that can alter the state and then we perform a set of tests. In our case our test is going to be whether we can manipulate the price of an oracle. So the test is going to be fairly simple and uh unfortunately the majority of the workshop is set up which hopefully we'll address in the future through uh just better uh technology. So a very brief idea on how fuzzing works.

We have blackbox, gray box and whitebox fuzzing. The idea is that uh you have some information about the source with whitebox fuzzing. Uh most fuzzers are actually just gray box which means that they build a representation of the system as they fuzz it and then they use the representation to be more effective. Uh um um in the case of Akidna what we're going to uh and also found more recently what we're going to be doing is we're going to build a corpus which means that it's a sequence of random operations that we're going to save to disk so that we can replay them very quickly. And so fuzzing uh professionally consists of almost these two phases of mining the corpus where we just build this set of interesting transactions and then uh performing the

test which is something that is more common and something that all of you are familiar if you use foundry. Uh in terms of when to fuzz versus FV uh I'm going to be followed up soon. So most likely we'll have diverging opinions but fundamentally my biggest advice is to use formal verification for symbolic execution and to break invariance meaning that you start from an abstract state you uh do some operation and then you uh can perhaps find a invariant violation. This type of technique would in my opinion would have flagged something like the balancer rack.

Whereas with fuzzing we are uh performing concrete operations which means that we always get a coded repro that can lead us to the exploit. So this tend to be more laborious in a sense because it's not from a random state but it also is 100% a realistic state which means that it's more actionable. So uh both techniques are very good. The way we use them at recon again is formal verification for quick shortcut to validate our properties and then fuzzing to actually get to the real repro that will lead us to an exploit. Um obviously if we could magically have formal verification of everything and we would have path coverage we would use that but in practice we run into timeouts with formal verification and the uh timeout

with fuzzing is that the fuzzer simply doesn't break a property or it doesn't explore the coverage. So uh I'll get to that as we start building. So, at this point, we're going to start with our basic tests. I'm not going to use the slides that much. And if I ever get confused, I'm going to go to the Visual Studio Code to show me what's happening, but most likely we'll be able to oneshot this. I'm going to use cursor. And this is our system under test. We fundamentally have an oracle, which is a oracle from uh Curvance, which adopted it from V-Max, which was a lending protocol. Both are lending protocols.

And it's fundamentally a naive implementation of the fair reserve uh LP uh pricing formula. I'm not sure if you're super familiar with it, but the way you will price NLP formula offchain is you will simply take the value that is within the pool and then you will divide it by the total supply. This is considered naive and I'll show you why in a moment. There is some extra math here with uh square root to try and make this work. But it's fundamentally this is a flawed implementation that is prone to um exploitation by performing imbalance swaps meaning that I'm effectively losing money in the swap.

But because of this I'm tricking the oracle into repricing the LP. So it's actually a pretty interesting thing. And then the pool implementation is a very common uh uh valadrome uh pool. This is straight up from Valadrome which is a fork of um u it called um can't remember right now but it was bu built by Andre Coronia. So to start I'm going to use the recon extension to help me scaffold and uh this is the only I guess piece of um where you have to trust me a bit. I'm gonna glance over what I'm going to do now and then I'll go back to it to show you why I did it. uh but it's all it's mostly just uh due to time so that I can set up two test two testing uh

environments at the same time uh without having to write two separate suites and two separate set of contracts. So I'm just going to click on build project here which means that we compiled and off of the compilation I'm going to select exclusively the pool and then I'm going to select the oracle and I'm going to click scaffold and what's going to happen is we're just created some boiler plate here for fuzzing. Uh uh unfortunately the uh learning curve is a bit steep but I'm going to try and keep it as simple as possible. So fundamentally we have this setup file which we'll use for uh deployment. So if you ever written a test in Foundry, you know the setup function. This is exactly what it is. We

just put in a separate file for good software engineering. And then I'm going to go over the rest later. Uh so for now just trust me the setup we're going to is going to be used for something else later. And now we have the crypto founder as well for the uh actual testing. So at this point I'm going to open up my terminal and I'm just going to forge build to see whether the code works. Maybe I have uh something that I'm missing here. So let me see. Let's try again.

This is the the one thing that you never want to see happen live. So, I'm just going to switch to my cheat sheet and we're just going to do it off of that. So, the cheat sheet is available at the link I uh showed before and it basically has all of the work already done. So, what I'm going to do is I'm just going to rerun the extension to effectively override that work and uh basically will start effectively from scratch. So, we have this uh as I said this setup um file and uh we have a setup function. So our next goal is simply to get two compilation. So I'm going to forge build and then uh we likely will need to wipe

this out because this is kind of my uh cheat sheet from before. And so at this point we have an oracle and a pool. The first thing I have to do is initialize the pool. I'm going to get the initialize function. As you can see we need two tokens and whether it's a stable pair. We're going to use a non-stable pair and again for convenience I have a utility function called new asset. So I'm gonna instantiate the two tokens by doing address token zero and address token one so that I can use them from storage. And then from here I again I'm using a utility that comes from our extension just for the sake of speed but fundamentally I'm just using a mock token and I'm going to set it. So I'm going to use token zero equals to

new asset with 18 decimals and token one is equal to new asset with 18 decimals. So for the purpose of our uh demo you can imagine this being two wrapped if variants something like wdf versus uh re both starting at a 1:1 ratio. So this pool is going to be an unstable pool, but at the same time it's uh uh assets that are fairly uh similar and um so I'm just going to initialize here with the initialize command. I'm going to set token zero and token one and I'm going to set it to not be um stable. So at this point we have the setup done. We just deployed the pool.

So naturally the next level of testing the next level of progressive escalation as we build more complex things to test our code will be a simple unit test with foundry. So I will do function test basic. What do we need to do? We most likely need to mint the token send the token to the pool and then from there we can uh actually mint some assets. So the simplest way to do this will be to uh we already have the mockery here. So I'm just going to mock your C20 token zero dot mint on the address of the pool and I'm going to say uh deposit about uh 118 assets and I'm going to do the same thing for the token one. And from here

I'm going to just call pool mint and I'm going to mint to myself. So this is a very basic test. We're going to run it. Let's see if it works. And it does. So fundamentally we minted 118 assets. So going back to fuzzing what would be the most direct way to fuzz this? It would really be to simply add a tier say in 256 amount and basically we would mint that amount to the pool. And this would allow us to get some sort of a baseline. Uh before I do that I want to get the price. So I'm going to get the price by calling the oracle. I believe it's get price. And we're just going to uh pass the pool here as the asset and we're just going to log it so we know what it

is. So for good good software engineering I always put what I'm logging uh in a separate uh line so that you can see what I'm actually logging but uh it's fundamentally the same and uh sometimes you don't actually see it for whatever reason but fundamentally this is chewy 18 so our expectation is that the oracle will assert that a a stable pool with a nonarbited scenario has a price of chewy 2018. I think that's pretty clear and our expectation is that the price could perhaps increase if we have some fees but it fundamentally shouldn't change uh meaningfully because as we um perform swaps uh we basically

shouldn't be able to uh uh arbitrage or sorry to alter the price of the pool. So let's see if that's the case. We'll just do a test basic fuzz. We'll put a unit in F6 amount public and then from here we'll just effectively redo the same operation but the main change is going to be that we're going to perform an assertion here. We're going to assert that the um so in this case we can use assert eq that the price is equal to 218 which is our magic constant price is not money pulable. So in the case in this case we are simply testing for what we will call a balanced LP right is fully balanced. I'm going to change this to

amt in a moment and we expect this to uh effectively be fine and have no issue except that we get this arithmetic underflow. And so this is one of the first insights in testing in general is that when you actually test the system versus when you are um just writing it, you may not think of these edge cases. But the edge case here is simply that if we provide less than about I think 188 uh assets the uh minimum liquidity that has to be donate donated on the first mint causes an underflow. So obviously we got this opaque error but I' I've done it on purpose. So what we're going to do here is what I would call the naive clamp. We simply take this value and we add 18. And we'll see quickly how

there's going to be a bunch of jankiness here but hopefully this makes you think. So I'm simply going to do if amount less than 18 then I'm going to increase amount by8 and obviously this should cause another overflow because if we provide with a value that is very close to the maximum we're going to overflow. So this shows you how uh clamping by itself can actually cause more issues and uh um we'll address them momentarily. So a common pattern that I use is limiting the input amount. So in this case to U in 88 and then obviously we're going to run into the same overflow here. So we actually have to do the following. We would have to do U in 256 of AMT plus 18

and that will actually allow us to u uh oh sorry this is um no this is actually fine because it's not going to overflow if it's too small. And so uh we may run into some other issue but we don't. And as you can see the price is constant, right? I'm performing this balanced amount uh balanced deposit and the price doesn't change. So now we obviously will escalate this by adding a imbalanced amount. So we would have amount zero and amount one. And let's do like who's who thinks we're going to get an exploit here? But raise your hand if you think this is imbalanced. So it should break, right?

The price should break. No, it sounds reasonable. So now we just have to apply the clamping strategy, naive clamping to both of the parameters. And we're going to actually see whether this breaks or not. And yeah, my expectation is this should break. It's imbalanced. It's incorrect. So why why wouldn't it? Let's see. Let's see what happens. And as you can see, the test actually doesn't break. It actually is fine. for just to make sure I'm gonna call it test uh imbalanced fuzz just to make sure that it's not that it's actually testing what I'm trying to test. And as you can see, we are now into know the valley of a false sense of security. Like to be

being a developer at this point is a very tough position because the test is passing. I'm passing all hypothetical values. It's safe. No, who will ship this? No. Reasonably, obviously, it's not audited, whatever. But this is shippable, right? It's tested. Go to audit. And now I'm going to show you how uh with stateful fuzzing we're not going to have this our coded sequence because obviously I could add some random stuff here right swap whatever I could do a few operations but with stateful fuzzing we're going to delegate those tasks to the fuzzer and our job is simply to set it up so that it actually explore the state and so this is where the magic will happen and obviously I'm going to

also show the downside of this I don't want to paint you know a picture that this is particularly easy I link though is fairly simple to follow and it will hopefully show you how powerful it actually is. So the setup that I showed you actually can be used with a kid as well. I'm going to do a maybe a fiveminute detour on how akidna works and I'll show you how to run it before I start using our framework which abstracts a ton of these away uh and avoids us doing this low-level stuff. But I just want to make sure you can do it at home if you ever need to use Akidna. So here I have a file called the akidna example and so I also always put a comment above on how to run it just because akidna is really clunky. For example, if we disable payable here,

akidna doesn't work. So every constructor needs to be payable for whatever reason. We have a bunch of other gotchas here uh with akidna as a tool, but it personally allowed me to save $20 million this year. So I love this tool. I think it's the most underrated tool and I will continue to preach using it as much as I can. So fundamentally what do we have here? We have a private variable, a function to increase the variable and then we have a assertion here that will assert false when the count is above two. We could also add here a function called add three just for the sake of demo. And we can perhaps put a require that count is above uh than four.

And so we will just add three to the count in this case. But we could also put a require false just to show you an idea on how fuzzing uh works which is that reverts in fuzzing are ignored. We don't consider a revert an error. We consider only assertion failures as an error. And this is a complete mindset shift because if we had to it's like having a drill or having a sprinkler of water. If I have to focus on every drop going where I want it, I'm just going to waste so much time. So what we do is we ignore all the extra collateral damage in a sense and we just focus on the assertion failure. This is something that for example Foundry doesn't do by default. It's one of my main criticism

of it. When once foundry starts uh teaching this stuff, we will likely promote using Foundry for stateful fuzzing as well. But uh that said, let's run Akidna, our beautiful little uh uh tool. And we'll just open up a new terminal tab. you'll see kind of this AFL fuzzing like UI. The biggest issue with a kid is the compilation speed extremely slow unfortunately. But what you see here is a terminal that basically shows you that to break our assertion we have to call add one three times and then we call check two. So what does this mean? This means that the tool uh was instrumented to call this contract. Right? This is what we would call the target contract.

These are the target functions, the functions that explore the state. But we didn't have to create those sequences. We didn't have to tell the fuzzer which sequences to try. It just tries all the sequences and it figures it out for you. And then it also learns from the sequences. It puts them here under the coverage folder where it fundamentally saves all the interesting stuff so that it can be replayed. And this is why for professional uses we we always talk about corpus reuse which is the idea that we mind the corpus as the expert. We give the corpus to the customer and now they can they can quickly retest those properties very rapidly without having to wait a long time because I um may have undersold uh how how much time

this can take but sometimes this this could have to run for weeks uh if it's not uh clamped or if we don't take some specific strategy. So in in our case, I'm I'll make sure to be in time, but fundamentally keep in mind that um the true guiding factor of the fuzzer is the coverage report. So we'll see down here the covered file. I'm going to reveal in Finder so I can open it. And this is basically showing us what Akidna did here with the target. Uh it's pretty pretty annoying file. The new version of Akidra is a bit better. But fundamentally, let's see. We should be able to stop the fuzzer. It should

generate the report here. I'm seeing it's 16 of November. So, it must not be this one. So, maybe in this case it's not generating it because I didn't provide it with a folder. So I'll show you later but fundamentally what uh what it's done is basically generate some artifact that helps us evaluate the fuzzer. So I'll show you I'll show you that uh with the real example and so the uh having used the recon extension you you definitely noticed we have a bunch of files that's because of our opinionation on how we do stateful fuzzing where the setup is common between foundry and other tools.

Our our framework called the Kimera framework can be used with Akidra, Medusa, Almos and control. Uh the uh interface is the same because we always use uh solidity to perform all these uh tests and also to provide the fuzzer with what we call the target functions. Uh you can see they're abstracted away here into the targets folder. But fundamentally what the the tool did what the extension did is for any external function present in the AI it automatically gives us what we call a uh target function or a handler which is a way for us to call the contract and perform that operation. Uh based on our framework we would also have custom target functions. We leave them up here and we typically use them for clamping

which will be that we try to guide the fuzzer to be a bit smarter in how it generates its inputs. If the fuzzer was perfect, we wouldn't have to do it, but today we have to. Um, and I'm going to actually talk about this during the event um uh in a separate talk at another event. So, but fundamentally, we have a way to export state with the fuzzer uh with uh with pools and then through the manager targets, we actually have a way to mint assets and approve them to the pool as well. meaning that when I uh wrote add asset here I fundamentally created a token that the system can already recognize it can mint it etc on our behalf. So this is a bit of magic that saves us time but it fundamentally allows us to explore the

state much faster. So from here the only thing that we're missing uh I think I I have it already written but I'll just delete everything. We'll start from first principle. What we would have to uh do is we would have to translate the foundry test we wrote like the assert eq8 to something that akidra can actually understand and the way that works is uh we will typically use what we call an assertion so we will likely write something like property price cannot be altered and this will be an external function we write them as public because I'll show you later that our framework allows us to break the property with a kidra and immediately debug it with foundry. So that's why we need public.

But the key idea is it's an external function that akidner will call. And what we would have to do is assert that the price is um uh the same as Chewy 18. So we could also do it programmatically here which I think is better. So we'll do initial price and we'll uh we'll set it to nothing. We'll then in instantiate the pool with some value. Uh this is um um this is because otherwise we're going to get a zero price. Uh so but but actually I'm not going to do it because um for I want to show you a problem that we're going to run into. So I'm just going to do a very basic assertion here uh with

uh asserting that if the pool total supply is zero then we ignore because the price is going to be zero on a zero total supply. So this is just a gotcha and we have to account for and then what we're going to do here is I'm going to use my utility from from our framework which is basically an assertive q and we're going to assert that the uh oracle get price on the pool is exactly 218 at all times 218 is the only price and so let's see what happens here. I'm just going to forge build first because we have the guarantee that if the code

compiles with foundry it will compile with akidnra. And now from there I'm simply going to run aidra through the command in the critic tester um which which basically is how we expose the test to aid. So if I didn't say it already, we have create to foundry for the foundry part and create tester for every other tool including um uh control whereas almos is already uh foundry compatible. So we're basically running the fuzzer. I have format text which means that it's not going to look show you the terminal and then I have 16 workers because I have 16 threads on my machine. I'm setting a test limit and I also passed the configuration file. We typically never alter this. uh it's basically just setting it up so that

it's fully compatible with Foundry and then it's uh uh making so that it compiles everything so that you don't have weird issues in compilation which unfortunately can be very difficult to debug. So the fuzzer is running and it's basically saying that it's replaying some sequences from the corpus that already had and then it's basically here and it's showing me that I have 18 tests. I'm running a bunch of tests and it's not breaking the property instantly. Right? So for the purpose of demo, I'm going to get it to break the property very quickly. But this is kind of the one of the biggest reasons why fuzzing is very difficult to actually use in production. And it's why if you want to actually try it, I recommend you fuzz something very simple, something uh that that you can easily reach coverage

in because what's happening now is that the fuzzer is struggling to reach coverage. And the way we're going to assess that is by let's say I'm going to just delete the kidnap folder to find the coverage file. But basically, we're going to stop the fuzzer. He's going to save the corpus, meaning he saves everything he tried. And then he saves the coverage report as well. So, I'm going to go here and I'm going to basically grab this. And from here, we have to as the expert, we have to actually diagnose why the fuzzer is struggling to kind of reach coverage. So, we're going to go on pool.

And this is the pool uh all the variables being explored. And so you can see making a very long story short that any red lines means it wasn't hit. Any green line means that it was hit. So obviously we had the initialization in the setup. So it was called it works. Then we have the claim fees. You can see here that no fees were ever paid. So most likely we're not doing swaps, but we're going to continue investigating. We see update zero, update one not being called. We see update four not being called. But obviously the key entry points for us are likely swap and mint.

So we can see here that mint uh is struggling to go past this line. So uh for the purpose of demo I'm going to provide the solution. But uh this is really the uh the reason why this is a can be a grind is that now we would have to make a very important decision as to whether we want to uh quickly uh write some sort of a trick like a clamped function that will cover these lines or whether we want to actually let the fuzzer naturally find its way which is obviously better because the fuzzer will try more combinations than the ones that we can think of. Uh but in this case uh because I already tried this code, we likely simply want to give it an easier state uh on which we want to start with

because the the problem that fuzzer is running into now. Yeah. Uh which obviously is is somewhat advanced is that we have zero tokens minted. We have zero approvals to the pool. we have uh we have to mint a minimum amount and as such those three things that have to be done all these preconditions can be easily done in setup and will lead us to a much better result. So that's exactly what we can do. We can go and mint oursel some tokens. So I'm just going to import the mock token which I think I had here simply the mock token interface. I'm going to then mock your C20 of token0.mint

to address this for you in 888. This comes from experience, but um we typically never mint the maximum amounts. That's because obviously we're going to introduce new overflows that we don't want to deal with and most tokens uh tend to have a total supply that is less than you in 88 anyway. So this is a bit of an opinionation but fundamentally I'm giving myself enough tokens so that I don't get like a 100% overflow on everything that I do and then at the same time I don't uh I can explore a bunch of stuff which will be low amounts and high amounts. Uh similarly I'm going to approve the token to the pool.

So in this case it will be address uh of the pool for this is always a bit of a tricky question whether I should approve for the maximum on all or only what I'm willing to lose. Um maybe we should give the good example and just give everything we have versus the maximum. But fundamentally this means that the fuzzer will start from a state in which the the tokens are already minted and the pool is already approved. And my belief at least from from my uh from the way I remember it uh we likely will still run into issues for the purpose of demo. Whereas if we run this in the cloud maybe for a couple hours or a day or whatever the fuzzer will be able to actually break the property. So for the purposes of demo I'm going to clamp even

further. But fundamentally this is kind of a trade-off between uh the actual uh complexity of the state space that you want to fully explore versus your like just the need to actually get to a quick repro. Uh and the fuzzing is good at both but there's definitely nuance in in in deciding how much you want to clamp and how effectively. Uh and uh yeah um generally speaking uh we we we kind of consider like a 4-hour run something that most customers will consider acceptable but anything past four hours we will consider somewhat unacceptable except maybe for the weekend where we could run for two or three days. So generally speaking what we do in our

engagements is we spend a lot of time building the corpus so that the customers can run it within four hours because it's fundamentally uh as you can see there's so many pieces of knowledge and so much stuff that if we even ask the customer to rerun it for like a week they wouldn't do it. It just doesn't make any sense. So as you can see it failed to break the property. But what we can do as a good practice will be to again investigate the coverage and see whether there's some meaningful difference between this version and the new version. We can see that uh uh we're still struggling to create an initial mint. So we we could do a bunch of things uh for this. Most likely what I will do professionally will be to simply

provide with a shortcut function that means correctly. But for the sake of demo, we'll simply start from a state in which we actually have some assets so that the likelihood that we perform a swap on the pool is extremely high and also we likely will also perform donations. So let's simply uh mint some tokens. We're going to do exactly what we did here on the original test in foundry. We're going to mint ourselves 118 uh or rather we're going to mint to the pool and then we're going to mint to oursel some initial supply. And so that simply means that the we're basically helping the fuzzer even more by by having a starting state that is much more um welldeveloped, much easier to uh for the fuzzer to explore. So let's see

what we get. But fundamentally, we're still simply asking the fuzzer whether uh the price is always 218 whenever the total supply is non zero. And I'm pretty sure it already uh broke the property instantly. That's this is something that tends to happen very frequently. Uh and the logical equivalent in formal verification will be to uh simplify the system much uh uh uh very much to the point where uh the uh Z3 or whatever other solver quickly uh gives you a repro. So as you can see we start from an interesting state. We instantly break the property. So, who's willing to bet that this is going to be a massive exploit?

Okay, nobody. Nobody. Okay. A couple of people thinks it could be. It could be big, but no, likely it's not. So, the fuzzer is uh uh done. We're going to stop it. And fundamentally, the way the fuzzer works is it will give you this repro and it will shrink it. shrinking means that the fuzzer was running hundreds of com combinations at a time and then it tries to simplify the sequence of operations to the minimum necessary to actually still break the property. And you can see that we shrunk for maybe uh 12,000 times. We could have shrunk for more, but we fundamentally mint to this random address, most likely the pool. We then call sync and then we see what what happens to the price. And so really what what we're seeing here as

an intuition is that donating to the pool and syncing it alters the oracle pricing uh in a way that we wouldn't have found by swapping we wouldn't have found by you know using the pool at the higher level but instead by interacting with it at a lower level something broke and we don't know by how much but we definitely broke. So, uh, our extension does this, uh, in a much cleaner way, but I'm just going to go to the website because this is how I do it personally. I, we have a a bunch of scrapers that scrape these fuzzers and automatically convert them to a foundry repro. So, fundamentally, akidna, a solidity tool, found a bug, and gives us a repro. And then we use foundry for everything else

that is not stateful fuzzing. So we go back to Foundry immediately going back to the creek to Foundry because now we have a unit test that actually breaks the the the pro uh the code. So just for the sake of not dealing with uh some old code, I'm just going to delete all the basic tests. And fundamentally, we don't exactly know what this is, but I'm pretty sure it's the pool. And uh we're going to run this uh test right here. So as you can see, we have a two-way discrepancy on a price. And what like systematically anytime you have this small of a rounding error, the customer will say the rounding error is uh low, the rounding error doesn't impact the code. The code has been audited by three

other companies. We're going to ship with it. This is 100% what's going to happen. So as the auditor, it's on you to prove that this is a serious issue and it has to be treated with the appropriate considerations and appropriate respect. And so thankfully uh Akidna offers a different mode called the optimization mode which means that we can simply rewrite our tests to ask it by how much can you inflate the price uh obviously in a concrete way meaning that it's not going to find us the absolute theoretical maximum but it's going to find us some value that it was able to do within this time and the way this works I'm going to check the Akina config because Akina is clunky it's a great product but it's also really clunky but fundamentally we're going

have to change the mode here to optimization and we're going to have to prefix every test to optimize and we'll also need to return a int 256 for whatever reason. So we're going to call it function optimize underscore max uh price and this is going to be a public function that returns a int 256. And from here we're going to have a similar scenario where when the total supply is zero we don't care. And then anytime the price is above 218 we want to return a positive value. So fundamental we'll just return uh int 256 of 218 or actually we'll just return the get price minus 218. So this means that there can

be negative numbers. uh if we run into some weird bugs, we'll we'll change the code again, but I think it's going to be fine because the absolute uh highest value is going to be a positive value. Uh in this case, we would expect two ways, right? That's the expectation from the test is two way. Who thinks we're going to find more? Just a few people. Okay. Okay. So now we're going to run Akidna again. So let me see. I'm going to grab this command. It's the same command because we changed the mode through the configuration file. But now it's going to uh it's going to display the uh result in a slightly different way. We run into compilation issues. So I'm not going to use a Kiddra. I'm going to go back to Foundry to see the error and fix

it because if it doesn't compile in Foundry, it doesn't compile with Akidra. That's kind of the idea of our framework. And it seems like these should return a zero. So let's return a zero. Forge build works. Now we're going to run Ekkidra. And uh what you're going to see is there's going to be a bunch of square brackets showing us the um value the highest value of the property uh that we have. And it's going to start mining by basically uh trying a bunch of random combinations. And so you can see that now we're at 66 ways. It's still chugging. And uh this is where we would

just uh you know uh go for a coffee break or something like that and we will wait. It will actually be probably cool if I just leave leave it run until the next talk. But fundamentally what a kidney is doing is it's exploring the state and the various combinations and now it's reward function is optimizing the value. So or at least uh I think so but fundamentally is it's trying to find the maximum value and it's going to constantly save the new uh sequence that generated a higher value to its corpus so that it can continuously self-improve that value. Uh the underlying logic of of how it works is actually not that sophisticated. I believe it could be made much better and much faster and

much more performant uh in various ways but at the same time we're already at something that looks somewhat meaningful. So I'm going to divide it here by 118 just to see what we got. We got a 600 63,000x improvement uh right over the original Chewy 18 price. So that's an example of what happens thanks to progressive escalation. thanks to uh thinking from first principles and fundamentally thanks to applying these techniques in a very diligent way in a very consistent way and so if I can um uh I'm going to show some slides to wrap up but something that I can say uh with extreme confidence is that uh if we look at

something like what happened to balancer or if we look even at something that could have happened here uh this is kind of the way you want to look at uh your systems. We want to find the fastest way to identify if the invariant can be broken. And my recommendation is symbolic execution. Just see if it can be broken. And then once you believe in it, because you have to be confident that you're going to find something, otherwise you're going to quit. But once you believe in it, that's when you start to concretize it. And an example will be to start with a simplified version of the system that you will then fuzz and then perhaps you slowly over time make it much more complex. So uh hopefully this shows you an end toend foundry naive fuzzing stateful fuzzing

optimization of it and it shows you the power of it because if this was a production uh contract deployed in production this would have been wrecked for 60 million times whatever uh the value was. So let me see if I have uh some other slide uh to show you. But uh I think uh I wonder if you guys have any question and if you want me to show uh something specific while uh we have a bit of time. >> I give you the code.

>> Ah right. Yeah I forgot. Right. Right there. So basically now we got the maximum value. Right. This would lead you to a war room and it will lead you to an investigation. I think we can all agree that you cannot have a deployed system in this state. It would be completely unacceptable. However, to go from this to an actual repro, it takes a bit of nuance. So, I'm going to show exactly that. I'm going to stop the fuzzer. And the first problem, another reason why Akidna is this beautiful disaster is that it's not going to be shrunk. Right? We have a 100 calls in our sequence to break the pool. And so, it's really unintelligible information.

Alpha this revert. we cannot actually perform our process. So, I'm gonna show you how we do it. I'm actually gonna show you a bug first just to uh show you how clanky this can be. But basically, I'm gonna also add the minimum version of this. And the minimum I'm actually just going to always return zero just uh to to show you. But when you have a function for this is a bug I'm fixing on a kid. when you have a function that doesn't require a sequence uh to to return the maximum value then the entire entirety of the kiddra will just give up and it will crash and it's not going to optimize anything. So uh or rather it will optimize but it will not shrank it shrink it. So fundamentally what I'm really saying is there's a

bunch of uh bugs with the tool and even in spite of the tool I still recommend using it because it as I showed you it can have an insane impact uh in spite of its clunkiness. So the way we will trigger shrinking will be to remove any function that uh we don't care about and then we will reduce the test limit to a small number let's say to 10,000 tests. And so this means that we're going to quickly replay the corpus which is stored in our uh computer and that will make it so that we go back to the high value and but because we're running a small uh set of tests we likely will not find a higher value. We're just going to get a reproof for that value and then you can see reproducer blah blah blah is trying all that stuff. It gave us the

big value and now it's is stopping. You see that the fuzzing number is not increasing and that the maximum value is static. This means that the fuzzer is entering shrinking mode which means that it's simplifying the sequence for us. It's basically finding the needle in the haystack and uh uh sometimes you have to let this uh you know chill for a few minutes. Um but sometimes that's not necessary. So we're going to just stop it now and let's see what we got. We got a maximum value by minting basically a ton of tokens, right? and then syncing the pool. And so as you can see, uh it's not a particularly difficult exploit to perform. Obviously requires some assets.

So likely we would have to fine-tune this a bit more by perhaps reducing the maximum amount that we can donate to perhaps a realistic value which will be a value that could be flashed on the chain. But fundamentally we can go back to the same idea that we would grab the logs go on our log parser get the repro and then from here we would go to the create to foundry and we will simply console.log log the optimize uh property which will was called optimize max price.

So let's add a nice log max price and run the test. And there you go. We now have a fully coded foundry repro that shows you the maximum impact from here. Obviously, you would have to investigate the actual root cause etc. But hopefully this um uh will lead most uh developers to drop the code and start from scratch. Do we have a do we have any other question?

>> Go ahead. So you basically will want to store the state that will trigger the invariant to be broken. >> Yeah. >> Yeah. Well, from the rep rip pro you will get it here. So you will just do it manually. But um um if you only care about verifying that you could in theory

break a property, you will use symbolic execution because symbolic execution will give you a model that tells you all of the state that will break the property. It wouldn't tell you whether you can get there realistically in a concrete way. But so that's the downside. But that's what I will do if I just wanted to know if I could break it. Whereas here we will simply add a bunch of internal functions something like log state and we will most likely also uh um manipulate the pool contract to uh log whatever we need. But that's how you will do it. You you would use whatever you need from foundry because now you're back in Foundry. So you can etch, roll, warp, etc. And you would debug from there.

seems like >> yeah um I would I wouldn't I don't think about it in terms of false positives because most of the times so the way our engagements work is we have what we call the setup phase it's basically the deployment then we have the coverage phase which takes the most uh effort because we want to test the meaningful stuff and then we likely just have the uh property part and the iteration on there. So from my experience you can get to a point where you all the

false positives are properties you wrote incorrectly. That's that's the point that you get to. And uh that's really a a skill in of in it of itself how to avoid writing that stuff. uh uh but it's uh but it tends to be a a good place to be because if your only problem is that you write bad properties but you can quickly iterate and uh explore the combinations then you're already in the in a good place whereas if you cannot test the combinations because your your coverage is insufficient this this effort is completely valueless and so our work at recon is really to minimize the amount of time to get you to set up we don't want you to set up anything we want it to work uh because I believe if

we did that everybody would use this technology whereas if you write some wrong property you're going to fix it you're a developer I don't see the problem there >> yeah well um let's chat perhaps later about all the downsides of fuzzing but fundamentally the the um it's the same problem. It's not particularly different in uh let's say I I wouldn't I didn't want to have the hard-coded uh mint here, right? Let's just say I didn't want to have this. So something that we could have done would have been to without loss of generality, right? So

because that's the other problem is are you creating a fake system or not? I'm our job is to create uh not lose that generality. So what we will do is we will go to the pull targets and we will create what we call a clamped handler but in this case I will call it a shortcut handler. So I will call it shortcut mint. And so this will simply put amount zero and amount one. But because I know that I provided my um actor with only u8 then I can also do this right still without loss of generality. This is just a shortcut. And then what I will do to maintain all of this because our framework is actually pretty cool if you dig into it is we

would likely use the pool mint handler because this handler may have a bunch of checks a bunch of stuff. So we want to maintain that. So in our shortcuts we never put anything except the uh clamping but we never alter the state in any meaningful way. So we will simply do address this here. Uh so this will basically be the uh mint and then obviously we will need to get the mock c20 address zero uh no it's uh what was it token zero amount zero so this will be c20 token0 mint address

pool amount zero and then obviously we would have the amount one here and again Same idea if it compiles in foundry will compile with Akidra. Uh we don't have the identifier because we need to import the uh mock uh but that's fundamentally the approach we will take. we would over time add ways and then you run into the real limitations which are that if your uh reward function to determine if a state is valuable is based on simple coverage then the fuzzer has inherent limitation with that decision and but those are something that we will have to talk about for like an hour or something. So but once you get to that point you

already understand the limitations and so you will play around with them. So an example for balancer will be that I would have never in my life fuzzed the entirety of balancer. I would have taken out the loop unrolled it into two instances or three instances and fuzzed it in line and that's that would lead you to finding the bug. But then again as I said I would just use we uh um symbolic execution to give me that precondition and then I will have to spend weeks to actually escalate it into a serious bug. One last question. All right. Thank you for having me.

[applause]