Finding the Euler Hack Using Automated Tooling / Martin Derka
Prague DeFi Summit 2023 · June 2023 · 22:49
Martin Derka walks through using automated tooling to find the kind of smart contract vulnerability exploited in the Euler Finance hack, a widely reported DeFi exploit. The talk situates the case study within the broader practice of tool-assisted security auditing in DeFi protocols.
Speakers
Topics
From Prague DeFi Summit 2023, hosted by Prague DeFi Summit 2023.
Transcript
foreign okay okay so we don't have okay so I
also will hold money oh there we go all right so uh thank you very much for introduction uh my name is Martin I'm from Quan stamp uh we are security Auditors and uh I want to be talking about some tooling that we have for discovering economic manipulation attack vectors and you know Finding flash loan attacks so I have a list of protocols in here and you know do you know what they have in common all of these they were all hacked right in the past uh they were hacked actually for a lot of money uh in summary we have roughly 300 million dollars and these hacks have happened within the past you know two two and a half years
most notably the most recent one and quite large one here is Euler that was hacked for 197 Millions uh you know kudos to Euler they eventually managed to get all the money back but uh you know the very initial damage was uh quite large so before I talk about anything I should probably tell you what a flash loan is right so that we all start on the same page so a flash loan is generally an uncoateralized loan that you can take out for a span of a single transaction it is provided to you by a smart contract and the way how it works is that you say hey please dear smart contract give me a lot of money and with that money on my behalf do something
and that smart contracts takes that money it you know triggers the transactions or like continues the transaction that you have triggered does those actions that uh you requested and then at the end of that transaction it double checks that it received the balance back whatever you know it was providing to this transaction and if that loan was indeed repaid it's fine and if it was not then it actively reverts the transaction and that's the reason why flash loans can actually provide arbitrarily amounts of money so really a lot of money uh and they can be certain that this money is going to be repaid okay so you know pending liquidity we actually know that flash loans can be arbitrarily large and
therefore they can be used to do various stuff in the market that you know people did not really intend so I have an example of one flash loan attack in here uh so that we are not talking just in abstract terms so imagine that you have a smart contract and a smart contract is going to hold build a sample of ether and its goal is going to be to sell this ether so you will be able to come to the smart contract and say hey I have some usdc please sell me some of that pool of eth so therefore the smart contract needs to know how to price that eth right what is the exchange rate between eth and usdc and in this design which I'm going to 100 admit right here is vulnerable in this design
uh the pool is going to check the spot price on uni Swap and that's how it is going to uh you know price to the east for you right so if an attacker wanted to exploit such a protocol it would be actually super super simple they would take a flash loan for something like 100 000 eth which is you know 200 million dollars flash loans are really really are large and then they would go to UNI Swap and they would dump all that East on uni swap right that would drive the price of eth really really down so you know for the sake of an example let's assume that that would be something like 10 usdc and then still within the same transaction then they would take that usdc go to the pool and say hey deal pool deer pool I have a lot of usdc
right now please sell me all that eth that you have right and the pool would go it would check the price on uni swab it would see that this is ten dollars and it will start selling this eth for ten dollars but we all know that this you know at least right now and hopefully forever doesn't really match the reality right and then when attackers done they would have you know purchased their 20 million eth from that pool they would go back to UNI Swap and whatever you know East they have Bagley which is uh sorry whatever where usdc they have back they would purchase back that eat that uh day uh dumped initially and eventually they would repay that flash loan of 100 000 each right and because they already made 200 million or
sorry 20 million each uh in the in the Second Step while you know buying it from the pool they would end up with some profit right so this is roughly how flash flown tax work clearly this design is absolutely wrong uh it's vulnerable and we know that uh the pool should be using some kind of Oracle that is not manipulable uh to price that eth so that's kind of what's Happening now why are flash loans so interesting to me flash loans are so interesting to me because they tend to be super super devastating uh in the defy world and there are multiple reasons why they are so devastating so the first one is that flash loans are not provided for free right if I want to borrow 200 million
dollars from somebody even for a little bit in the end I will have to pay fees and even if the fees are really really low like 0.3 percent right um these fees add up because I just borrowed 200 million dollars so these hacks they actually have to generate a lot and a lot of money so they cause a lot of damage so that they can cause a lot of damage they actually come a little bit later in the lifespan of a protocol so you know that is when the protocol picked up some traction when people have deposited a lot of money and because people have deposited a lot of money in a given protocol and their extraction it actually you know draws more attention and more people into the protocol and provides this like
seemingly you know sense of security right because all the other people have money in there but that's absolutely wrong at some point flashing is going to happen because suddenly you know that whole hack became profitable these flash loans they also very often apply to Concepts that people in D5 really really really often try to do and they really often try to do them because they you know keep rediscovering this very very appealing wheel such as single-sided trading pools right if you're providing liquidity into uni swap you're providing both sides of the pair right Heath and usdc for example and you are exposing yourself to impermanent loss many protocols try to invent this single-sided trading pool where you will
only provide one side of these of these two assets and therefore there should be no Implement loss but that is very often manipulable and hackable in some way right uh then very obviously flash loan hacks they actually permeate multiple protocols because you usually have one D5 protocol that is integrated with with something else then you go to something else you manipulate that and that's how you hack your original D5 protocol so they are actually really hard to find because you know this like structure of integration can be actually really deep they're also very ephemeral that means that they can be applicable in one state or in one block and eventually they can disappear if you go back to the example that I have given at the beginning where
I'm speaking about that pool of eth right imagine that the pool of eth actually didn't have too much heat in it that there would be like 10 eath well it would be absolutely non-profitable for you to borrow 200 million dollars to get 10 eth the fees would kill you right so these flash loan attacks sometimes you know they're profitable sometimes they are not and and therefore they are ephemeral and typically they can unfortunately drain the entire tvl over the hack protocol and you know overall they are caused by flawed logic so you know this logic in D5 it touches both the financial principles and the mathematical principles and Technical principles in the protocol and therefore they are really really hard to find and you need really experienced Auditors to find that
so the first flashlight tags happened at East Denver in 2020 and ever since because I you know saw and did they are very very dangerous and detrimental I've been looking for some automated tool that would help us discover these opportunities for such hacks in a little bit better way right and just like having humans analyze the code bases so I have some survey of what was done before already in 2020 there were some attempts to use mithril uh for detecting some Mev opportunities and some some um you know flash loan stuff unfortunately uh all these use cases of mithril uh you know they were very Elementary very basic and mithril actually didn't
perform very well on those so you know it didn't fulfill the goal that I was looking for for a tool that could help us you know search for these in the wild last year I was at Stanford in August and there was this talk about kushal Babel about something called A Clockwork Finance framework so this is something that builds on the game framework on the formal verification capabilities and it looks at uh you know at these flash loan attacks as an MAV opportunity there are some Mev on chain you can extract it if you try to maximize it you know hopefully it will work right it's based on formal verification so it actually has very good results the caveat here is that I tried to you know replicate the experiments and set up the repository
based on their very academic publication and I was unable to this is academic work it's nowhere near production ready and it has some strong caveats where you have to re-express the entire protocol in the language of King framework so you know not not really usable in practice either finally last December I ran into something called Vanguard Vanguard it was a you know symbolic or static analyzer by uh very dice it's no longer available on GitHub so you know this is kind of an obsolete reference but it claimed that it was able to detect flash loan attacks and it couldn't that analyzer was just doing something absolutely different it was just detecting that a smart contract is
calling method called balance off so it had nothing to do with flashlight attacks so the bottom line is there is really nothing out there that can help you you know find these hacks right and that applies up until now because now I'm going to talk about a tool that for the first time ever in the university is capable of doing that so you know through my search I actually found a very very interesting idea that researchers at the University of Toronto had so I decided hey this is great we should partner up and we should actually bring your ideas and the tool into a production setting so this is what have been what we have been working at at constant for the past now let's say half a year so we have developed and productionized a tool that is capable of
doing exactly what I'm you know trying to do in here the tool Works roughly as follows it sees the profit that comes out of a potential flash loan attack as a profit function of a sequence of actions that's like you know depositing money into a protocol withdrawing money from the protocol liquidating somebody and praise holder parameters for these actions so how much are we going to deposit how much are you going to withdraw what are the exact parameters that you are going to uh you know call these functions with and then this tool essentially guesses uh sequences of such actions and for such for each such action sequence it tries to create
using some numerical analysis a model of this multivariate polynomial that expresses the profit function and then it evaluates that polynomial looks for spots where we have some local Maxima right and if those are positive it actually checks on chain whether the attacker really really receives the profit I said that he checks on chain because so far I said we only construct a model right it doesn't have anything to do with blockchain this is just you know a mathematical analysis that happens on top of that so then we actually go and we check whether that model that we have constructed is correct and if it is then we say yes this actually was a hack and here is the exact sequence of actions with the parameters that you need to execute to
actually realize your profit if the parameters and the action sequence do not result in a hack or you know do not really provide a profit that was estimated by the model then we can use this and rename to force the model and somehow actually improve it right and we have magnificent results with that all those protocols that I've showed you before we are actually automatically able to find all those hacks so that's 300 million dollars that didn't have to be lost to hackers in the past and this is where we currently stand I have these like little exclamation marks by uh inverse finance and yearn uh it only means that you know the tool requires a little bit of finagling uh executing it a little bit different states of blockchain then when
uh the attack actually happened but the tool is capable of finding these hacks too so this is how it looks when we run it this is an example of our report because we are actually launching a product around that we are providing these analyzes as a service to D5 protocols this is an output that you know would be applicable to Euler the tool right away tells us hey there is a symbolic attack Vector you have to deposit you have to donate you have to Mint you have to donate you have to liquidate yourself and that will give you 17 million dollars in profit and then we can take these symbolic attack vectors and actually maximize them as Auditors and you know we are able to find everything that actually happen in practice and in the wild I have a whole bunch of notes I'm slowly running out of
time I was getting that signal from the back so I'm you know going to speed this up a little bit so this tool is not fully automated it requires some manual uh annotations for your code but the good thing is that you know first the first time ever we are actually in the position where we are able to make that happen within the scope of roughly one or two work days of a regular human so it's nothing that you know would be beyond the capacity any firm in the in the world has um this tool can detect any kind of Market manipulation vulnerabilities it doesn't have to be just uh the just the flash loan attacks
latest iterations of this tool are closed source so we are not releasing it we are trying to publish it academically when we are done with this psychomatic Publications uh we actually may release the tool for public use but you know what I just told you how it works right so you know if you need to go ahead and Implement one and as I already mentioned we have built a product for this tool uh the current product it's capable of analyzing flash flow attacks and all the possible evm chains so you know whatever you want from this list and going beyond beyond but because I've just conveyed a conceptually very new technique it doesn't really you know work with that chain much except for the simulation of the suspected attack this actually can apply to many many other chains we can
support different runtimes we can even you know uh say that this applies to chains that don't even have flash loan attacks right because it detects logical flaws in the designs of the protocol there is one scenario where the tool doesn't work well it's this one so you know I said that we are looking for the values of some multivariate polynomial if this multivariate polynomial has some sudden spikes in the profit function that would be like you know I don't know if the address equals the owner then rockpool or something like that this would be what's causing such a profit Spike right then it would have a hard time finding that because these polynomials with sudden spikes without any indication they are hard to model and approximate so uh yeah that's that one drawback
luckily D5 protocols and the profit functions in them they actually do not exhibit that behavior so our results are actually still pretty good we also have some future work planned for this tool so we want to increase the performance this is a tool that tries to cover some search space searching for these tracks uh hacks you know the more uh the more search space we can cover the better so you know luckily our implementation allows for that and we already have some plans of how we will increase the performance the tool severely relies on the fact that we have an accurate model for these polynomials right so we actually are going to use some AI Tools in there to kind of improve the search for those
polynomials as well and I already also mentioned that it requires some annotations for the code right to actually say hey these are the possible sequences that might be Irrelevant in here so this is also another space where we will try to apply AI to actually reduce the amount of work that is necessary and you know obviously since this can be applied to other chains we will try that why not you know why should this work only for ethereum so the bottom line is for the first time ever we actually do have a tool uh for detecting flash loan attacks and economic manipulation opportunities it uses some novel approach it's very novel it has nothing to do you know with uh static analysis and then similar stuff
so that means that flash loan attacks are you know not really necessary I will put it in little quotes right because again uh it's a Search tool if it doesn't find anything which is my next point it doesn't really mean that there is nothing right but our empirical results show that you know we are pretty good at using this tool and we will only be getting better as we are more and more optimizing those those models of those polynomials so you know let me say yes flash loan attacks right now obsolete unnecessary hopefully uh I already mentioned that so it's uh you know not a fully automatic tool it still it requires some manual intervention from experts but you know we are fine with this and it is a non-exhaustive Search tool so if it doesn't find a hack
it doesn't mean that a hack doesn't exist but the history shows that we are pretty good we may open source it eventually but you know what I'm really here for today is we're looking for D5 protocol and change to Pioneer this with so if you are a D5 protocol that potentially might be a target of flash loan hack so or other economic manipulations I would be very happy to talk you know we will start offering this service to you and other communities uh that's everything that I have to say once again I'm Martin uh here's my email so you know if you don't catch me after the talk somewhere in the event feel free to contact me over there find me on LinkedIn uh whatever you want uh side note Quant stem started in Waterloo Ontario Canada and there's
going to be East Waterloo after a few you know years of a pause each bottle is in two weeks so if you make your way to Canada please hit me up you know happy to hang out I will be definitely there come as well thank you questions [Applause] hi um thank you for the talk uh could you elaborate on other any possibilities for maybe automatic reaction to potential attacks so as long as you uh discover that the attack maybe will be happening in the next moments is there any way to actually prevent this absolutely so yes I did say that you know these flash loan attacks are ephemeral they depend on the state of chain right so it makes sense to turn
this tool into some kind of a monitoring mechanism that says hey if we have right now arrived to the state of the chain where it has found an attack opportunity we can automatically trigger a pause of the protocol provided that the protocol itself embedded this functionality and gave us the rights to to pause this but yes this is in theory possible more questions over there hi so you claim that flesh loan attack is no more possible for now on and so I want to ask where you've been on 13 April when or 30 March when the Euler was attacked or right March 13th your
product was launched and so our product back then was not launched yet yes uh and we have sorry do you want to finish it this is first you can ask and then okay so uh yes we did take a look at Euler we you know obviously our for-profit company we offer audits we for us serve our clients Euler unfortunately was not our client at that time and even if they were the product was not ready at the time we were you know we would probably use it in some experimental fashion but uh no we did take a look at Euler prior to the hack and we are very sad that we didn't take a look at all prior to the hack because you know if we did it would have never happened and it would be really awesome but yeah unfortunately
mismatching timing and the continuation yeah second is uh why is so important to to make it as the close code and not even present the principle of your work or oh that's not the case there there are Publications out there we have preprints on archive they are public uh the repositories unfortunately have to remain you know the most recent iterations are hidden some initial versions of this tool are actually in public if you you know search deep enough you will find it I've just missed in presentations I'm very flock on the principles how how it works sounds good uh you know principles were here send me an email I can send you a link to the
repos okay thanks you're welcome okay we're out of time so uh thank you Martin very awesome thank you very much [Music]