Automated Flash Loan Attack Synthesis
DeFi Security Summit 2023 · 16 Jul 2023 · 8:35
Martin Derka of Quantstamp presents the Flash Loan Analyzer, built with the University of Toronto, which synthesizes flash loan attacks automatically. The tool guesses sequences of protocol actions, models the attacker's profit as a multivariate polynomial, finds parameters that yield a profit and validates the exploit in a simulated blockchain environment. He frames it against roughly 300 million dollars lost to flash loan attacks between 2020 and 2023, including Euler, and earlier tools that fell short, such as Mythril-based attempts, the Clockwork Finance framework and Vanguard.
Speakers
Topics
From DeFi Security Summit 2023, hosted by DeFi Security Summit.
Transcript
all right uh thank you for the introduction so I'm Martin I'm from quantstamp and I want to be talking today about Flash loans and you know how we can synthesize such flash loans and attack vectors automatically so here is a list of protocols and very obviously you can guess that all of them were hacked right all of them were hacked within the period of 2020 up until 2023 using flash loans most notably the largest one Euler was hacked for nearly 200 million dollars this year so all together this sums up to 300 million US dollars in Damages and I'm here today to talk about tool at Quantum that we have that can achieve something like that if we had that tool
three years ago nobody would have been hacked so what is a flash loan just to be complete in our definitions flash loan is simply an uncollateralized loan that you can take as a developer from a smart contract for the scope of a single transaction right so you will say hey please give me a flash loan of size X if this liquidity is available the smart contract will give it to you it will run actions that you want it to run and at the end it will check whether you have repaid this flash loan if you did then the transaction will remain unreverted and otherwise it will revert right so this is what a flash loan is what they were developed for or designed for where or is closing Arbitrage
opportunities and you know sometimes they're used for that but sometimes because you can actually borrow a lot a lot of money they are actually being used to export D5 protocols so you know attackers usually take flash loan they manipulate some Market somewhere and then they exploit another protocol that uses that given Market as a price or Oracle for some purposes and the reason why I'm able to be here today and why I was able to show you that slide before is that you know unfortunately due to composability of D5 flash loan attacks and attack vectors they're actually really hard to find so you know for this reason I've been actually on a lookout for a tool that could Aid the discovery of such attack
vectors for us uh for you know pretty much since the very first flash loan attack so the very fly first flash loan attack happened at East Denver in uh 2020 and right in 2020 uh we actually had some first attempts to use automation to discover such attacks so the very first one that I am aware of that was Bernhard Mueller who used mithrail and myth X to discover flash loan tax and he actually gave talks here in Paris at each CC about that still in like July of 2020 but unfortunately he was only able to handle some very basic cases he was actually portraying it and framing it as discovering Arbitrage opportunities he was using uni swap
contracts and you know the general performance and and the quality of these findings were not sufficient for practical use in the auditing industry then uh last year in August at the Stanford blockchain conference I actually saw a really nice talk about something called Clockwork Finance framework which uses formal verification and the game framework to discover uh flash loan attacks it has a lot of caveats it's a purely academic work and it's also not suitable for you know practical use and finally uh there is also something or there was also something called Vanguard so uh Vanguard was a tool developed by uh very
dies I checked it in December 2022 so last year uh it is no longer available it was taken down from GitHub and it was also tempting to discover flash loan vulnerabilities but you know was not successful in doing so so the bottom line is if you actually want some Automation and if you want help from tooling uh you need some new ideas in here there is nothing out there or there was nothing out there up until this point that would work so I discovered his work by a student at the University of Toronto who we partnered with at one stamp and you know brought into production a tool that uh Works roughly as follows it precedes the entire protocol and the sequence of
actions that you can perform on the protocol as a profit function of the as a profit function of the potential profits to the attacker so you know imagine something like compound right you can deposit funds into it you can withdraw funds from it you can liquidate somebody else and then there are various parameters that go into these uh into these function calls so these parameters those are some variables of a multi multivariate polynomial and if you sequence them if you plop in some particular values you will get a value back and that value back is what you would receive as a attacker if you were you know performing this action now if it is action is positive or if the result of this function is positive then as an attacker you would make money if
it is negative then you would not make money right and if you ran everything inside of a flash loan call then uh then such a sequence of actions would revert because you would not be able to um to repay your loan and so this is what we actually do we generate whole bunch of random sequences of these actions and parameters that can be fed into those and then we evaluate what profit would the attacker get if this was run inside of a smart contract that would take flash loan and run this as an attack and then whenever you know we just get these whole bunch of random points then we model this multivariate polynomial and we take a look at what are the local Maxima that give us a
positive profit right and once we find something that gives us the positive profit we actually take these parameters the specific sequence of action and we execute it in a simulated chain environment so imagine something like a fork of blockchain on Foundry or hard hat or something and then if this confirms that such a sequence of actions actually executes and gives us the profit we have synthesized it automatically a full attack Vector that would exploit the given protocol and if it doesn't if it reverts or if the profit is actually negative then we have obtained another function point right another point of that polynomial that we can plop in back into our models and improve those models and keep searching and searching and
searching and this is showing to have a very very very good results as I showed you on one of those initial slides we are able to find pretty much all the significant flash loan attacks and hacks from the past three years including Euler so you know here is uh an example of an output how it looks in our particular implementation for the Euler protocol uh and that's about it so in summary what I wanted to tell you is that at constant we now have a tool that is actually capable of automatically discovering flash loan tax it uses completely new approach you will not find any symbolic execution or formal verification in there it just uses pure numerical analysis and modeling of
polynomials um unfortunately you know for the whole time I was saying yes it's automated yes it is automated the search runs automatically but tool still requires a little bit of manual guidance and a little bit of you know retrofitting for every single protocol but thanks to all the work that I have done together with Jeff within this past half year uh this pendum of work that is actually required is not so much it is very very comparable it's actually a little bit less of the amount of work that we do when we perform a normal regular audit so it is extremely applicable and it's extremely executive executable and repeatable in practice for discovering such hacks uh So currently we have an
implementation it applies to all evm chains but you know as you can guess this technique is actually super super generic so it could be applicable to other runtimes and we would be able to apply it to other blockchains or even cross chains interactions as well but we have not done that work yet and finally the main reason why I'm here we are looking for D5 protocols and blockchains and funds and whoever else who is interested in this topic and uh you know wants to Pioneer with us so if you do please get in touch with me there is a QR code in here that's the telegram contact for me I will be in Paris for the whole week and yeah thank you for your attention