Research Summary: FlashSyn: Flash Loan Attack Synthesis via Counter Example Driven Approximation

@zhiychen Is the complete code available for download or would it need to be recreated from the paper?

1 Like

Hello @Cryptoresearcher
We do plan to release our code later. When it’s released I will post the link here. stay tuned!

1 Like

@parseb Thanks for your question!
I’m also curious whether FlashSyn works outside a lab environment. But it’s too much work for a research paper. Let’s wait to see if the community have answers in future.

Yeah I totally agree that the time to find an attack is always bigger than block production time.

Note there is usually a relatively long time after a contract is depolyed and before the contract is attacked. One use case of FlashSyn is to examine the contracts during that time.

2 Likes

@Fuwala Thank you for bringing that paper into discussion!

Yes. I also found that one when I was doing literature review. I was even lucky enough to attend Liyi’s presentation synchronously online. It is a really good one! But their research problem and methods are different from ours in many aspects!

Research problem: Their research focus on how to find the most profitable arbitrage path across different AMMs(eg. Uniswap, MakerDAO, Bancor). Note the formulas for these AMM swaps are known. The task is to find a path and amounts which give best profit given known formulas. However, our research targets how to find a profitable attack vector which reveals the design flaws inside the smart contracts without explicitly knowing these formulas. FlashSyn works on not only AMMs but also lending protocols, deflationary tokens, and complicated AMM(Curve Finance). Some of them are hard to find the formula because they compose DeFi smart contracts together.

Approach: Since they explicitly know the (composed) AMM formulas, DeFiposer-SMT can symbolically encode all variables and do Z3 symbolic execution. FlashSyn does not explicitly know the formula so symbolic execution is not feasible in this case. Actually Defiposer-ARB is closer to our approach. It performs a greedy local search to find parameters while FlashSyn performs a global search.

Another small point is that, the number of actions per path is at max 5 in their paper. While FlashSyn works on an attack vector with at max 8 actions.

Their tool should be much faster than ours since their tool specifically targets AMM arbitrage.

In terms of adaptiveness, their tool could be used to find arbitrage opportunities. Because this kind of opportunities will be easily taken by others if you are not fast enough. Our tool could be used to detect Flash loan vulnerabilities by auditors, or to examine smart contracts after their deployment. FlashSyn should finally return no false postives because they are execution results instead of estimations.

3 Likes

@zhiychen Wow, thanks for your extensive reply!

On re-reading, I don’t understand why you are using a black-box optimizer (shgo) even though you know the expressions of the functions you’re trying to optimize (the approximated state transition functions)?
Does it simply work faster than non-black-box global optimizers?

I also wonder if you’ve calculated the execution time for each step, and if so, which are the steps that are responsible for the large time required to drive the analysis?

2 Likes

Hello, I also work in our group on DEFI safety. Your paper has benefited me a lot. If you can open source your code, it will help us a lot.

3 Likes