- FlashSyn is the first automated end-to-end program synthesis tool for detecting flash loan exploitable vulnerabilities and synthesizing profitable attack vectors as proofs.
- This is a novel numerical approximation technique to handle sophisticated logics in the implementation of decentralized finance (DeFi) smart contracts. FlashSyn uses two numerical methods – polynomials and interpolations.
- We used a counter-example driven refinement technique to improve the precision of the approximation.
- FlashSyn is evaluated on 12 DeFi protocols from three blockchains that were victims to flash loan attacks and 2 DeFi protocols from Damn Vulnerable DeFi challenges. FlashSyn successfully generates profitable attack vectors for all cases.
Chen, Zhiyang and Beillahi, Sidi Mohamed and Long, Fan. “FlashSyn: Flash Loan Attack Synthesis via Counter Example Driven Approximation.” arXiv preprint arXiv:2206.10708 [2206.10708] FlashSyn: Flash Loan Attack Synthesis via Counter Example Driven Approximation
Flashloan-enabled attacks have caused tremendous financial losses to the DeFi ecosystem exceeding 0.5 billion US dollars in just the last two years. There is a dire need for tools and mechanisms to help smart contract developers write safer protocols. We propose a new approach, FlashSyn. FlashSyn takes a given smart contract’s functions and key states and synthesizes flash loan attacks targeting those contracts.
Program Synthesis: A programming language method to automatically find a program that satisfies user-provided specifications.
Numerical Method: A popular mathematical tool to find approximate solutions for complex problems.
Optimization: A popular mathematical tool to find input values that maximize (or minimize) an objective function subject to some constraints.
Decentralized Finance (DeFi): A peer-to-peer financial system built on top of blockchains. A few DeFi protocols dominate the DeFi market and serve as references and callees for other decentralized applications: stable coins, price oracles, decentralized exchanges (DEXes), aggregators, and lending and borrowing providers.
Flash Loan: In the DeFi ecosystem, lenders can offer flash loans to borrowers without upfront collaterals deposits, i.e., loans that are only valid within a blockchain transaction and must be repaid with some fees by the end of that transaction. Adversaries can use flash loans to gather large amounts of assets to launch costly exploitation targeting DeFi protocols.
DeFi Protocol State: the state of the DeFi protocol stored on the blockchain which includes among others the amounts of tokens the protocol controls.
Action: A function call, through transactions, to a DeFi smart contract.
Attack: A sequence of actions. An attack is feasible if at the end of the attack the initiator of the sequence of actions gains positive profit.
FlashSyn aims to find flash loan attacks that:
- involve calling functions in existing DeFi smart contracts only
- can be executed atomically within a single transaction.
This work is useful to smart contract developers who want test their protocols against flash loans enabled attacks. In particular, we believe this approach is suitable for new DeFi protocols that interact with existing DeFi protocols, e.g., DEXes, and lending/borrowing protocols.
In developing FlashSyn, we had to overcome a number of technical challenges:
- The underlying logic of DeFi smart contracts is often too sophisticated to reason about. Additionally, some DeFi protocols interact with closed-source smart contracts which prevents even simple code inspection.
- Since the number of possible attacks is exponential with respect to the number of actions in a DeFi protocol, a naive search algorithm that enumerates all possible attacks and executes them locally in a forked environment will be notoriously slow. Thus, it will be impossible to check every possible attack with all possible input parameters.
To address the first challenge: FlashSyn approximates the behaviors of actions in a given DeFi protocol and then uses the approximation to find candidate attacks.
To address the second challenge: FlashSyn first employs a set of heuristics to prune possible attacks, for instance FlashSyn prunes out a sequence that consists of repeating the same action.
For a feasible attack, FlashSyn then uses an off-the-shelf optimizer to find the input parameters that maximize the profit of the attack initiator.
Preparation and Methodology
FlashSyn is implemented in a tool with the same name. Given a DeFi protocol in the form of a set of smart contract functions and key states for each function, FlashSyn first executes transactions in a forked blockchain environment to collect data points and approximate the actions in those smart contracts.
Then, based on numerical methods, FlashSyn uses these data points to build approximated functions for the above actions. It utilizes these functions to find an attack that is estimated to have a positive profit using the optimizer to prune the input parameters.
FlashSyn validates whether the estimated profit of the discovered attack is accurate by executing the attack on the original contracts and checking the actual profit it obtains against the estimated one.
If the difference between the actual and estimated profits is over a fixed accuracy then FlashSyn considers this as a witness of the inaccuracy (counter example) of the approximations. FlashSyn uses this information to extract new data points, plug them into the numerical methods, and refine the approximations iteratively. We call this process counter example guided data collection.
FlashSyn uses two different numerical methods to infer approximated actions, namely multivariate polynomial approximation and multivariate interpolation.
FlashSyn is evaluated using 12 real-world flash loan attacks on three different blockchains (Ethereum, Binance Smart Chain, and Fantom) and 2 imaginary flash loan attacks that are part of a DeFi security challenge proposed by the community. The preliminary results of the evaluation show FlashSyn is able to find flash loan attacks for all cases and in some cases FlashSyn was able to find more profitable attacks. In the table below we give a summary of the FlashSyn evaluation:
|Input Tokens||Output Tokens||Polynomial||Interpolation|
|Blockchain||Application||Actual Profit||# Actions||Profit||Time(s)||Profit||Time(s)|
|ETH||ETH, WBTC||ETH, WBTC||bZx1||1194||2||2336||106||2331||60|
|USDT, USDC||USDT, USDC||Harvest_USDC||338448||4||82152||343||25929||1166|
|USDT, USDC||USDT, USDC||Harvest_USDT||307416||4||60203||82||57187||2284|
|WETH, DAI||WETH, DAI, USDC||Warp||1693523||6||2528667||374||-||-|
|ETH||ETH, USDC, USDT, DAI||Cheesebank||3335773||7||1762771||4180||111011||120|
|Damn Vulnerable DeFi||DVT, ETH||DVT, ETH||Puppet||93000||2||102160||121||102982||204|
|DVT, ETH||DVT, ETH||PuppetV2||953100||3||915560||112||243642||144|
FlashSyn synthesizes flash loan attacks indicating vulnerabilities in smart contracts code, thus simulating the work of the experienced users who exploited those vulnerabilities before.
The counter-example guided data collection allows FlashSyn to refine the approximation efficiently since the data points collected through this process contain very interesting features that improve the accuracy of the approximation. This leads to faster convergence between estimated and the actual profits of attacks enumerated by FlashSyn.
The results of the evaluation show that in some cases FlashSyn finds the most profitable attack using multivariate polynomial approximation while in other cases FlashSyn finds the most profitable attack using multivariate interpolation approximation method.
Our belief is that when the values of the input parameters of attacks do not deviate much from the values used to collect data points, the interpolation approximation method performs well. On the other hand, when the values of the input parameters deviate considerably from the values used to collect data points, the polynomial approximation method performs well.
We see two ways to prevent flash loan attacks.
- Developers can insert a mandatory time gap between two contract function calls. For example, assets can only be withdrawn at least 2 blocks after they are deposited.
- DeFi contracts should use cumulative price. Instead of directly calculating token prices based on instant DEX states, developers can calculate time-weighted prices. Many DEX protocols like Uniswap/Chainlink already have such price oracles.
For more information about the mathematics of flashloan attacks, please see https://2003.03810.pdf .
Damn Vulnerable DeFi, a wargame to learn offensive security of DeFi smart contracts, contains data from the last two benchmarks collected, and information related to non-flash loan DeFi attacks (such as NFT attacks).