FlashSyn: Flash Loan Attack Synthesis via Counter Example Driven Approximation
Zhiyang Chen, Sidi Mohamed Beillahi, Fan Long
TL;DR
FlashSyn addresses the challenge of identifying flash loan vulnerabilities in DeFi by automatically synthesizing adversarial transaction sequences. It replaces exact symbolic reasoning with data-driven, numerically approximated models of DeFi contract functions and iteratively refines these approximations through counterexamples. The approach is demonstrated on 16 real-world attack benchmarks and 2 DVF challenges, solving most cases and occasionally yielding higher profits than historical attackers, with scalability aided by pruning and parallel optimization. The work enables proactive security assessment of DeFi protocols and has been adopted by a leading smart contract auditor, highlighting practical impact.
Abstract
In decentralized finance (DeFi), lenders can offer flash loans to borrowers, i.e., loans that are only valid within a blockchain transaction and must be repaid with fees by the end of that transaction. Unlike normal loans, flash loans allow borrowers to borrow large assets without upfront collaterals deposits. Malicious adversaries use flash loans to gather large assets to exploit vulnerable DeFi protocols. In this paper, we introduce a new framework for automated synthesis of adversarial transactions that exploit DeFi protocols using flash loans. To bypass the complexity of a DeFi protocol, we propose a new technique to approximate the DeFi protocol functional behaviors using numerical methods (polynomial linear regression and nearest-neighbor interpolation). We then construct an optimization query using the approximated functions of the DeFi protocol to find an adversarial attack constituted of a sequence of functions invocations with optimal parameters that gives the maximum profit. To improve the accuracy of the approximation, we propose a novel counterexample driven approximation refinement technique. We implement our framework in a tool named FlashSyn. We evaluate FlashSyn on 16 DeFi protocols that were victims to flash loan attacks and 2 DeFi protocols from Damn Vulnerable DeFi challenges. FlashSyn automatically synthesizes an adversarial attack for 16 of the 18 benchmarks. Among the 16 successful cases, FlashSyn identifies attack vectors yielding higher profits than those employed by historical hackers in 3 cases, and also discovers multiple distinct attack vectors in 10 cases, demonstrating its effectiveness in finding possible flash loan attacks.