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.

翻译：在去中心化金融（DeFi）中，贷方可向借款方提供闪贷，即仅在区块链交易内有效且需在交易结束时支付费用的贷款。与传统贷款不同，闪贷允许借款方无需预先抵押即可借入大量资产。恶意攻击者利用闪贷获取大量资产，以攻击存在漏洞的DeFi协议。本文提出一种新框架，用于自动合成利用闪贷攻击DeFi协议的对抗性交易。为降低DeFi协议的复杂性，我们提出一种新技术，通过数值方法（多项式线性回归与最近邻插值）近似DeFi协议的功能行为。随后，利用DeFi协议的近似函数构建优化查询，寻找由一系列函数调用序列构成的攻击向量，并通过最优参数实现最大收益。为提高近似精度，我们提出一种新颖的反例驱动近似精化技术。将上述框架实现为工具FlashSyn。我们在16个曾遭闪贷攻击的DeFi协议及2个来自Damn Vulnerable DeFi挑战的协议上进行评估。FlashSyn在18个基准测试中自动为16个案例合成了攻击向量。其中，有3个案例生成的攻击向量收益超过历史黑客所用方法，且在10个案例中发现多个不同攻击向量，充分验证了其在发现潜在闪贷攻击方面的有效性。