Fuzzing Liquity — Alex The Entreprenerd | Recon

Thank you. Yeah. So, I'm Alex the entrepreneur. This talk is called fuzzing liquidity. And [snorts] uh as um you already heard I previously worked at Badger.

I'm currently a lead security researcher at Spearbit and I co-ounded Recon which is a boutique audit firm that uh specializes in audits u that are backed by invariant testing. Uh as of today I uh received about $500,000 in public awards and my proudest achievement was preventing a critical exploit uh on live contracts this year for about $20 million. Amongst our returning customers, we have Badger, Centrifuge, corn, liquidity and balancer DAO and many more. And in terms of what we do at our uh company, we do audits and we also do invariant testing as a service which fundamentally means we set up uh this uh specific type of tests that help us explore uh combinations in smart contracts in order to uh find bugs. We also um have uh some custom deals where we um first of all allow you to run the invarant test in the cloud through recon pro but we also have monitoring um as a service.

Uh and it's actually something I'll talk about tomorrow of how we use invariant testing to uh predict exploits instead of detecting them. Um first of all about this story um this is based on public available facts but everything I'm going to say never made it to prod the liquidity team um originally engaged us uh to help them both audit and uh write the v2 governance contract and uh because of their foreigness uh everything that I'm I'm going to show never made it to prod they actually change uh their smart contracts in order to uh remove the issue that I'm going to talk about. And this is really the story of uh this specific line. If you've been fuzzing smart contracts as much as I have, uh you will know that any division uh creates uh truncation, which means that uh the machine actually deletes the uh data uh that is divided. You basically lose uh the remainder.

And uh we're going to see how uh that line ended up causing uh about $100 million in uh inflated votes for their contract uh in their previous iteration. So before I can talk about the bug, I'm going to need to give some uh uh context about how the governance soul contract works. And uh first of all, liquidity actually chose not to uh use VE which is voting escrow or vested escrow uh which is the most common governance contract available uh in DeFi. And the way voting escrow works uh it fundamentally forces uh a user to lock their tokens and based on the amount of time for which they lock their tokens they end up getting voting power. Whereas uh the way the uh liquidity vu uh governance contract works is based on what I like to call voting power.

uh fundamentally whenever you deposit some liquidity token I mean first of all they chose not to deploy a new token they actually kept the original one then they actually wrapped the original staking the V1 staking on top of the V2 and the V2 mechanism looks a little like the uh chart that you can see provided by chain security where fundamentally as time passes you increase in voting power and the slope of these lines is equal to the amount of liquidity you deposited whereas the uh value is determined by the amount of time in which you uh left your liquidity staked and so this is effectively a soft lock where um you can withdraw at any time and you will lose the voting power. You can see that uh it uh falls down to a lower value but you also have this um mechanism that makes it so that you cannot flesh loan voting power. If you were to deposit some tokens uh in the same block, you will actually end up getting the same voting power and then you will actually lose it the second you withdraw. And so we can simplify our voting power formula to uh this which is basically now block timestamp minus the average age where average age is effectively the average age at which a user deposited their liquidity. If I did a single deposit, I will get the average age of my deposit.

Whereas, if I start depositing multiple times, I will get some sort of a weighted average based on the amount of tokens uh that are deposited. And so, the key uh mechanism is kind of this novel mechanism, this interesting formula, which I guess I'll go back for a second, but it's going to come back later. But fundamentally it all boils down to having a previous outer average time stamp, a new inner average time stamp and then uh doing some math to effectively find a mean, a weighted mean among those two. And so this is really cool because it's a new mechanism. It also is a soft lock and uh they also didn't uh deploy a new token.

They actually made their original design work. And so uh we were basically tasked uh to help fix a bunch of bugs and in doing that uh we ended up writing a part of this and uh uh I'm going to kind of go through some of the bugs that we were presented with. This is all from the chain security audit report which was given to us for version v1 and that we contributed in building version v2 whereas the deployed version is actually version v3. So one of the bugs that we were presented with was this um uh initiative votes overflow. Fundamentally a uh initiative state was represented as a uint 88 whereas the function allocate liquidity could be used with a int 176.

Hopefully it's pretty straightforward uh to think that you can truncate a uint 176 into a uint 88 and you can actually cause an overflow. And so uh this was effectively an overflow. There are many ways to catch this type of bugs. But one of my favorite ways is to have a global accounting property uh that effectively checks that the math was sound before an operation and then it checks that the math was sound after an operation. So this is an example of a bug you can also find with formal verification by applying the weakest precondition.

You just ask the tool whether it can generate you a precondition in which you have an overflow and you should be able to find it fairly easily. So this was not particularly difficult to fix but this is something we were presented with. The next bug was effectively a type a strct. Uh but it points to the same issue that the global accounting math was unsound and uh most importantly was untested which is um if you actually read the chain security report and uh the DOB report they actually um uh the quality of the testing of the codebase was praised partly because of our work as well which uh we we helped boost that quality and something else that I thought was extremely interesting uh but it's not as impactful as these overflows was the vote telling being incorrect fundamentally based on uh various states that the governance contract uh could be in, you would actually uh see that the contract will tally the votes differently. So the total votes will actually change uh in a way that was inconsistent.

And so whenever we think about this idea of um a state and effectively um some sort of aggregate value to u discuss this state then you want to think about the high level idea of having a finite state machine and this is something that uh the moment I started seeing these bugs I really thought about how the contract needed to have an explicit state machine and I'll show you what I mean uh very soon. Uh we also have another issue tied to the final state machine where deallocating from a disabled initiative uh would effectively break the uh global state accounting uh property. These are tend to be somewhat semantics because at the end of the day whether you should count or not count a uh initiative uh or or its votes is not particularly relevant. However, what's relevant is that uh these type of inconsistencies can compound and uh they can also be solved fairly elegantly. So in general whenever you have uh these type of uh bugs or these type of reports you you want to address them by changing the design of your smart contract which is what we did.

We also have this quirky bug. If you check the solution is inspired by some of the work I did in various contest for optimism but we basically took their optimism library for safe call with Ming gas and uh we basically made it so that initiative couldn't grief uh uh by burning all the gas which is uh just just a cool bug [snorts] and uh so we were presented with quite a few um you can imagine that there were actually more and we also find more found more as we started working on the codebase and so whenever Whenever you're tasked to do a massive amount of work in very little amount of time, you want to think about invariant-driven development, which is what we actually did and what we are advocating for. We're not the only ones, but we definitely are uh hopefully we are leading by example with this. And so the key idea of invariant-driven development is that we can look at a smart contract for example the governance contract and that [snorts] we can define some sort of bounds for the behavior of that contract. And so what I mean is that we can look at let's say the soundness of the math or let's or let's say that the total votes should always increase.

We can look at something that is that elegant and that simple. We can write a simple property and then we can structure our CI/CD in a way that that property is always checked. Meaning that even though we start with something really wide, right, we cast a wide net for behavior, we're slowly reducing the amount of variability and the amount of complexity that the contract can have by doing that. And the key part is also that having that allows us to iterate faster. And anytime we reintroduce a bug, which obviously can happen, I can type, you know, make a typo, make a mistake, you know, or do a merge incorrectly, uh we will simply rerun the suite and we will effectively uh immediately notice that we introduced the bug again.

And so in practice, what this looks like, it looked like, you know, scaffolding the suite back when we were working on this engagement. We we had the original version of the create key template, something we open sourced on our GitHub. uh we currently have the second version which is a lot easier to use. Uh and the other aspect is having a big corpus that's a based on a uh fallacy on how uh people uh use these tools. When when you run a benchmark on something like a kidna versus foundry uh akidna will always lose the benchmark for uh uh finding bugs.

It's actually is literally slower than foundry. However, in practice, because of the fact that Akidna has corpus reuse, meaning that it learns from its previous runs, in practice, Akidna is always better for developers that actually work on the codebase. And that's why every single professional uses Akidna uh or I guess every single is a bit an exaggeration, but the vast majority of people that do this professionally do it. And so, uh the last part is debugging broken properties. This was created by my co-founder Antonio Vano.

Basically we uh use a template that connects uh Foundry with Akidra and makes it so that anytime a tool such as Akidra Medusa even Halmos and control break a property we can quickly get a Foundry repro meaning that we run the tool because it's better but obviously we use Foundry because we're not uh you know uh we we like foundry it's a really efficient way to iterate on smart contract and so when it came to fixing the first bug the overflow we simply changed the allocate liquidity to have a type that was closer to the intended goal of a u in88 and then you can see that we have a simple check for recording non- negative. So that was a very straightforward fix. Whereas when it comes to the typo in the uh uh causing an incorrect calculation, we basically added a property called property sum of user voting weights bounded. you know very verbose name but we fundamentally just sum up all the votes and then verify that within a certain tolerance the votes match up this tolerance this tolerance is going to come back later and then when it comes to the finite state machine something I'm pretty proud of is I basically made it fully uh view or I tried my best to make it a fully view set of view functions that given some state will basically return the current state uh in the form of a global state and then the snapshot meaning the uh state that was actually snapshotted at a specific time and it would then tell you whether it needs to be updated. So we effectively have we have a cache or a rolling cache that tells you whether you should actually call the uh storage altering function to alter it.

And then I tried my best to make this get initiative state function fully stateless. It's not exactly stateless but it's fairly close. And it makes it so that we can just pass these uh uh internal storage values and that we can effectively get all of the possible states that the contract can be in. And this uh mapping this in our contract to our properties makes it so that we can uh quickly write a few properties to specify uh behavior. And this is a really convenient way to uh ensure that the contract behave in a way that is intended.

And you can see that there's there's actually quite a few. But given any initiative we can then assert that it will behave as we intended uh with the specific status uh being consistent and the status getting the status is as easy as calling at initiative state. So it's a very easy test to write once you restructure your smart contract in that way. And so all we were left with after spending two weeks and a half almost three weeks uh in uh fixing the bugs, rewriting the code, doing all the invarants and all was really this line. And uh this was the impact that we had QA low severity average time stamp can be off by one second.

And uh the chain security the team at chain security actually did a great work in uh attempting their best at uh changing this impact. And I think they they actually wrote a really interesting uh report. It's poorly pasted here, but you can find it on their uh on the audits from uh liquidity. And so our side what we did is we repurposed our suite to uh ask a kid what was the maximum impact that it could generate. And so this is uh kind of the meat and potatoes of of the talk.

And the most interesting part is really that uh all engagements almost uh all uh end up working in the same way and the um my what I'm advocating is that you basically watch these next few slides and then uh immediately use optimization mode for a kid now basically but fundamentally we have this global property called property sum of initiative uh initiative matches the total votes which fundamentally will sum all the votes that are being used and then all the votes that are stored in the state and it will assert that they match which is something that should typically happen for most uh governance uh and other uh types of protocol and uh we basically saw that uh akidna was able to break it but it will break it with a small value so you would only get like a an error of two an error a few thousand ways so it wasn't particularly relevant and so whenever you're met with uh this type of uh broken properties. Most engineers will simply add the tolerance something like 188 saying okay it's off by one liquidity who cares we did free audits let's just you know let's just be done and that's really the uh it's also what we did uh but you know because of uh my expertise in in this I I just couldn't stop at at this point uh and the reason why this happens is really that uh all these rounding errors they tend to be you know swept under the rug um they they typically get accepted as low severities and most projects stop. Uh and what I'm advocating is you instead convert this to an optimization test which is what we did. We literally took our previous function, created a simple internal function so we could grab those values and then we followed this simple temp template of having a optimization function which needs to return a signed integer. And we have one optimization function called insolvent and one called underpaying.

An insolvent optimization function leads you to a critical bug and underpaying one simply means that there's probably a rounding error. So it's typically okay to have an underpaying contract that uh you know shorthands every user but having an insolvent one can be really problematic. And another pattern that we saw will be using uh thresholds such as 118 or dividing by uh basis points for you to gauge the value or gauge the size the relative size of this. And so off of these uh running the optimization suite we effectively as you can see we have a very simple property really elegant really simple to write and uh we had to shrink it that's because Akidra is a really clunky software and we run into this bug called the zero calls bug. Basically anytime one of your optimization properties uh is broken or is optimized with zero calls, akidna actually breaks uh and the the solution is really to just comment out every property.

So you can actually do that and off of that we actually got this fairly readable repro still you know somewhat rough but at the end of the day it really boils down to having a user performing a big deposit waiting some time I think it's about uh one week and then uh deploying a new initiative and then performing a vote on that new initiative and fundamentally in doing that and voting with 100% of a user voting power we then Uh since we're using Foundry, we can quickly debug it by using console.log. Although uh you know, one day hopefully we'll get the runtime verification debugger to work with cheat codes. But uh off of that, you can see that we still are off by 1 second. And uh uh in this case, we were off by 1 second when comparing the global uh liquidity average time stamp versus the average staking time stamp of the initiative.

And what that does is uh it means that um this one second error could be off for every user. And in this specific uh example of depositing a bunch of liquidity and then waiting a week, uh it will actually an error that will start as about 15 liquidity will actually be magnified to about $151 million of liquidity uh in error. And so whenever you're presented with something like this, which from my perspective, we could have spent months fully investigating this into a critical bug by um building various preconditions. But whenever you're presented with this uh you want to basically look at the root cause which in this case was this truncation on the votes over new liquidity balance and then you want to make the difficult decision of uh rewriting the uh math and that's what the team at liquidity did. they basically were faced with shipping an unknown bug that could probably be magnified or simply changing the formula and uh writing it from first principle.

And that's what they did. they changed it to this uh unallocated liquidity and unallocated offset. Basically a slope plus offset formula which still carries some rounding error but it uh uh is massively smaller than the one that they um that we had on the V2. And so yeah, as a conclusion, my biggest advice is to try fuzzing and most importantly use optimization mode uh for Akidna uh whenever you end up uh having a rounding error as a means to escalate it. Uh thank you for having me.

[applause]

Okay, thank you Alex. So [snorts] now we have a few minutes for questions if any. Please raise your hand if you Okay, we have one question there and then after behind.

So I'm curious in this engagement did you have to invent invariance or did the developers give you some of the invariance?

The invariance.

The invariance. Yeah.

Okay. So no I wrote all the properties myself. The specification from the team was uh there was some documentation and also we collaborated with chain security uh to uh ask them because obviously once you set this up you can uh the impact of an auditor is massively helpful. But um I wrote the vast majority of the properties uh myself and I think uh uh one I guess one side effect of this talk is really this idea of the uh solvency formula. Most contracts have some sort of a solveny formula where you have uh a user uh like a running sum of for of user states and then a global uh total accounting and you will always want to compare them.

So it's it's actually a fairly common uh pattern uh for for properties.

Okay.

Great talk. Hey, it's it's really difficult for a lot of us to start fuzzing. Is there anywhere you know of where we can kind of go to just making fuzzing easier just to to maybe even fuzz from our GitHub? I'm glad you asked. Definitely come to get recon.

xyzipide for [laughter] the best fuzzing engagements to get five grand off your first engagement. But yeah, jokes aside, we have book.get recon.xyz. Uh, originally we used to do office hours where every week I would improvise a talk on the topic.

There's a bunch of them on my YouTube channel uh on YouTube uh Alex the Entrepreneur. Uh but we basically took the best of them and we put them in a book called book.getricon.xyz and that's where we plan on putting all of our open source and uh playbooks. So if if you had to check one resource that's probably the best one to get started and uh most likely will lead you to using our extension called the recon extension which uh we basically made it uh once you have a foundry project you just click a button and it scaffolds the suite for you.

It's not going to uh do the entire work for you, but it definitely will get you very far if you want to get started on something simple. Uh we have time for one more question. Uh did I think I saw a hand on the right? Oh yeah, I think so. Here was first.

Thank you for the talk. I know often people get too focused on tools, but I will ask about tools. Um, do you still see Akidna as the go-to? Is Medusa coming up? Is there any other tools I don't know about?

Yeah, I would uh say as of today, we still use Akidra on the daily. However, for specific use cases, for example, for forked mainet testing, Medusa is actually better, but only if you have a local node. So, Medusa is starting to become uh better. I think trail of bits will consider it comparable. I still think akid is slightly better today.

Uh and as far as I know foundry um alpha rash who used to be an engineer at bits now works at symmetric research is working on making foundry stateful. So the days foundry stateful you probably should try it uh day one until then I think our setup is the best because we break it with a tool that is specialized and then we send you back to foundry for the debugging which I think is the best experience today. Um let's let's try to is your question minute enough maybe?

Yeah, let's try let's try. Yeah, thanks for the talk. Um you mentioned in passing something that's also a social problem which is especially in contests these small errors often get swept under the rug. Do you see any chance for using automation to make you know get more signal on these things that teams often don't engage with in an audit?

Yeah, I think uh if you've uh tried scribble from consensus, I think scribble tried to solve the issue of writing properties uh but fundamentally added a new language. I have given up on uh using a new language but I think uh uh with some work we should be able to make it so that our extension you basically double click on a pro on a function and then you click on another one and then it automatically scaffolds an optimization test. I hope that's how we make it easy. uh but uh there's no escaping the fact that you need to be able to run the tool, understand how it works, understand the weirdness and uh so it's fundamentally it's very easy and very good if you're willing to learn, but if you're not willing to waste about four hours for this stuff, I think it's there's a massive gap there making it easy for everybody to use.

Okay. Um that's it for the Q&A. Let's give Alex a big applause.

[applause]

Okay, I'm going to tell everyone all my cool friends use

the recon extension.

No, like