# FlashSyn: Flash Loan Attack Synthesis via Counter Example Driven
Approximation (Extended Version)

Zhiyang Chen  University of TorontoTorontoOntarioCanada
<EMAIL_ADDRESS>,  Sidi Mohamed Beillahi  University of
TorontoTorontoOntarioCanada<EMAIL_ADDRESS>and  Fan Long  University
of TorontoTorontoOntarioCanada<EMAIL_ADDRESS>
(2024)

###### 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.

program synthesis, program analysis, blockchain, smart contracts,
vulnerability detection, flash loan

††journalyear: 2024††copyright: acmlicensed††conference: 2024 IEEE/ACM 46th
International Conference on Software Engineering; April 14–20, 2024; Lisbon,
Portugal††booktitle: 2024 IEEE/ACM 46th International Conference on Software
Engineering (ICSE ’24), April 14–20, 2024, Lisbon, Portugal††doi:
10.1145/3597503.3639190††isbn: 979-8-4007-0217-4/24/04††conference: 46th
International Conference on Software Engineering; April 2024; Lisbon,
Portugal††ccs: Security and privacy Software security engineering††ccs:
Software and its engineering Software testing and debugging††ccs: Security and
privacy Software security engineering††ccs: Software and its engineering
Software testing and debugging

##  1\. Introduction

Blockchain technology enables the creation of decentralized, resilient, and
programmable ledgers on a global scale. Smart contracts, which can be deployed
onto a blockchain, allow developers to encode intricate transaction rules that
govern the ledger. These features have made blockchains and smart contracts
essential infrastructure for a variety of decentralized financial services
(DeFi). As of April 1st, 2023, the Total Value Locked (TVL) in 1,417 DeFi
smart contracts had reached $50.15$ billion (DefiLlama, 2023).

However, security attacks are critical threats to smart contracts. Attackers
can exploit vulnerabilities in smart contracts by sending malicious
transactions, potentially stealing millions of dollars from users.
Particularly, a new type of security threat has emerged, exploiting design
flaws in DeFi contracts by leveraging large amounts of digital assets. These
attacks, commonly referred to as _flash loan attacks_ (SlowMist, 2023; McKay,
2022; Zhang et al., 2023), typically involve borrowing the required large
amount of assets from flash loan contracts. Among the top $200$ costliest
attacks recorded in Rekt Database, the financial loss caused by $36$ flash
loan attacks exceeds $418$ million USD (McKay, 2022).

A typical flash loan attack transaction consists of a sequence of actions, or
function calls to smart contracts. The first action involves borrowing a
substantial amount of digital assets from a flash loan contract, while the
last action returns these borrowed assets. The sequence of actions in the
middle interacts with multiple DeFi contracts, using the borrowed assets to
exploit their design flaws. When a DeFi contract fails to consider corner
cases created by the large volume of the borrowed assets, the attacker may
extract prohibitive profits. For example, many flash loan attacks use borrowed
assets to temporarily manipulate asset prices in a DeFi contract to trick the
contract to make unfavorable trades with the attacker (Qin et al., 2021; Cao
et al., 2021). Although researchers have developed many automated program
analysis and verification techniques (Mossberg et al., 2019; Feng et al.,
2019; Grieco et al., 2020; Brent et al., 2020) to detect and eliminate bugs in
smart contracts, these techniques cannot handle flash loan attack
vulnerabilities. This is because such vulnerabilities are design flaws rather
than implementation bugs. Moreover, these techniques typically operate with
one contract at a time, but flash loan attacks almost always involve multiple
DeFi contracts interacting with each other.

FlashSyn: We present FlashSyn, the first automated end-to-end program
synthesis tool for detecting flash loan attack vulnerabilities. Given a set of
smart contracts and candidate actions in these contracts, FlashSyn
automatically synthesizes an action sequence along with all action parameters
to interact with the contracts to exploit potential flash loan
vulnerabilities. Additionally, FlashSyn can analyze past blockchain
transaction history, assisting users in identifying candidate actions for
synthesis.

The primary challenge FlashSyn faces is that the underlying logic of DeFi
actions is often too sophisticated for standard solvers to handle. Even if the
action sequence was already known, a naive application of symbolic execution
might not be able to find action parameters because it may need to extract
overly complicated symbolic constraints causing the solvers to time out.
Moreover, FlashSyn synthesizes the action sequence and the action parameters
together and therefore faces an additional search space explosion challenge.

FlashSyn addresses these challenges with its novel _synthesis-via-
approximation_ technique. Instead of attempting to extract accurate symbolic
expressions from smart contract code, FlashSyn collects data points to
approximate the effect of contract functions with numerical methods. FlashSyn
then uses the approximated expressions to drive the synthesis. FlashSyn also
incrementally improves the approximation with its novel _counterexample driven
approximation refinement_ techniques, i.e., if the synthesis fails because of
a large deviation caused by the approximations, FlashSyn collects the
corresponding data points as counterexamples to iteratively refine the
approximations. The combination of these techniques allows the underlying
optimizer of FlashSyn to work with more tractable expressions. It also
decouples the two difficult tasks, finding the action sequence and finding the
action parameters. When working with a set of coarse-grained approximated
expressions, FlashSyn can filter out unproductive action sequences with a
small cost.

Experimental Results: We evaluate FlashSyn on $16$ DeFi benchmark protocols
that were victims to flash loan attacks and $2$ DeFi benchmark protocols from
Damn Vulnerable DeFi challenges (Damn Vulnerable DeFi, 2023a). FlashSyn
synthesizes adversarial attacks for $16$ out of the $18$ benchmarks. For
comparison, a baseline with manually crafted accurate action summaries only
synthesizes attacks for $7$ out of the $18$.

Contributions: This paper makes the following contributions:

  * •

FlashSyn: The first automated end-to-end program synthesis tool for detecting
flash loan attack vulnerabilities. It enables approximate attack synthesis
without diving into sophisticated logics of DeFi contracts.

  * •

Synthesis-via-approximation: A novel synthesis-via-approxi- mation technique
to handle sophisticated logics of DeFi contracts.

  * •

Counterexample Driven Approximation Refinement: A novel counterexample driven
approximation refinement technique to incrementally improve the approximation
during the synthesis process.

  * •

Experimental Evaluation: We implemented FlashSyn in a tool and evaluated it on
$16$ protocols that were victims to flash loan attacks and $2$ fictional flash
loan attacks.

Our solution, FlashSyn has been adopted and further developed by Quantstamp, a
leading smart contract auditing company for the detection of flash loan
vulnerabilities in DeFi contracts (Martin Derka, 2023; Quantstamp, 2023a, b).

##  2\. Background

Blockchain: Blockchain is a distributed ledger that broadcasts and stores
information of transactions across different parties. A blockchain consists of
a growing number of blocks and a consensus algorithm determining block order.
Each block is constituted of transactions. Ethereum (Wood, 2012; Buterin,
2014) is the first blockchain to support, store, and execute Turing complete
programs, known as smart contracts. Many new blockchains use the Ethereum
virtual machine (EVM) for execution due to its popularity among developers.

Smart Contracts: Each smart contract is associated with a unique address, a
persistent account’s storage trie, a balance of native tokens, e.g., Ether in
Ethereum, and bytecode (e.g., EVM bytecode (Wood, 2012; Buterin, 2014)) that
executes incoming transactions to change the storage and balance. Users
interact with a smart contract by issuing transactions from their user
accounts to the contract address. Smart contracts can also interact with other
smart contracts as function calls. Currently, there are several human-readable
high-level programming languages, e.g., Solidity (Foundation, 2023a) and Vyper
(Foundation, 2023b), to write smart contracts that compile to the EVM
bytecode.

Decentralized Finance (DeFi): DeFi is a peer-to-peer financial ecosystem built
on top of blockchains (Wüst and Gervais, 2018). The building blocks of DeFi
are smart contracts that manage digital assets. A few DeFi protocols dominate
the DeFi market and serve as references for other decentralized applications:
stable coins (e.g., USDC and USDT), price oracles, decentralized exchanges,
and lending and borrowing platforms. In DeFi, a special type of loan called
flash loan allows lenders to offer loans to borrowers without upfront
collaterals deposits. The loan is only valid within a single transaction and
must be repaid with fees before the completion of the transaction.

##  3\. Illustrative Example

We next present a motivating example to describe the complexity of flash loan
attacks and our proposed approach to synthesize them.

Background: On October 26th 2020, an attacker exploited the USDC and USDT
vaults of Harvest Finance, causing a financial loss of about $33.8$ million
USD. In this section, we will focus on the attack on the USDC vault. The
attacker repeatedly executed the same attack vector 17 times targeting the
USDC vault. Fig. 1 summarizes the attack vector. The attack vector contains a
sequence of actions that interact with the following contracts:

  * •

Uniswap: Uniswap is a protocol with flash loan services.

  * •

Curve: Curve is an exchange protocol for stable coins like USDT, USDC, and
DAI, whose market prices are close to one USD. It maintains pools of stable
coins and users can interact with these pools to exchange one kind of stable
coins to another. For example, Y Pool in Curve contains both USDC and USDT.
Users can put USDC into the pool to exchange USDT out. The exchange rate
fluctuates around one, which is determined by the current ratio of USDC and
USDT in the pool. Note that internally Y pool automatically deposits USDT and
USDC to _Yearn_ ,111Yearn is a DeFi protocol that generates yield on deposited
assets. yTokens of Yearn represent the liquidity provided in a Yearn product.
keeps yUSDT and yUSDC tokens, and retrieves them back when the users withdraw.
We omit this complication for simplicity.

  * •

Harvest: Harvest is an asset management protocol and the victim contract of
this attack. Users can deposit USDC and USDT into Harvest and receive fUSDC
and fUSDT tokens which users can later use to retrieve their deposit back.
Harvest will invest the deposited USDC and USDT from users to other DeFi
protocols to generate profit. Note that the exchange rate between fUSDC and
USDC is also not fixed. It is determined by a vulnerable closed source oracle
contract, which ultimately uses Curve Y pool ratios to calculate the exchange
rate.

Figure 1. Harvest USDC Vault Price Manipulation Attack.

Attack Actions: The attack vector shown in Fig. 1 first flash loaned $18.3$M
USDT and $50$M USDC, then called $4$ methods (actions) to exploit the design
flaw in Harvest. The first action, action $1$, swaps $17,222,012$ USDT for
$17,216,703$ USDC via _Curve.Fi Y Pool_. Action $1$ reduces the estimated
value of USDT based on the ratio in Y pool as the amounts of USDT in Y Pool
considerably increases. This in turn reduces Harvest Finance’s evaluation of
its invested assets. Action $2$ deposits $49,977,468$ USDC into _Harvest
Finance USDC vault_ and due to the reduced evaluation of the invested
underlying assets, the attacker receives $51,456,280$ fUSDC back, which is
abnormally large. Similar to action $1$, action $3$ then swaps $17,239,234$
USDC back to $17,230,747$ USDT via _Curve.Fi Y Pool_ , which normalized the
manipulated USDT/USDC rate in the pool. It also brings Harvest Finance’s
evaluation of its invested underlying asset back to normal. Finally, action
$4$ withdraws $50,298,684$ USDC (using $51,456,280$ fUSDC) from _Harvest
Finance USDC vault_. Assuming $1$ USDC $=1$ USDT $=1$ USD, the profit of the
above attack vector is $307,420$ USD.

This attack is a typical case of oracle manipulation. The exploiter
manipulated the USDT/USDC rate in _Curve.Fi Y Pool_ by swapping a large amount
between USDC and USDT back and forth, which caused Harvest Finance protocol to
incorrectly evaluate the value of its asset, leaving large arbitrage space for
the exploiter. The actions sequence and particularly the parameters are
carefully chosen by the attacker to yield best profit. There are multiple
challenges FlashSyn faces to synthesize this attack.

Challenge 1 - Sophisticated Interactions: The attack involves several smart
contracts that interact with each other and with other contracts outside the
attack vector. The state changes caused by one action influence the behavior
of other actions. This makes the synthesis problem of finding an attack vector
more complicated as the effect of an action depends on its predecessor actions
thus actions cannot be treated separately.

Challenge 2 - Close Source: Some external smart contracts that a DeFi protocol
interacts with are not _open-source_. For instance, the source code of the
external smart contract _PriceConverter_ 222Ethereum address:
0xfca4416d9def20ac5b6da8b8b322b6559770efbf. of Harvest Finance protocol is not
available on Etherscan (Etherscan, 2023), and it is called by actions $2$ and
$4$ to determine the exchange rate between fUSDC and USDC. This impedes the
complete understanding of the DeFi protocol implementation and to reason about
its correctness to anticipate attacks vectors.

Challenge 3 - Mathematical Complexity: DeFi contracts use mathematical models
that are too complex to reason about. For instance, actions $2$ and $4$ swap
an amount of token $i$ to token $j$, while maintaining the following
_StableSwap invariant_ (Egorov, 2019):

$A\cdot n^{n}\sum_{i}x_{i}+D=A\cdot n^{n}\cdot
D+\frac{D^{n+1}}{n^{n}\prod_{i}{x_{i}}}$ where $A$ is a constant, $n$ is
number of token types in the pool($4$ for _Curve.Fi Y Pool_)333Ethereum
address: 0x45f783cce6b7ff23b2ab2d70e416cdb7d6055f51., $x_{i}$ is token $i$’s
liquidity, $D$ is the total amount of tokens at equal prices. There does not
exist a closed-form solution for $D$ as it requires finding roots of a
_quintic equation_. In the actual implementation, $D$ is calculated
iteratively on the fly via Newton’s method (see Appendix A).

To demonstrate the complexity of DeFi protocols, we run an experiment with
Manticore (Mossberg et al., 2019), a symbolic execution tool for smart
contracts, to execute the function _get_D_ , for computing _D_ as shown in
Fig. 2, with symbolic inputs and explore all possible reachable states.
Manticore fails and throws a solver-related exception together with an _out of
memory_ error. We then simplified _get_D_ by removing the outer _for_ loop and
bounding the length of _xp_ to $2$, Manticore still fails and throws the same
error.

⬇

1function get_D(uint[] xp) returns (uint):

2 uint N_COINS = xp.length;

3 uint S = sum(xp);

4 // ...

5 uint D = S;

6 uint Ann = A * N_COINS; // A is a constant

7 for (uint i = 0; i < 255; i = i + 1) {

8 uint D_P = D;

9 for (uint j = 0; j < xp.length; j = j + 1) {

10 D_P = (D_P * D) / (xp[j] * N_COINS + 1);

11 }

12 uint Dprev = D;

13 D = ((Ann * S + D_P * N_COINS) * D) /

14 ((Ann - 1) * D + (N_COINS + 1) * D_P);

15 if (abs(D - Dprev) <= 1) break;

16 }

17 return D;

Figure 2. _get_D_ Method to Compute _D_.

###  3.1. Apply FlashSyn

We will now show how FlashSyn synthesizes the Harvest USDC vault attack from
the identified set of actions listed in Table 1.444In Section 6, we present
FlashFind to automatically find the set of candidate actions that are used
here by FlashSyn to synthesize an attack vector. The first two input arguments
to _exchange_ specify the token types to be swapped. The third argument
specifies the quantity to swap.555Note that in the implementation the actual
name of the _exchange_ method is _exchange_underlying_ , $1$ and $2$ are used
to identify the tokens USDC and USDT, respectively, and the method has a
fourth argument to specify the minimal quantity expected to receive from the
swapping. Table 1 lists each action’s token flow, along with the number of
data points collected initially (without counterexamples) and the total number
of data points for polynomial and interpolation, respectively. The amounts of
tokens transferred in/out for each action are calculated based on its
contract’s member variables or read-only functions. We refer these variables
and functions as states of an action. A prestate refers to the state before
the execution of an action. Executing an action will also alter states, which
are denoted as poststates. The states not altered by any action are ignored.

For example, exchange(USDT,USDC,v) leverages two states, balances[USDC] and
balances[USDT], to calculate the amounts of token exchanges. Upon execution,
this function also modifies these two states. Consequently, these two states
act as both the prestates and poststates of exchange(USDT,USDC,v).

Initial Approximation: To generate the initial approximation of the state
transition functions of each action, FlashSyn first collects data points where
each data point is an input-output pair. The input is the action’s prestates
and parameters, and the output is its poststates and the outputted values. To
collect data points, FlashSyn executes the associated contracts on a private
blockchain (a forked blockchain environment) with different parameters to
reach input-output pairs with different prestates and poststates. FlashSyn
then uses the collected data points to find the approximated state transition
functions. We consider two techniques to solve the above multivariate
approximation problem: linear regression based polynomial features and
nearest-neighbor interpolation (Montgomery et al., 2021; Rukundo and Cao,
2012). The following example is one of _exchange(USDT,USDC,v)_ ’s state
transition functions approximated by polynomials:
$\mathsf{s}_{1}^{\prime}=0.73244455\times\mathsf{s}_{1}-0.23655202\times\mathsf{s}_{2}-0.85915531\times
v+27351279.416023515$ where $\mathsf{s}_{1}$ and $\mathsf{s}_{1}^{\prime}$ are
the prestate and poststate balances[USDC], $\mathsf{s}_{2}$ is the prestate
balances[USDT], and $v$ is the third argument of the action
_exchange(USDT,USDC,v)_.

Table 1. Actions in Harvest USDC Vault Attack. IDP and TDP denotes the initial
and total number of datapoints. USDT(-) (resp., USDC(+)) denotes USDT (resp.,
USDC) tokens transferred out (reps., in).

Action | Token Flow | IDP | TDP-Poly | TDP-Inter
---|---|---|---|---
exchange | USDT(-), USDC(+) | 2000 | 2238 | 2792
(USDT, USDC, v) |  |  |
exchange | USDC(-), USDT(+) | 2000 | 2148 | 2888
(USDC, USDT, v) |  |  |
deposit(v) | USDC(-), fUSDC(+) | 2000 | 2162 | 2358
withdraw(v) | fUSDC(-), USDC(+) | 2000 | 2364 | 2876

Enumerate and Filter Action Sequences: After capturing an initial
approximation of state transition functions, FlashSyn leverages an
enumeration-based top-down algorithm to synthesize different action sequences.
FlashSyn applies several pruning heuristics to filter unpromising sequences.
For each enumerated action sequence, FlashSyn uses the approximated state
transition functions to construct an optimization problem, consisting of
constraints and an objective function that represents profit. FlashSyn then
applies an off-the-shelf optimizer to obtain a list of parameters that
maximize the profit estimated using approximated transition functions.

Counterexample Driven Refinement: After obtaining a list of parameters that
maximize the estimated profit of an action sequence, FlashSyn proceeds to
verify the synthesized attack vectors by executing them on a private
blockchain and check their actual profits. If the difference between the
actual profit and the estimated profit of an attack vector is greater than
$5\%$, FlashSyn reports it as a counterexample, indicating inaccuracy of our
approximated transition functions. To correct this inaccuracy, FlashSyn
employs counterexample driven approximation refinement technique. FlashSyn
utilizes the reported counterexamples to collect new data points and refine
the approximations. The revised approximations are subsequently used to search
for parameters in next loops. For example, FlashSyn with polynomial
approximations collects $238$ additional data points for the action
_exchange(USDT, USDC, v)_ throughout $7$ refinement loops.

Synthesized Attack: In the Harvest USDC example, FlashSyn successfully found
the following attack vector that yields an adjusted profit of $110051$ USD
using the interpolation technique with the counterexample driven refinement
loop.

_exchange(USDT, USDC, 15192122)_ $\cdot$ _deposit(45105321)_ $\cdot$
_exchange(USDC, USDT, 11995404)_ $\cdot$ _withdraw(46198643)_

##  4\. Preliminary

Labeled Transition Systems (LTS). We use LTS to model behaviors of smart
contracts. A LTS $A=(Q,\Sigma,\mathsf{q}_{0},\delta)$ over the possibly-
infinite alphabet $\Sigma$ is a possibly-infinite set $Q$ of states with an
initial state $\mathsf{q}_{0}\in Q$, and a transition relation
$\delta\subseteq Q\times\Sigma\times Q$.

Execution. An _execution_ of $A$ is a sequence of states and transition labels
(_actions_)
$\rho=\mathsf{q}_{0},\mathsf{a}_{0},\mathsf{q}_{1}\ldots\mathsf{a}_{k-1},\mathsf{q}_{k}$
for $k>0$ such that $\delta(\mathsf{q}_{i},\mathsf{a}_{i},\mathsf{q}_{i+1})$
for each $0\leq i<k$. We write
$\mathsf{q}_{i}\xrightarrow{\mathsf{a}_{i}\ldots\mathsf{a}_{j-1}}_{A}\mathsf{q}_{j}$
to denote the subsequence
$\mathsf{q}_{i},\mathsf{a}_{i},...,\mathsf{q}_{j-1},\mathsf{a}_{j-1},\mathsf{q}_{j}$
of $\rho$.

Invocation Label. Formally, an _invocation label_ $\mathsf{adr}.m(\vec{u})$
consists of a method name $m$ of a contract address $\mathsf{adr}$,
accompanied by a vector $\vec{u}$ containing argument values.

Operation Label. An _operation label_
$\ell:=\mathsf{adr}.m(\vec{u})\Rightarrow(I,v)\ \cup\ \bot$ is an invocation
label $\mathsf{adr}.m(\vec{u})$ along with a return value $v$ , and $I$ is a
sequence of operation labels representing the “internal” calls made during the
invocation of $m$. The distinguished invocation outcome $\bot$ is associated
to invocations that revert.

Interface. The _interface_ $\Sigma_{\mathsf{adr}}$ is the set of non-read-only
operation labels in the contract $\mathsf{adr}$. We assume w.l.o.g. that the
preconditions are satisfied for all the operations in $\Sigma_{\mathsf{adr}}$,
otherwise, the external invocation $\mathsf{adr}.m(\vec{u})$ reverts.
$\Sigma_{\mathsf{adr}}$ is a superset of the set of action candidates of
FlashSyn.

Smart Contract. A _smart contract_ at an address $\mathsf{adr}$ is an LTS
$C_{\mathsf{adr}}=(Q_{\mathsf{adr}},\Sigma_{\mathsf{adr}},\mathsf{q}_{0},\delta_{\mathsf{adr}})$
over the interface $\Sigma_{\mathsf{adr}}$ where $Q_{\mathsf{adr}}$ is the set
states and $\delta_{\mathsf{adr}}$ is the transition relation.

Symbolic Actions Vector. We define the notion of a symbolic actions vector
$\mathbf{S}=\ell_{\mathsf{adr}1}\ldots\ell_{\mathsf{adr}n}$ s.t.
$\ell_{\mathsf{adr}i}\in\Sigma$ for $1\leq i<n$ as the sequence of operation
labels (possibly from different contracts) associated with the execution
$\rho$, i.e.,
$\rho=\mathsf{q}_{1},\ell_{\mathsf{adr}1},\mathsf{q}_{1}\ldots\ell_{\mathsf{adr}n},\mathsf{q}_{n}$.

Balance. We define the balance of address $\mathsf{adr}$ in a blockchain state
$\mathsf{q}$ as the mapping $\mathcal{B}:Q\times\mathbf{A}\implies\mathbf{V}$
that maps the pair $(\mathsf{q},\mathsf{adr})\in Q\times\mathbf{A}$ to the
weighted sum of tokens the address $\mathsf{adr}$ holds at $\mathsf{q}$, i.e.,
$\mathcal{B}(\mathsf{q},\mathsf{adr})=\sum_{\mathsf{t}\in\mathbf{T}}{\mathbf{M}(\mathsf{q},\mathsf{adr},\mathsf{t})\cdot\mathbf{P}(\mathbf{t})}$,
where $\mathbf{T}$ represents tokens hold by $\mathsf{adr}$,
$\mathbf{M}(\mathsf{q},\mathsf{adr},\mathsf{t})$ represents the amount of
token $\mathsf{t}$ hold by $\mathsf{adr}$ at the blockchain state
$\mathsf{q}$, and $\mathbf{P}(\mathsf{q},\mathbf{t})$ represents the price of
token $\mathsf{t}$ at the blockchain state $\mathsf{q}$.

Attack Vector. An _attack vector_ by an adversary $\mathsf{adr}$ consists of a
symbolic actions vector $\mathbf{S}$ where the symbolic arguments are replaced
by concrete values (integer values) and $\mathbf{S}$ transforms a blockchain
state $\mathsf{q}$ to another state $\mathsf{q}^{\prime}$ such that
$\mathcal{B}(\mathsf{q}^{\prime},\mathsf{adr})-\mathcal{B}(\mathsf{q},\mathsf{adr})>0$,
i.e., the adversary $\mathsf{adr}$ generates profit when the sequence of
actions $\mathbf{S}$ is executed with the concrete values.

Problem formulation. Given a specification $\varphi$ (which contains
vulnerable contract addresses or action candidates) and a blockchain state
$\mathsf{q}$, the objective is to find an attack vector consisting of a
concretization of the symbolic actions vector
$\mathbf{S}=\ell_{\mathsf{adr}1}\ldots\ell_{\mathsf{adr}n}$ s.t.
$\ell_{\mathsf{adr}i}\in\Sigma\cap\varphi$ for $1\leq i<n$, transforming the
state $\mathsf{q}$ to a state $\mathsf{q}^{\prime}$, and that maximizes the
profit of an adversary $\mathsf{adr}$,
$\mathcal{B}(\mathsf{q}^{\prime},\mathsf{adr})-\mathcal{B}(\mathsf{q},\mathsf{adr})$.

##  5\. FlashSyn

###  5.1. Symbolic Actions Vectors Synthesis

Algorithm 1 gives the overall synthesis procedure of FlashSyn. FlashSyn first
collects initial data points to approximate the actions in $\mathbf{Act}$
(line 3) where FlashSyn uses the state $\mathsf{q}$ as a starting blockchain
state. Then, using the sub-procedure Approximate FlashSyn generates the
approximations $\mathsf{ApproxAct}$ of the actions in $\mathbf{Act}$ using the
collected data points (line 5). FlashSyn uses the sub-procedure ActionsVectors
to generate all possible symbolic actions vectors of length less than
$\mathsf{len}$ (line 6). FlashSyn then iterates over the generated actions
vectors and uses some heuristics implemented in the sub-procedure IsFeasible
to prune actions vectors (line 8). For instance, an actions vector containing
two adjacent actions invoking the same method can be pruned to an actions
vector where the two adjacent actions are merged. Afterwards, using the
actions vector and approximated transition functions, the sub-procedure
Construct constructs the optimization framework $\mathcal{P}$ for the actions
vector (line 9). Then, FlashSyn uses the optimization sub-procedure Optimize
(line 10) to find the optimal concrete values to pass as input parameters to
the methods in the actions vector that satisfy the constraints of
$\mathcal{P}$. FlashSyn then validate whether the attack vector generated by
the optimizer indeed generates the profit with the sub-procedure QueryOracle
to execute the generated attack vectors on the blockchain. If the query is
successful, i.e., the actual profit closely matches the profit found by the
optimizer, FlashSyn adds the attack vector to the list of discovered attacks.
Otherwise, FlashSyn considers the attack vector to be a counterexample, and
uses it to generate new data points to refine the approximation in the
subsequent iterations, within the sub-procedure CEGDC (referenced in line 14
and introduced later in Section 5.4). FlashSyn repeats the process until the
number of iterations reaches $\mathsf{n}$ (line 4).

1:procedure Synthesize($\mathbf{Act}$, $\mathsf{len}$, $\mathsf{P}$,
$\mathsf{q}$, $\mathsf{n}$)

2: for each $\mathsf{a}\in\mathbf{Act}$

3:
$\mathsf{datapoints}[\mathsf{a}]\leftarrow\textsc{DataCollect}(\mathsf{q},\mathsf{a});$

4: for each $i\in[0;\ \mathsf{n}]$

5:
$\mathsf{ApproxAct}\leftarrow\textsc{Approximate}(\mathbf{Act},\mathsf{datapoints});$

6:
$\mathsf{wlist}\leftarrow\textsc{ActionsVectors}(\mathsf{ApproxAct},\mathsf{len});$

7: for each $\mathsf{p}\in\mathsf{wlist}$

8: if $\textsc{IsFeasible}(\mathsf{p})$

9: $\mathcal{P}\leftarrow\textsc{Construct}(\mathsf{p},\mathsf{ApproxAct})$

10:
$(\mathsf{p}^{\star},\textsf{profit})\leftarrow\textsc{Optimize}(\mathsf{p},\mathcal{P})$;

11: if $\textsc{QueryOracle}(\mathsf{q},\mathsf{p}^{\star},\textsf{profit})$

12: $\mathsf{answerlist}.\textsf{add}(\mathsf{p}^{\star},\textsf{profit})$;

13: else

14:
$\mathsf{datapoints}:=\mathsf{datapoints}\cup\textsc{CEGDC}(\mathsf{p}^{\star},\mathsf{q})$;

15: return $\mathsf{answerlist}$;

Algorithm 1 Attack vectors synthesis procedure. Its inputs are actions
$\mathbf{Act}$, the maximum length $\mathsf{len}$, a blockchain state
$\mathsf{q}$, and a threshold number of iterations $\mathsf{n}$. Its outputs
are attack vectors that yield positive profits.

###  5.2. Pruning Symbolic Actions Vectors

The sub-procedure IsFeasible implements some heuristics to prune undesired
symbolic actions vectors.

Heuristic 1: no duplicate adjacent actions. Two successive calls to the same
method in a DeFi smart contract are usually equivalent to a single call with
larger parameters. Thus, we discard actions vectors containing duplicate,
successive actions.

Heuristic 2: limited usage of a single action. Using the observation that
attack vectors do not contain repetitions, we fix a maximum number of calls to
a single method an attack can contain and discard actions vectors that do not
satisfy this criterion, e.g., an actions vector of length $4$ cannot contain
more than $2$ calls to the same method.

Heuristic 3: necessary preconditions. Based on the observation that owning
certain tokens is a necessary precondition for invoking some actions, FlashSyn
prunes symbolic actions vectors that contain actions requiring tokens666Note a
token can be standard tokens (ERC20, BEP20), or any other forms of tokens such
as debt tokens or share tokens. not owned by the attacker. For example, in
Harvest USDC example, invoking _withdraw_ method requires users own some share
tokens (fUSDC) beforehand. The only action candidate that mints fUSDC for
users is _deposit_ ; thus, this heuristic mandates that _deposit_ must be
called before invoking _withdraw_. This heuristic establishes a necessary but
not sufficient condition to ensure that synthesized attack vectors will not be
reverted.

###  5.3. Optimization

Given a symbolic actions vector and their approximated transit functions, the
sub-procedure Construct constructs an optimization framework to find optimal
values for the parameters for the actions. Recall that given a blockchain
state $\mathsf{q}$ and an address $\mathsf{adr}$, the actions vector
$\mathbf{S}$ transforms $\mathsf{q}$ to another state $\mathsf{q}^{\prime}$.
The objective function in the optimization problem targets to increase the
tokens values in the balance of the address $\mathsf{adr}$, i.e.,
$y=\mathcal{B}(\mathsf{q}^{\prime},\mathsf{adr})-\mathcal{B}(\mathsf{q},\mathsf{adr})$.
The optimization problem is accompanied by constraints on the symbolic values
to be inferred. For instance, the balance of any token $\mathbf{t}$ for any
address $\mathsf{adr}^{\prime}$ must always be non-negative, i.e., the
adversary and the smart contracts cannot use more tokens than what they have
in their balances, otherwise the transaction reverts. In the following, we
give the definition of the optimization problem.

$\displaystyle\mathcal{P}:\ \ \ $
$\displaystyle\begin{cases}\max_{p_{0},p_{1},...,p_{n}}\
y=\mathcal{B}(\mathsf{q}^{\prime},\mathsf{adr})-\mathcal{B}(\mathsf{q},\mathsf{adr})\\\
\textrm{subject to: }\forall\
\mathbf{t}\in\mathbf{T},\mathsf{adr}^{\prime}\in\mathbf{A}.\
\mathbf{M}(\mathsf{q}^{\prime},\mathsf{adr}^{\prime},\mathbf{t})\geq
0\end{cases}$

###  5.4. Counterexample Guided Data Collection (CEGDC)

The optimization sub-procedure might explore parts of the states space not
explored during the initial data points collection. This might challenge the
accuracy of the approximations and result in mismatch between the estimated
and the actual values. Thus, it is necessary to collect new data points based
on the counterexamples that show the mismatch between the estimated and the
actual values, to refine the approximations. Therefore, we propose
counterexample guided data collection (CEGDC), inspired of counterexample
guided abstraction refinement (Clarke et al., 2000), to refine approximations
when mismatches are identified.

We use $\mathbf{C}$ to denote the attack vector s.t.
$\mathsf{q}\xrightarrow{\mathbf{C}}\mathsf{q}^{\prime}$.
$\mathsf{q}^{\prime}_{e}$ and $\mathsf{q}^{\prime}_{a}$ denote the estimated
value for the state $\mathsf{q}^{\prime}$ found by the optimizer and the
actual value obtained when executing $\mathbf{C}$ on the actual protocol on
the blockchain, respectively.
$\mathcal{P}_{e}(\mathbf{C})=\mathcal{B}(\mathsf{q}^{\prime}_{e},\mathsf{adr})-\mathcal{B}(\mathsf{q},\mathsf{adr})$
and
$\mathcal{P}_{a}(\mathbf{C})=\mathcal{B}(\mathsf{q}^{\prime}_{a},\mathsf{adr})-\mathcal{B}(\mathsf{q},\mathsf{adr})$
denote the estimated profit and actual profit, respectively.

###### Definition 5.0.

A counterexample is an attack vector $\mathbf{C}$ whose estimated profit
$\mathcal{P}_{e}(\mathbf{C})$ is different from its actual profit
$\mathcal{P}_{a}(\mathbf{C})$. Formally,
$|\mathcal{P}_{e}(\mathbf{C})-\mathcal{P}_{a}(\mathbf{C})|\geq\varepsilon\cdot(|\mathcal{P}_{e}(\mathbf{C})|+|\mathcal{P}_{a}(\mathbf{C})|)$,
where $\varepsilon$ is a small constant representing accuracy tolerance.

1:procedure CEGDC($\mathbf{C}$, $\mathsf{q}$)

2: $\mathsf{datapoints}\leftarrow[\ ]$;

3: for each $k\in[len(\mathbf{C});\ 1]$;

4:
$\mathsf{q}^{\prime}_{e}\leftarrow\textsc{Estimate}(\mathsf{q},\mathbf{C},k);$

5:
$\mathsf{q}^{\prime}_{a}\leftarrow\textsc{Execute}(\mathsf{q},\mathbf{C},k);$

6: if $\textsc{IsAccurate}(\mathsf{q}^{\prime}_{e},\mathsf{q}^{\prime}_{a})$

7: returns $\mathsf{datapoints}$ ;

8: else

9: $(\mathsf{a},\textsf{paras})\leftarrow\mathbf{C}[k]$;

10:
$\mathsf{datapoints}[\mathsf{a}]\leftarrow(\mathsf{q},\textsf{paras},\mathsf{q}^{\prime}_{a})$;

11: return $\mathsf{datapoints}$;

Algorithm 2 Counterexample guided data collection procedure. It takes a
counterexample $\mathbf{C}$ and a state $\mathsf{q}$, and returns datapoints.
$k\in[n;1]$ means that in the first iteration $k=n>0$.

In Algorithm 2, we present the sub-procedure CEGDC for collecting new data
points from a counterexample. CEGDC takes as inputs a counterexample
$\mathbf{C}$ which is known to have an inaccurate profit estimation, and a
blockchain state. The for loop on line 3 is used to locate approximation
errors backward from the last action to the first action and collect new data
points accordingly. In a loop iteration $k$, FlashSyn checks if the estimated
methods of the action at the index $k$ of $\mathbf{C}$ are accurate. First,
FlashSyn computes the estimated state $\mathsf{q}^{\prime}_{e}$ reached by
executing $\mathbf{C}$ until reaching the action indexed $k$ (line 4) using
the approximated transition functions. Second, FlashSyn fetches the actual
state $\mathsf{q}^{\prime}_{a}$ reached by executing $\mathbf{C}$ until
reaching the action indexed $k$ (line 5) on the actual smart contracts on the
blockchain. Then, FlashSyn compares the estimated and actual execution results
(line 6). If the estimation is accurate, this indicates that the transition
functions of the action at the index $k$ of $\mathbf{C}$ and its predecessors
are accurate; so the procedure breaks the loop and returns the data points
computed in the previous iterations (line 7). Otherwise, it indicates
inaccurate transition functions of this action or/and its predecessors. Thus,
we add a new data point associated with the action at the index $k$ of
$\mathbf{C}$ (lines 9 and 10) and proceed to the next iteration of the loop to
explore the action predecessors.

###  5.5. FlashFind: Action Candidates Identification

Flash loan attacks typically focus on victim contracts containing functions
capable of transferring tokens,777Here, tokens refer to various forms of DeFi
tokens, including stable coins, debt tokens, share tokens, liquidity tokens,
asset tokens, etc. which can be invoked by regular users. The attacker
manipulates the transfer amount under specific conditions to make profit.

We designed and built a tool FlashFind to assist users of FlashSyn to select
action candidates likely to be involved in an attack vector. Given a set of
target smart contracts, FlashFind identifies action candidates in the
following steps.

####  5.5.1. Selecting Action Candidates from Contract Application Binary
Interfaces (ABIs)

For all verified smart contracts, their ABIs are made public to facilitate
users to call functions and engage with the contracts. An ABI typically
comprises (public or external) function names, argument names/types, function
state mutability, and return types. During the process of selecting action
candidates, certain functions can be safely ignored: (1) Functions with the
view or pure mutability can be excluded. (2) Functions that can only be
invoked by privileged users, such as _transferOwnership_ and _changeAdmin_ ,
can also be disregarded since they are unlikely to be accessed by regular
users888Previous works (Ghaleb et al., 2023; Liu et al., 2022) have
extensively researched access control vulnerabilities. We exclude them from
the scope of this work.. (3) Token permission management functions/parameters,
such as the function _approve_ or parameter deadline, are excluded999To
simplify the search process of FlashSyn, these permissions are assumed to be
granted maximally.. These functions/parameters solely control whether a
transaction will be reverted or not and do not affect the behaviors of
contracts.

####  5.5.2. Learning Special Parameters from Transaction History

After selecting a set of action candidates from contracts’ ABIs, some non-
integer parameters(eg. bytes, string, address, array, enum) can still be
unknown. FlashFind collects past transactions of the target contracts and
extracts function level trace data from these transactions, and utilizes the
trace data to learn the special parameters from previous function calls made
to the contract.

####  5.5.3. Local Execution and Intra-dependency Analysis

After learning special parameters, each action candidate is executed at a
given block to verify its executability. An action candidate may not be
executable due to various reasons: (1) the function is disabled by the owner
or admin; (2) internal function calls to other contracts are disabled by the
owners or admins of those contracts; (3) the function is not valid under
current blockchain states. The inexecutability due to these reasons cannot be
identified by static analysis and can only be determined by executions. All
such inexecutable functions are filtered out.

FlashFind automatically collects storage read/write information during the
execution of these functions and infers the Read-After-Write (RAW)
dependencies101010This RAW dependency information is also employed in
FlashSyn’s initial data collection to expand the range of data points. between
different action candidates. An action A has a RAW dependency (or
equivalently, is RAW dependent) on action B if the execution of action A reads
the storage written by action B111111It is important to note that this step
excludes any tx.origin/msg.sender-related storage reads/writes, as such
storage accesses do not alter the global state of the protocol and are
therefore unlikely to impact the functional behaviors of actions.. From the
RAW dependencies, it is possible to observe that certain functions behave
independently, meaning they do not have any RAW dependencies on other
functions, and other functions do not have any RAW dependencies on them
either. Consequently, these independent functions can be safely ignored.

After analyzing ABIs, transaction history, and local executions, FlashFind
generates a list of action candidates with only their integer arguments left
undetermined. These action candidates are then input into FlashSyn for further
synthesis.

##  6\. Implementation

FlashSyn is implemented in Python. Figure 3 shows an overview of our
implementation.

Figure 3. An Overview of FlashSyn Implementation

The components Runner, Synthesizer, Approximator, and Optimizer implement the
FlashSyn synthesis procedure presented in Algorithm 1. An optional component
FlashFind is used to automatically identify action candidates.

(1) Approximator. Approximator approximates the transition functions using
data points collected by Runner. The approximated transition functions are
then given to Optimizer to construct the optimization framework. In
Approximator, all transition functions of an action are approximated unless
the transition functions are straightforward assignment/addition/subtraction
(by simple inspection of smart contract codes), or the action is very common
(such as Uniswap that has been widely studied (Qin et al., 2021; Xia et al.,
2021; Xu et al., 2021)). FlashSyn implements two numerical methods using
external libraries. FlashSyn-poly utilizes sklearn (Pedregosa et al., 2011;
Buitinck et al., 2013), and FlashSyn-inter employs scipy (Virtanen et al.,
2020). The choice of polynomial and interpolation methods is motivated by
several considerations. First, FlashSyn requires fast evaluation of
approximated functions, as thousands of evaluations are performed in the
optimization process. Second, when provided with an input not seen before, the
approximation method needs to yield a reasonable estimation based on the
nearest points. Lastly, given that a typical FlashSyn process involves
learning dozens of approximated formulas, the approximation process for one
formula should not exceed a few seconds. Polynomial and interpolation methods
are the two most popular approximation approaches that meet all of these
criteria and there are off-the-shelf tools like sklearn and scipy that are
easy to intergate in FlashSyn.

(2) Optimizer. Optimizer automatically builds an optimization problem using
the approximated transition functions returned by Approximator and the
symbolic actions vectors enumerated by Synthesizer and performs global
optimization on it. The obtained attack vector that yields a positive profit
is then executed by Runner to confirm the accuracy of the estimation. If the
estimation is inaccurate, the attack vector is treated as a counterexample and
is used to collect new data points by Runner that are used by Approximator to
refine the approximation. We built Optimizer on top of an off-the-self global
optimizer scipy.optimize.shgo (Joe and Kuo, 2008; Endres et al., 2018; Wales,
2015), which solves the simplicial homology global optimization algorithm to
find the optimal parameters.121212Note that we were not able to use local
optimizers in scipy.optimize library (Virtanen et al., 2020) which require an
initial guess of parameters. Under our settings, it is not feasible to find an
initial guess for every symbolic attack, as each attack behaves differently.
In FlashSyn-poly, we parallelized Optimizer component using up to $18$
processes where Optimizer is run over multiple symbolic actions vectors in
parallel.

(3) Runner. Runner executes transactions on a forked blockchain. It performs
both initial and counterexample based data collection, and validates results
of Optimizer. We implemented Runner on top of Foundry (Foundry Contributors,
2023), a toolkit written in Rust for smart contracts development that allow to
interact with EVM based blockchains.

(4) Synthesizer. Synthesizer first enumerates and prunes symbolic actions
vectors using heuristics. Then, during counterexample guided loops, it employs
priority scoring to gradually drop actions vectors based on their scores.
Synthesizer uses iterative synthesis. Optimizer can be configured with
different hyperparameters to perform different strengths of parameter search.
We designed $3$ sets of hyperparameters which represent different strengths of
parameter search. Synthesizer first conducts a weakest parameter search on all
enumerated symbolic actions vectors using Optimizer. After Runner validates
the results, Synthesizer ranks symbolic actions vectors and drops the ones
with low priority scores. The actions vector with high priority score will be
searched with higher strengths. Specifically, if a symbolic actions vector
yields a positive profit $\mathcal{P}$ in iteration $k$, its priority score of
iteration $k+1$ is $\mathcal{P}$. If a symbolic actions vector does not yield
a positive profit in iteration $k$, it is given a small priority score between
$1$ and $10$ based on Optimizer results. An actions vector will also be
dropped when its priority score does not increase between iterations. When all
actions vectors are dropped, the whole synthesis procedure stops, and FlashSyn
returns all the profitable attack vectors it found.

(5) FlashFind. We also implemented FlashFind as an optional component.
FlashFind uses TrueBlocks (Rush, 2023) and Blockchain Explorers (Etherscan
(Etherscan, 2023), BscScan (BscScan, 2023), and FtmScan (FTMScan, 2023)) to
collect past transactions of the target contracts. FlashFind employs Phalcon
(BlockSec, 2023) and Foundry (Foundry Contributors, 2023) to extract function
level trace data from those transactions and perform analysis on storage
accesses. Our evaluation shows that FlashFind is able to identify action
candidates and helps FlashSyn discovers alternative attack vectors (see RQ4 in
Section 7).

FlashSyn does not require prior knowledge of a vulnerable location or
contract. Given a set of DeFi lego user interface contracts, action candidates
and their special parameters such as strings are given by the users or
automatically extracted from transaction history using FlashFind. FlashSyn
utilizes these action candidates to synthesize attack vectors and search for
optimal numerical values. Note that these action candidates are not
necessarily the ones that contain the vulnerability. Rather, they serve as
user interfaces for interacting with the protocol. The vulnerability may
reside in any contract invoked through nested calls originating from these
action candidates. If FlashFind is not utilized, users can consult the
protocol documentation to identify the appropriate user-interface contracts
and functions (action candidates), as well as how to select special parameters
for invoking these functions. Such information is essential for any user
interacting with the protocol, and is generally available in the
documentations of DeFi protocols.

Table 2. Benchmark of Attacks Used in the Evaluation.

| Benchmark | #C+ | LoC∗ | Vulnerability Type | Tx
---|---|---|---|---|---
ETH | bZx1 | 6 | 4964 | pump&arbitrage | (Etherscan, 2020a)
Harvest_USDT | 6 | 6446 | manipulate oracle | (Etherscan, 2020d)
Harvest_USDC | 6 | 4095 | manipulate oracle | (Etherscan, 2020e)
Eminence | 2 | 489 | design flaw† | (Etherscan, 2020c)
ValueDeFi | 8 | 7043 | manipulate oracle | (Etherscan, 2020g)
Cheesebank | 12 | 1246 | manipulate oracle | (Etherscan, 2020b)
Warp | 11 | 13139 | manipulate oracle | (Etherscan, 2020h)
Yearn | 5 | 2200 | forced investment | (Etherscan, 2021)
inverseFi | 7 | 5734 | manipulate oracle | (Etherscan, 2020f)
BSC | bEarnFi | 3 | 3007 | asset mismatch | (BscScan, 2021c)
AutoShark | 6 | 8052 | design flaw† | (BscScan, 2021b)
ElevenFi | 7 | 5613 | design flaw† | (BscScan, 2021d)
ApeRocket | 7 | 1562 | design flaw† | (BscScan, 2021a)
WDoge | 2 | 788 | deflationary token | (BscScan, 2022b)
Novo | 4 | 7080 | design flaw† | (BscScan, 2022a)
FTM | OneRing | 14 | 5386 | design flaw† | (FtmScan, 2022)
DVD | Puppet | 2 | 742 | manipulate oracle | (Damn Vulnerable DeFi, 2023b)
PuppetV2 | 1 | 161 | manipulate oracle | (Damn Vulnerable DeFi, 2023c)
Total Financial Loss in History | 82.5 million USD

##  7\. Evaluation

We aim to answer the following research questions:

  1. RQ 1:

How effective is FlashSyn in synthesizing flash loan attack vectors?

  2. RQ 2:

How well does the synthesis-via-approximation technique perform compared to
precise baselines?

  3. RQ 3:

How much does counterexample driven approximation refinement improve
FlashSyn’s results?

  4. RQ 4:

How effective is the combination of FlashFind and FlashSyn to synthesize
attack vectors end-to-end?

Scope: FlashSyn focuses on flash loan attacks that generate positive profit by
sequentially invoking functions within existing DeFi contracts. Security
attacks that require exploiting other vulnerabilities such as re-entrance or
conducting social engineering are outside the scope of FlashSyn and our
evaluation. The goal of FlashSyn is to prove the existence and the
exploitability of flash loan vulnerabilities. Consequently, activities such as
getting and repaying the flash loan are not part of our synthesis task.

Benchmarks: We investigated historical flash loan attacks that span from
02/14/2020 to 06/16/2022 across Ethereum, Binance Smart Chain (BSC), and
Fantom (FTM) and attempted to reproduce each of them in our environment. In
the end, we reproduced $16$ attacks that are within our scope and collected
them as our benchmark attacks. These attacks invoked $2$-$14$ contracts of the
victim protocol in the nested invocation tree per attack, consisting of a
total of $489$ to $13,139$ lines of code, reflecting the multifaceted nature
of the DeFi protocols exploited in real-world flash loan attacks. Also,
protocols in our benchmark contain up to $15$ action candidates from which
FlashSyn needs to find an attack vector. Altogether, the $16$ historical flash
loan attacks in our benchmark have caused over $82.5$ million US dollars in
losses and include widely-known cases such as Harvest, bZx, and Eminence.
Additionally, we include $2$ fictional attacks from the Damn Vulnerable DeFi
(DVD) challenges (Damn Vulnerable DeFi, 2023a).

Ground Truth: For historical flash loan attacks, we forked the corresponding
blockchain at one block prior to the attack transaction and replayed the
attacker’s attack vector as the ground truth. For DVD benchmarks, we select
community solutions as ground truth. Note that in a flash loan attack, if the
same attack vector is repeated multiple times, we remove the loop and only
consider the first attack vector as the ground truth.

Table 3. Summary of FlashSyn Results. AC denotes the number of action candidates. AP denotes the number of action candidates to approximate. GL and GP denote the length and the profit of the ground truth attack vector, respectively. IDP and TDP denote the initial and total number of collected of data points, respectively. Time denotes the time spent in seconds. | FlashSyn-poly | FlashSyn-inter | Precise
---|---|---|---
Benchmark | AC | AP | GL | GP | IDP | TDP | Profit | Time | TDP | Profit | Time | Profit
bZx1 | 3 | 3 | 2 | 1194 | 5192 | 5849 | 2392 | 422 | 6373 | $2302^{\dagger}$ | 441 | cs
Harvest_USDT | 4 | 4 | 4 | 338448 | 8000 | 9325 | $110139^{\dagger}$ | 670 | 10289 | $86798^{\dagger}$ | 7579 | cs
Harvest_USDC | 4 | 4 | 4 | 307416 | 8000 | 8912 | $59614^{\dagger}$ | 677 | 10914 | $110051^{\dagger}$ | 8349 | cs
Eminence | 4 | 4 | 5 | 1674278 | 8000 | 8780 | 1507174 | 1191 | 8104 | / | / | 1606965
ValueDeFi | 6 | 6 | 6 | 8618002 | 12000 | 19975 | $8378194^{\dagger}$ | 4691 | 15758 | $6428341^{\dagger}$ | 11089 | cx
CheeseBank | 8 | 3 | 8 | 3270347 | 2679 | 2937 | $1946291^{\dagger}$ | 4391 | 2715 | $1101547^{\dagger}$ | 10942 | $2816762^{\dagger}$
Warp | 6 | 3 | 6 | 1693523 | 6000 | 6000 | $2773345^{\dagger}$ | 1164 | 6000 | / | / | $2645640^{\dagger}$
bEarnFi | 2 | 2 | 4 | 18077 | 4000 | 4854 | 13770 | 470 | 4652 | 12329 | 688 | 13832
AutoShark | 8 | 3 | 8 | 1381 | 2753 | 2753 | $1372^{\dagger}$ | 5484 | 2753 | / | / | cx
ElevenFi | 5 | 2 | 5 | 129741 | 4000 | 4070 | 129658 | 409 | 4326 | 85811 | 898 | cx
ApeRocket | 7 | 3 | 6 | 1345 | 6000 | 6402 | $1333^{\dagger}$ | 733 | 6235 | $1037^{\dagger}$ | 3238 | cs
Wdoge | 5 | 1 | 5 | 78 | 2000 | 2001 | 75 | 272 | 2080 | 75 | 289 | 75
Novo | 4 | 2 | 4 | 24857 | 4000 | 4164 | 20210 | 702 | 4031 | 23084 | 861 | cx
OneRing | 2 | 2 | 2 | 1534752 | 4000 | 4710 | 1814882 | 585 | 4218 | 1942188 | 367 | cx
Puppet | 3 | 3 | 2 | 89000 | 6000 | 6301 | $89000^{\dagger}$ | 1203 | 6452 | $87266^{\dagger}$ | 1238 | $89000^{\dagger}$
PuppetV2 | 4 | 3 | 3 | 953100 | 4491 | 4836 | $747799^{\dagger}$ | 2441 | 5061 | $362541^{\dagger}$ | 2835 | $647894^{\dagger}$
|  Solved:16/18 Avg. Time: 1594 |  Solved:13/18 Avg. Time: 3754 |

Precise Baseline: To demonstrate the effectiveness of synthesis-via-
approximation techniques, we implemented a baseline synthesizer that works
with manual summaries of smart contract actions. Specifically, we manually
inspected all benchmarks whose relevant smart contracts that are all open-
source and for each benchmark we allocated more than $4$ manual analysis hours
to extract the precise mathematical summaries. The baseline synthesizer then
uses the manually extracted precise summaries to drive the synthesis.

Environment Setup: We assume that the flash loan providers are generally
available, and we do not consider the borrow and the return as the part of the
synthesis task. To facilitate FlashSyn experimentation, we manually annotated
the prestates and poststates for each action. The details of this annotation
process are described in Appendix C. Although this manual effort is required,
it’s worth noting that automation of this step is possible. Techniques such as
dynamic taint analysis and forward symbolic execution can be employed to
automatically identify which storage variables influence the change in token
balances, thereby streamlining the annotation of prestates and poststates. The
experiments are conducted on an Ubuntu $22.04$ server, with an AMD Ryzen
Threadripper 2990WX $32$-Core Processor and $128$ GB RAM.

Experiment Overview. To answer RQ 1, we apply FlashSyn to the $18$ benchmarks
with the same set of candidate actions in ground truths. For each candidate
action, the prestates and poststates are annotated for FlashSyn to drive the
approximated formula for this action. We set a timeout of $3$ hours for
FlashSyn-poly and $4$ hours for FlashSyn-inter. FlashSyn does not know a
priori whether a benchmark has an attack vector with a positive profit, and it
does not set any bounds on the profit. It tries iteratively to synthesize an
attack vector with a maximum profit. FlashSyn’s refinement loop is guided by
intermediate results and FlashSyn stops when it cannot improve the profit or
the above timeouts are reached. To answer RQ 2, we replace Approximator
component of FlashSyn with manually extracted precise mathematical summaries,
and conduct the same experiment with $4$ hours timeout. To answer RQ 3, we
evaluate FlashSyn with different initial data points and with CEGDC
enabled/disabled. To answer RQ 4, we first use FlashFind to identify candidate
actions from given contract addresses which the hacker used in history,
manually annotate them as in RQ 1, and then apply FlashSyn with this new set
of candidate actions to synthesize attack vectors under the same setting as in
RQ 1. The results for RQ 1+RQ 2, RQ 3, RQ 4 are summarized in Table 3, Table
4, and Table 5, respectively.

Table 4. Summary of FlashSyn Results under Different Settings (see Appendix F for complete results). n+x: n denotes the settings of initial number of data points and +x denotes whether FlashSyn uses counterexample driven loops.  | FlashSyn-poly | FlashSyn-inter
---|---|---
| 200 | 200+x | 500 | 500+x | 1000 | 1000+x | 2000 | 2000+x | 200 | 200+x | 500 | 500+x | 1000 | 1000+x | 2000 | 2000+x
Avg. Time (s) | 632 | 893 | 1120 | 1747 | 842 | 1397 | 982 | 1594 | 2601 | 3509 | 3180 | 3917 | 3022 | 3845 | 3200 | 3754
Avg. Data Points | 584 | 1042 | 1432 | 2376 | 2795 | 3571 | 5445 | 6367 | 584 | 1338 | 1432 | 2450 | 2795 | 3656 | 5445 | 6248
Avg. Norm. Profit | 0.793 | 0.829 | 0.846 | 0.922 | 0.762 | 0.786 | 0.717 | 0.945 | 0.539 | 0.555 | 0.630 | 0.634 | 0.535 | 0.580 | 0.594 | 0.641
Benchmarks Solved | 15 | 15 | 15 | 16 | 15 | 15 | 15 | 16 | 13 | 13 | 14 | 14 | 13 | 13 | 13 | 13

RQ1: Effectiveness of FlashSyn. Table 3 summarizes the results of the
experiment. The first five columns of Table 3 list benchmark information
including the number of actions to be approximated and the length of the
ground truths. The four columns under FlashSyn-poly list data concerning the
synthesis using polynomial approximations. The four columns under FlashSyn-
inter list data concerning the synthesis using interpolation based
approximation.

Our results in Table 3 show that FlashSyn can effectively synthesize flash
loan attack vectors. FlashSyn-poly (resp., FlashSyn-inter) synthesizes
profitable attack vectors for $16$ (resp., $13$) benchmarks with an average
normalized profit (w.r.t. the ground truth profit) of $0.945$ (resp.,
$0.641$). In particular, for three benchmarks (_ApeRocket_ , _ElevenFi_ , and
_AutoShark_) the profits found by FlashSyn-poly are within $99\%$ of the
profits in the original attacks vectors. Surprisingly in another three
benchmarks (_bZx1_ , _Warp_ , and _OneRing_) the profits found by FlashSyn are
bigger than the profits in the original attacks vectors. For instance, in the
_Warp_ benchmark the profit is roughly double the ground truth profit (see
Appendix B for Warp case study). On average, FlashSyn-poly is $\times 2$
faster than FlashSyn-inter, because we used parallelism in FlashSyn-poly which
is not possible for FlashSyn-inter.

For $10$ benchmarks, FlashSyn successfully discovers new profitable symbolic
actions vectors that are different from the ground truths. These vectors
either exploit the same vulnerability but in a different order of actions, or
represent arbitrage opportunities that were not exploited by the original
attackers. For the remaining $6$ benchmarks, FlashSyn discovers exactly the
same symbolic actions vectors as the ground truths but with different
parameters. Note that FlashSyn is not able to solve _Yearn_ and _InverseFi_
which are not shown in Table 3. These two benchmarks put high requirements on
the precision of the approximation and small miss-approximation errors caused
FlashSyn to miss finding attack vectors and accurate parameters.

To evaluate the efficacy of the pruning heuristics introduced in Section 5.2,
we conduct experiments comparing the search space sizes when using FlashSyn
with and without the application of some of the heuristics. Our results
indicate that Heuristic 1 leads to an average reduction of $57\%$ in the
search space size. Subsequently, Heuristic 2 further reduces the remaining
search space by an additional $34\%$, and Heuristic 3 contributes an
additional reduction of $65\%$ to the remaining search space.

To compare FlashSyn with existing static analyzers, we manually select
contracts containing vulnerabilities in the benchmarks and apply the popular
smart contracts static analyzer Slither (Feist et al., 2019) to them. In the
experiments, we identify contracts that contain the root cause of the
vulnerabilities as the target contracts for Slither to analyze. Note that in
practice, identifying target contracts for Slither is much harder than that
for FlashFind. For FlashFind, the target contracts are simply user-interface
contracts. In contrast, identifying the contract with the actual
vulnerability, such as a contract invoked in a deeply nested call chain, can
be tedious. Slither fails to detect vulnerabilities for all $18$ benchmarks,
among them Slither fails to parse $2$ benchmarks (Novo and Yearn). The
possible reasons include: (i) Slither’s inability to reason across multi-
contract interactions, common in flash loan attacks; and (ii) its lack of
context awareness, such as not detecting Uniswap (Uniswap Labs, 2023) when
used as an oracle.

RQ2: Comparison with Precise Baseline. The last column of Table 3 lists data
when the approximation component of FlashSyn is replaced with precise
mathematical summaries for actions. Note that $4$ benchmarks are partially
closed-source (cs), and $5$ benchmarks are too complicated (cx), thus we are
not able to extract mathematical precise summaries for them. For others, we
list the profit generated using the manually extracted mathematical
expressions in the synthesizer and optimizer.

Our results in Table 3 show that the synthesis-via-approxima- tion approach
performs well compared to precise baselines. For the $9$ cases that the
precise baseline failed due to either close source (cs) or complicated
contract logics (cx), FlashSyn found attack vectors that generate positive
profits. On average, for the $7$ cases that the precise baseline succeeds, the
best profit from FlashSyn is $0.97$ of the profit returned by the precise
baseline. In particular, for _Warp_ and _PuppetV2_ FlashSyn synthesizes an
attack vector with a profit higher than that obtained by the precise approach.
This is because the approximations used in FlashSyn are simpler than the
mathematical summaries used in precise baseline. This enables the optimizer to
converge faster and find better parameter values within the fixed time budget.

RQ3: Counterexample Driven Approximation Refinement. Table 4 summarizes the
evaluation of FlashSyn under different settings. In particular, we evaluated
FlashSyn with $200$, $500$, $1000$, and $2000$ initial data points threshold
per action to be approximated without and with counterexample loop. The Avg.
rows in Table 4 are calculated based on the $16$ benchmarks excluding _Yearn_
and _InverseFi_. The Avg. Norm. Profit is calculated as the average of
normalized profits, i.e., profit / ground truth profit.

For FlashSyn-poly, the results in Table 4 show that only with counterexample
loop we are able to solve the $16$ benchmarks (Columns 500+x and 2000+x).
Also, the maximum average of normalized profits is achieved with
counterexample loop (Column 2000+x) which improved from $0.717$ (Column 2000)
without counterexample loop to $0.945$ with counterexample loop. For FlashSyn-
inter, the maximum average of normalized profits is also achieved with
counterexample loop (Column 2000+x) which improved from $0.594$ (Column 2000)
without counterexample loop to $0.641$ with counterexample loop.

Table 5. Summary of Evaluation Results of Combining FlashSyn with FlashFind. AC is the number of action candidates. AP is the number of action candidates to approximate. GL and GP are the length and the profit of the ground truth attack vector, respectively. IDP and TDP are the initial and total number of collected of data points, respectively. Time is measured in seconds. | FlashFind + FlashSyn-poly | FlashSyn-poly
---|---|---
Benchmark | GL | GP | AC | AP | IDP | TDP | Profit | Time | AC | AP | IDP | TDP | Profit | Time
bZx1 | 2 | 1194 | 3 | 3 | 5192 | 5849 | 2392 | 422 | 3 | 3 | 5192 | 5849 | 2392 | 422
Harvest_USDT | 4 | 338448 | 15 | 15 | 30000 | 34052 | $85593^{\ddagger}$ | 5514 | 4 | 4 | 8000 | 9325 | $110139^{\dagger}$ | 670
Harvest_USDC | 4 | 307416 | 15 | 15 | 30000 | 51726 | $33645^{\ddagger}$ | 3630 | 4 | 4 | 8000 | 8912 | $59614^{\dagger}$ | 677
Eminence | 4 | 1674278 | 4 | 4 | 8000 | 8780 | 1507174 | 1191 | 4 | 4 | 8000 | 8780 | 1507174 | 1191
ValueDeFi | 6 | 8618002 | 6 | 6 | 12000 | 19975 | $8378194^{\dagger}$ | 4691 | 6 | 6 | 12000 | 19975 | $8378194^{\dagger}$ | 4691
Warp | 6 | 1693523 | 8 | 5 | 7772 | 7772 | $2776351^{\ddagger}$ | 3129 | 6 | 3 | 6000 | 6000 | $2776351^{\dagger}$ | 1164
bEarnFi | 4 | 18077 | 2 | 2 | 4000 | 4854 | 13770 | 470 | 2 | 2 | 4000 | 4854 | 13770 | 470
ApeRocket | 6 | 1345 | 11 | 5 | 10000 | 10706 | $1179^{\ddagger}$ | 3064 | 7 | 3 | 6000 | 6402 | $1333^{\dagger}$ | 733
Wdoge | 5 | 78 | 7 | 2 | 4000 | 4107 | $75^{\ddagger}$ | 769 | 5 | 1 | 2000 | 2001 | 75 | 272
Novo | 4 | 24857 | 6 | 2 | 4000 | 4172 | 15183 | 791 | 4 | 2 | 4000 | 4164 | 20210 | 702
OneRing | 2 | 1534752 | 8 | 8 | 16000 | 16614 | $1814877^{\ddagger}$ | 1104 | 2 | 2 | 4000 | 4710 | 1814882 | 585

RQ4: Effectiveness of FlashFind. In this experiment, we evaluate the
combination of FlashFind and FlashSyn on the $14$ benchmarks that FlashSyn was
able to synthesize a profitable attack vector in Table 3 excluding the two
fictional DVD benchmarks.131313DVD benchmarks do not have historical
transactions that FlashFind can use.. In particular, only contract addresses
are provided to FlashFind and FlashFind identifies candidate actions for
FlashSyn to synthesize attack vectors with the $2000$ initial data points
threshold per action configuration. Table 5 presents the results.

FlashFind successfully identifies a reasonable number of action candidates for
$11$ out of the $14$ benchmarks from given contract addresses. Among them,
FlashFind identifies additional candidate actions for $7$ benchmarks. For
instance, FlashFind identifies $6$ additional candidate actions for _OneRing_.
The remaining $3$ benchmarks contains action candidates whose arguments are
non-primitive types, and FlashFind identifies an excessive and impractical
number of choices from transaction history.141414In such cases, we believe
experienced security analysts could manually identify special parameters and
further reduce the number of parameter choices.

Even with the extra candidate actions FlashSyn was able to synthesize
profitable attack vectors for all $11$ benchmarks. Surprisingly in $6$
benchmarks, FlashSyn finds attack vectors that contains new action candidates
from FlashFind that are not in the ground truth. There are two possibilities:
First, the new action candidates identified by FlashFind are functionally
similar to one action in ground truths (e.g, _withdraw_ and _withdrawSafe_ for
_OneRing_). Replacing old actions with new ones gives new attack vectors.
Second, the new action candidates represent another way of draining assets
which the attacker failed to identify. For example, in the _Warp_ benchmark,
the attacker only invoked _borrowSC(USDC, v)_ and _borrowSC(DAI, v)_ to drain
USDC and DAI (Etherscan, 2020h; Rekt, 2020), however, FlashFind identifies
_borrowSC(USDT, v)_ as another candidate action, which could have been used to
drain USDT as well in the same transaction.

Impact. One author of this paper collaborated with Quantstamp for applying
FlashSyn for 3 months. We discovered two zero-day flash loan vulnerabilities
in two protocols under audit.

Threats to Validity: The internal threat to validity mainly lies in human
mistakes in the study. Specifically, we may understand results of FlashSyn
incorrectly, or make mistakes in the implementation of FlashSyn. All authors
have extensive smart contract security analysis experience and software
engineering expertise in general. To further reduce this threat, we manually
check the balance changes for the best results given by FlashSyn in each
benchmark. We verify that with the help of on-chain exchanges, these attack
vectors can generate a post-balance strictly larger than initial capital (see
Appendix E). The external threat to validity mainly lies in the subjects used
in our study. The flash loan attacks we study might not be representative. We
mitigate this risk by using diverse and reputable data sources, including
academic papers (Qin et al., 2021; Cao et al., 2021) and an industrial
database (SlowMist, 2023).

Limitations: Like most synthesis tools, FlashSyn faces scalability challenges.
The search space grows exponentially with the number of actions and attack
vector length. A practical approach is to assess protocols on a module by
module basis. By focusing only on inter-dependent actions within, we can
maintain both the number of actions and the attack vector length at manageable
levels, thereby mitigating the scaling issue.

##  8\. Related Work

Parametric optimization: For some flash loan attack cases, researchers (Cao et
al., 2021; Qin et al., 2021) manually extracted math formulas of function
candidates, manually defined related parameter constraints, and used an off-
the-shelf optimizer to search for parameters which yield the best profit.
However, this technique requires significant manual efforts and expert
knowledge of the underlying DeFi protocols. Consequently, it becomes
impractical for checking a large number of potential attack vectors. Note that
our benchmark set contains significantly more flash loan attacks than prior
work (Qin et al., 2021; Cao et al., 2021), i.e., $18$ versus $2$ in (Qin et
al., 2021) and $9$ in (Cao et al., 2021).

Static Analysis: Slither (Feist et al., 2019), Securify (Tsankov et al.,
2018), Zeus (Kalra et al., 2018), Park (Zheng et al., 2022) and SmartCheck
(Tikhomirov et al., 2018) apply static analysis techniques to verify smart
contracts. There are also several works that use symbolic execution (King,
1976) to explore the program states of a smart contract, looking for an
execution path that violates a user-defined invariant, e.g., Mythril
(ConsenSys, 2022), Oyente (Luu et al., 2016), FairCon (Liu et al., 2020),
ETHBMC (Frank et al., 2020), SmartCopy (Feng et al., 2019), and Manticore
(Mossberg et al., 2019). These techniques tend to operate with one contract at
a time and therefore cannot handle flash loan attacks that involve multiple
contracts. These techniques also may suffer from the complicated logics of the
DeFi contracts, and cause path explosion. FlashSyn uses its novel synthesis-
via-approximation techniques to avoid these issues.

Fuzzing: ContractFuzzer (Jiang et al., 2018), sFuzz (Nguyen et al., 2020),
ContraMaster (Wang et al., 2020), SMARTIAN (Choi et al., 2021) and ItyFuzz
(Shou et al., 2023) introduce novel fuzzing techniques to discover
vulnerabilities in smart contracts. However, these techniques either only work
on one contract or focus on specific vulnerabilities like re-entrancy.
Moreover, flash loan attack vectors can contain up to $8$ actions and $7$
integer parameters, which is unlikely to be found by random fuzzing.

Flash Loan Attacks: Prior works (Qin et al., 2021; Cao et al., 2021; Werapun
et al., 2022) study specific flash loan attacks and manually analyze and
optimize the attack vectors. Some other tools (Xia et al., 2023; Ramezany et
al., 2023; Wang et al., 2022) are designed to monitor flash loan attacks after
they happened. Other researchers investigate other usage of flash loans
including arbitrage (Wang et al., 2021) or wash trading (Gan et al., 2022). To
the best of our knowledge, FlashSyn is the first tool that can detect flash
loan attacks before they happen and show successes in real-world DeFi
protocols under auditing.

##  9\. Conclusion

We have proposed an automated synthesis framework based on numerical
approximation to generate the flash loan attack vectors on DeFi protocols. Our
results of FlashSyn show that the proposed framework is practical and FlashSyn
can automatically synthesize attack vectors for real world attacks. Our
results also highlight the effectiveness of the synthesis-via-approximation
approach. The approach helps FlashSyn to overcome the challenges posed by
complicated functions in DeFi protocols and our results demonstrate that using
approximations of these functions is sufficient to drive the synthesis
process. FlashSyn has been adopted by a top smart contract auditing company to
detect flash loan vulnerabilities. The paper also points out a new promising
direction for solving trace synthesis problems when facing complicated
functions.

##  10\. Data Availability

The benchmarks, source code and experimental data of our artifacts are
publicly accessible on (Chen et al., 2024a) and have been archived on (Chen et
al., 2024b).

## References

  * (1)
  * 1inch Network (2023) The 1inch Network. 2023.  The 1inch SWAP.  https://app.1inch.io/.  Accessed: 2023-03-25.
  * BlockSec (2023) BlockSec. 2023.  Phalcon: Powerful Transaction Explorer Designed for DeFi community.  https://phalcon.xyz/ Accessed: 2023-03-27.
  * Brent et al. (2020) Lexi Brent, Neville Grech, Sifis Lagouvardos, Bernhard Scholz, and Yannis Smaragdakis. 2020.  Ethainter: a smart contract security analyzer for composite vulnerabilities. In _Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation_. 454–469.
  * BscScan (2021a) BscScan. 2021a.  ApeRocket Attack Transaction.  https://bscscan.com/tx/0x701a308fba23f9b328d2cdb6c7b245f6c3063a510e0d5bc21d2477c9084f93e0.
  * BscScan (2021b) BscScan. 2021b.  AutoShark Attack Transaction.  https://bscscan.com/tx/0xfbe65ad3eed6b28d59bf6043debf1166d3420d214020ef54f12d2e0583a66f13.
  * BscScan (2021c) BscScan. 2021c.  bEarnFi Attack Transaction.  https://bscscan.com/tx/0x603b2bbe2a7d0877b22531735ff686a7caad866f6c0435c37b7b49e4bfd9a36c.
  * BscScan (2021d) BscScan. 2021d.  ElevenFi Attack Transaction.  https://bscscan.com/tx/0x16c87d9c4eb3bc6c4e5fbba789f72e8bbfc81b3403089294a81f31b91088fc2f.
  * BscScan (2022a) BscScan. 2022a.  Novo Attack Transaction.  https://bscscan.com/tx/0xc346adf14e5082e6df5aeae650f3d7f606d7e08247c2b856510766b4dfcdc57f.
  * BscScan (2022b) BscScan. 2022b.  WDoge Attack Transaction.  https://bscscan.com/tx/0x4f2005e3815c15d1a9abd8588dd1464769a00414a6b7adcbfd75a5331d378e1d.
  * BscScan (2023) BscScan. 2023.  The BNB Smart Chain Explorer.  https://bscscan.com/
  * Buitinck et al. (2013) Lars Buitinck, Gilles Louppe, Mathieu Blondel, Fabian Pedregosa, Andreas Mueller, Olivier Grisel, Vlad Niculae, Peter Prettenhofer, Alexandre Gramfort, Jaques Grobler, Robert Layton, Jake VanderPlas, Arnaud Joly, Brian Holt, and Gaël Varoquaux. 2013.  API design for machine learning software: experiences from the scikit-learn project. In _ECML PKDD Workshop: Languages for Data Mining and Machine Learning_. 108–122.
  * Buterin (2014) Vitalik Buterin. 2014.  Ethereum: A next-generation smart contract and decentralized application platform.  https://ethereum.org/en/whitepaper/.
  * Cao et al. (2021) Yixin Cao, Chuanwei Zou, and Xianfeng Cheng. 2021.  Flashot: a snapshot of flash loan attack on DeFi ecosystem.  _arXiv preprint arXiv:2102.00626_ (2021).
  * Chen et al. (2024a) Zhiyang Chen, Sidi Mohamed Beillahi, and Fan Long. 2024a.  _GitHub Artifact for FlashSyn: Flash Loan Attack Synthesis via Counter Example Driven Approximation_.  https://github.com/FlashSyn-Artifact/FlashSyn-Artifact-ICSE24
  * Chen et al. (2024b) Zhiyang Chen, Sidi Mohamed Beillahi, and Fan Long. 2024b.  _Zenodo Artifact for FlashSyn: Flash Loan Attack Synthesis via Counter Example Driven Approximation_.  https://zenodo.org/records/10458602
  * Choi et al. (2021) Jaeseung Choi, Doyeon Kim, Soomin Kim, Gustavo Grieco, Alex Groce, and Sang Kil Cha. 2021.  SMARTIAN: Enhancing smart contract fuzzing with static and dynamic data-flow analyses. In _2021 36th IEEE/ACM International Conference on Automated Software Engineering (ASE)_. IEEE, 227–239.
  * Clarke et al. (2000) Edmund Clarke, Orna Grumberg, Somesh Jha, Yuan Lu, and Helmut Veith. 2000.  Counterexample-guided abstraction refinement. In _International Conference on Computer Aided Verification_. Springer, 154–169.
  * ConsenSys (2022) ConsenSys. 2022.  Mythril.  https://github.com/ConsenSys/mythril.  Accessed: 2022-06-06.
  * Damn Vulnerable DeFi (2023a) Damn Vulnerable DeFi. 2023a.  https://www.damnvulnerabledefi.xyz/.  Accessed: 2023-01-31.
  * Damn Vulnerable DeFi (2023b) Damn Vulnerable DeFi. 2023b.  Challenge #8 - Puppet.  https://www.damnvulnerabledefi.xyz/challenges/8.html.  Accessed: 2023-01-31.
  * Damn Vulnerable DeFi (2023c) Damn Vulnerable DeFi. 2023c.  Challenge #9 - Puppet v2.  https://www.damnvulnerabledefi.xyz/challenges/9.html.  Accessed: 2023-01-31.
  * DefiLlama (2023) DefiLlama. 2023.  DefiLlama.  https://defillama.com/.  Accessed: 2023-04-01.
  * Egorov (2019) Michael Egorov. 2019.  StableSwap-efficient mechanism for Stablecoin liquidity.  _Retrieved Feb_ 24 (2019), 2021.
  * Endres et al. (2018) Stefan C Endres, Carl Sandrock, and Walter W Focke. 2018.  A simplicial homology algorithm for Lipschitz optimisation.  _Journal of Global Optimization_ 72, 2 (2018), 181–217.
  * Etherscan (2020a) Etherscan. 2020a.  bZx1 Attack Transaction.  https://etherscan.io/tx/0xb5c8bd9430b6cc87a0e2fe110ece6bf527fa4f170a4bc8cd032f768fc5219838.
  * Etherscan (2020b) Etherscan. 2020b.  Cheesebank Attack Transaction.  https://etherscan.io/tx/0x600a869aa3a259158310a233b815ff67ca41eab8961a49918c2031297a02f1cc.
  * Etherscan (2020c) Etherscan. 2020c.  Eminence Attack Transaction.  https://etherscan.io/tx/0x3503253131644dd9f52802d071de74e456570374d586ddd640159cf6fb9b8ad8.
  * Etherscan (2020d) Etherscan. 2020d.  Harvest_USDC Attack Transaction.  https://etherscan.io/tx/0x35f8d2f572fceaac9288e5d462117850ef2694786992a8c3f6d02612277b0877.
  * Etherscan (2020e) Etherscan. 2020e.  Harvest_USDT Attack Transaction.  https://etherscan.io/tx/0x0fc6d2ca064fc841bc9b1c1fad1fbb97bcea5c9a1b2b66ef837f1227e06519a6.
  * Etherscan (2020f) Etherscan. 2020f.  inverseFi Attack Transaction.  https://etherscan.io/tx/0x958236266991bc3fe3b77feaacea120f172c0708ad01c7a715b255f218f9313c.
  * Etherscan (2020g) Etherscan. 2020g.  ValueDeFi Attack Transaction.  https://etherscan.io/tx/0x46a03488247425f845e444b9c10b52ba3c14927c687d38287c0faddc7471150a.
  * Etherscan (2020h) Etherscan. 2020h.  Warp Attack Transaction.  https://etherscan.io/tx/0x8bb8dc5c7c830bac85fa48acad2505e9300a91c3ff239c9517d0cae33b595090.
  * Etherscan (2021) Etherscan. 2021.  Yearn Attack Transaction.  https://etherscan.io/tx/0xf6022012b73770e7e2177129e648980a82aab555f9ac88b8a9cda3ec44b30779.
  * Etherscan (2023) Etherscan. 2023.  The Ethereum Blockchain Explorer.  https://etherscan.io/
  * Feist et al. (2019) Josselin Feist, Gustavo Grieco, and Alex Groce. 2019.  Slither: a static analysis framework for smart contracts. In _2019 IEEE/ACM 2nd International Workshop on Emerging Trends in Software Engineering for Blockchain (WETSEB)_. IEEE, 8–15.
  * Feng et al. (2019) Yu Feng, Emina Torlak, and Rastislav Bodik. 2019.  Precise attack synthesis for smart contracts.  _arXiv preprint arXiv:1902.06067_ (2019).
  * Finance (2022) Curve Finance. 2022.  Curve Finance.  https://curve.fi/.
  * Foundation (2023a) Ethereum Foundation. 2023a.  Solidity Programming Language.  https://docs.soliditylang.org/en/v0.8.14/.  Accessed: 2023-03-24.
  * Foundation (2023b) Ethereum Foundation. 2023b.  Vyper Programming Language.  https://vyper.readthedocs.io/en/stable/.  Accessed: 2023-02-24.
  * Foundry Contributors (2023) Foundry Contributors. 2023.  Foundry.  https://github.com/foundry-rs/foundry/.  Accessed: 2023-01-31.
  * Frank et al. (2020) Joel Frank, Cornelius Aschermann, and Thorsten Holz. 2020.  $\\{$ETHBMC$\\}$: A Bounded Model Checker for Smart Contracts. In _29th USENIX Security Symposium (USENIX Security 20)_. 2757–2774.
  * FtmScan (2022) FtmScan. 2022.  OneRing Attack Transaction.  https://ftmscan.com/tx/0xca8dd33850e29cf138c8382e17a19e77d7331b57c7a8451648788bbb26a70145.
  * FTMScan (2023) FTMScan. 2023.  The Fantom Blockchain Explorer.  https://ftmscan.com/
  * Gan et al. (2022) Rundong Gan, Le Wang, Xiangyu Ruan, and Xiaodong Lin. 2022.  Understanding Flash-Loan-based Wash Trading. In _Proceedings of the 4th ACM Conference on Advances in Financial Technologies_. 74–88.
  * Ghaleb et al. (2023) Asem Ghaleb, Julia Rubin, and Karthik Pattabiraman. 2023.  AChecker: Statically Detecting Smart Contract Access Control Vulnerabilities.  _Proc. ACM ICSE_ (2023).
  * Grieco et al. (2020) Gustavo Grieco, Will Song, Artur Cygan, Josselin Feist, and Alex Groce. 2020.  Echidna: effective, usable, and fast fuzzing for smart contracts. In _Proceedings of the 29th ACM SIGSOFT International Symposium on Software Testing and Analysis_. 557–560.
  * Jiang et al. (2018) Bo Jiang, Ye Liu, and Wing Kwong Chan. 2018.  Contractfuzzer: Fuzzing smart contracts for vulnerability detection. In _2018 33rd IEEE/ACM International Conference on Automated Software Engineering (ASE)_. IEEE, 259–269.
  * Joe and Kuo (2008) Stephen Joe and Frances Y Kuo. 2008.  Constructing Sobol sequences with better two-dimensional projections.  _SIAM Journal on Scientific Computing_ 30, 5 (2008), 2635–2654.
  * Kalra et al. (2018) Sukrit Kalra, Seep Goel, Mohan Dhawan, and Subodh Sharma. 2018.  Zeus: analyzing safety of smart contracts.. In _Ndss_. 1–12.
  * King (1976) James C King. 1976.  Symbolic execution and program testing.  _Commun. ACM_ 19, 7 (1976), 385–394.
  * Liu et al. (2022) Ye Liu, Yi Li, Shang-Wei Lin, and Cyrille Artho. 2022.  Finding permission bugs in smart contracts with role mining. In _Proceedings of the 31st ACM SIGSOFT International Symposium on Software Testing and Analysis_. 716–727.
  * Liu et al. (2020) Ye Liu, Yi Li, Shang-Wei Lin, and Rong Zhao. 2020.  Towards automated verification of smart contract fairness. In _Proceedings of the 28th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering_. 666–677.
  * Luu et al. (2016) Loi Luu, Duc-Hiep Chu, Hrishi Olickel, Prateek Saxena, and Aquinas Hobor. 2016.  Making smart contracts smarter. In _Proceedings of the 2016 ACM SIGSAC conference on computer and communications security_. 254–269.
  * Martin Derka (2023) Quantstamp Martin Derka. 2023.  Automated Flash Loan Attack Synthesis.  https://www.youtube.com/watch?v=e6VR7Rv-jiY&t=100s&ab_channel=DeFiSecuritySummit.
  * McKay (2022) Jack McKay. 2022.  DeFi-ing Cyber Attacks.  (2022).
  * Montgomery et al. (2021) Douglas C Montgomery, Elizabeth A Peck, and G Geoffrey Vining. 2021.  _Introduction to linear regression analysis_.  John Wiley & Sons.
  * Mossberg et al. (2019) Mark Mossberg, Felipe Manzano, Eric Hennenfent, Alex Groce, Gustavo Grieco, Josselin Feist, Trent Brunson, and Artem Dinaburg. 2019.  Manticore: A user-friendly symbolic execution framework for binaries and smart contracts. In _2019 34th IEEE/ACM International Conference on Automated Software Engineering (ASE)_. IEEE, 1186–1189.
  * Nguyen et al. (2020) Tai D Nguyen, Long H Pham, Jun Sun, Yun Lin, and Quang Tran Minh. 2020.  sfuzz: An efficient adaptive fuzzer for solidity smart contracts. In _Proceedings of the ACM/IEEE 42nd International Conference on Software Engineering_. 778–788.
  * Pedregosa et al. (2011) F. Pedregosa, G. Varoquaux, A. Gramfort, V. Michel, B. Thirion, O. Grisel, M. Blondel, P. Prettenhofer, R. Weiss, V. Dubourg, J. Vanderplas, A. Passos, D. Cournapeau, M. Brucher, M. Perrot, and E. Duchesnay. 2011.  Scikit-learn: Machine Learning in Python.  _Journal of Machine Learning Research_ 12 (2011), 2825–2830.
  * Qin et al. (2021) Kaihua Qin, Liyi Zhou, Benjamin Livshits, and Arthur Gervais. 2021.  Attacking the defi ecosystem with flash loans for fun and profit. In _International Conference on Financial Cryptography and Data Security_. Springer, 3–32.
  * Quantstamp (2023a) Quantstamp. 2023a.  Economic Exploit Analysis.  https://quantstamp.com/economic-exploits.
  * Quantstamp (2023b) Quantstamp. 2023b.  Web3 Security Firm Quantstamp Launches Novel Economic Exploit Analysis Service to Combat Flash Loan Attacks.  https://www.newswire.ca/news-releases/web3-security-firm-quantstamp-launches-novel-economic-exploit-analysis-service-to-combat-flash-loan-attacks-833815039.html.
  * Ramezany et al. (2023) Shahin Ramezany, Rachsuda Setthawong, and Pisal Setthawong. 2023.  Midnight: An Efficient Event-driven EVM Transaction Security Monitoring Approach For Flash Loan Detection. In _2023 20th International Joint Conference on Computer Science and Software Engineering (JCSSE)_. IEEE, 237–241.
  * Rekt (2020) Rekt. 2020.  WARP FINANCE - REKT.  https://rekt.news/warp-finance-rekt/.
  * Rukundo and Cao (2012) Olivier Rukundo and Hanqiang Cao. 2012.  Nearest neighbor value interpolation.  _arXiv preprint arXiv:1211.1768_ (2012).
  * Rush (2023) Thomas Jay Rush. 2023.  TrueBlocks.  https://trueblocks.io/.
  * Shou et al. (2023) Chaofan Shou, Shangyin Tan, and Koushik Sen. 2023.  ItyFuzz: Snapshot-Based Fuzzer for Smart Contract. In _Proceedings of the 32nd ACM SIGSOFT International Symposium on Software Testing and Analysis_. 322–333.
  * SlowMist (2021) SlowMist. 2021.  Analysis of Warp Finance Hacked Incident.  https://slowmist.medium.com/analysis-of-warp-finance-hacked-incident-cb12a1af74cc.
  * SlowMist (2023) SlowMist. 2023.  The 10 most common attacks.  https://hacked.slowmist.io/en/statistics/?c=all&d=all.  Accessed: 2023-02-01.
  * Swap (2022) Pancake Swap. 2022.  Pancake Swap.  https://pancakeswap.finance/.
  * Tikhomirov et al. (2018) Sergei Tikhomirov, Ekaterina Voskresenskaya, Ivan Ivanitskiy, Ramil Takhaviev, Evgeny Marchenko, and Yaroslav Alexandrov. 2018.  Smartcheck: Static analysis of ethereum smart contracts. In _Proceedings of the 1st International Workshop on Emerging Trends in Software Engineering for Blockchain_. 9–16.
  * Tsankov et al. (2018) Petar Tsankov, Andrei Dan, Dana Drachsler-Cohen, Arthur Gervais, Florian Buenzli, and Martin Vechev. 2018.  Securify: Practical security analysis of smart contracts. In _Proceedings of the 2018 ACM SIGSAC Conference on Computer and Communications Security_. 67–82.
  * Uniswap Labs (2023) Uniswap Labs. 2023.  Uniswap Protocol.  https://uniswap.org/.  Accessed: 2023-11-08.
  * Virtanen et al. (2020) Pauli Virtanen, Ralf Gommers, Travis E. Oliphant, Matt Haberland, Tyler Reddy, David Cournapeau, Evgeni Burovski, Pearu Peterson, Warren Weckesser, Jonathan Bright, Stéfan J. van der Walt, Matthew Brett, Joshua Wilson, K. Jarrod Millman, Nikolay Mayorov, Andrew R. J. Nelson, Eric Jones, Robert Kern, Eric Larson, C J Carey, İlhan Polat, Yu Feng, Eric W. Moore, Jake VanderPlas, Denis Laxalde, Josef Perktold, Robert Cimrman, Ian Henriksen, E. A. Quintero, Charles R. Harris, Anne M. Archibald, Antônio H. Ribeiro, Fabian Pedregosa, Paul van Mulbregt, and SciPy 1.0 Contributors. 2020.  SciPy 1.0: Fundamental Algorithms for Scientific Computing in Python.  _Nature Methods_ 17 (2020), 261–272.  https://doi.org/10.1038/s41592-019-0686-2
  * Wales (2015) DJ Wales. 2015.  Perspective: Insight into reaction coordinates and dynamics from the potential energy landscape.  _The Journal of chemical physics_ 142, 13 (2015), 130901.
  * Wang et al. (2022) Bin Wang, Xiaohan Yuan, Li Duan, Hongliang Ma, Chunhua Su, and Wei Wang. 2022.  DeFiScanner: Spotting DeFi Attacks Exploiting Logic Vulnerabilities on Blockchain.  _IEEE Transactions on Computational Social Systems_ (2022).
  * Wang et al. (2021) Dabao Wang, Siwei Wu, Ziling Lin, Lei Wu, Xingliang Yuan, Yajin Zhou, Haoyu Wang, and Kui Ren. 2021.  Towards a first step to understand flash loan and its applications in defi ecosystem. In _Proceedings of the Ninth International Workshop on Security in Blockchain and Cloud Computing_. 23–28.
  * Wang et al. (2020) Haijun Wang, Ye Liu, Yi Li, Shang-Wei Lin, Cyrille Artho, Lei Ma, and Yang Liu. 2020.  Oracle-supported dynamic exploit generation for smart contracts.  _IEEE Transactions on Dependable and Secure Computing_ (2020).
  * Werapun et al. (2022) Warodom Werapun, Tanakorn Karode, Tanwa Arpornthip, Jakapan Suaboot, Esther Sangiamkul, and Pawita Boonrat. 2022.  The Flash Loan Attack Analysis (FAA) Framework—A Case Study of the Warp Finance Exploitation. In _Informatics_ , Vol. 10. MDPI, 3.
  * Wood (2012) Gavin Wood. 2012.  Ethereum: A Secure Decentralised Generalised Transaction Ledger.  https://ethereum.github.io/yellowpaper/paper.pdf.
  * Wüst and Gervais (2018) Karl Wüst and Arthur Gervais. 2018.  Do you need a blockchain?. In _2018 Crypto Valley Conference on Blockchain Technology (CVCBT)_. IEEE, 45–54.
  * Xia et al. (2021) Pengcheng Xia, Haoyu Wang, Bingyu Gao, Weihang Su, Zhou Yu, Xiapu Luo, Chao Zhang, Xusheng Xiao, and Guoai Xu. 2021.  Trade or Trick? Detecting and Characterizing Scam Tokens on Uniswap Decentralized Exchange.  _Proceedings of the ACM on Measurement and Analysis of Computing Systems_ 5, 3 (2021), 1–26.
  * Xia et al. (2023) Qing Xia, Zhirong Huang, Wensheng Dou, Yafeng Zhang, Fengjun Zhang, Geng Liang, and Chun Zuo. 2023.  Detecting Flash Loan Based Attacks in Ethereum. In _2023 IEEE 43rd International Conference on Distributed Computing Systems (ICDCS)_. IEEE, 154–165.
  * Xu et al. (2021) Jiahua Xu, Krzysztof Paruch, Simon Cousaert, and Yebo Feng. 2021.  Sok: Decentralized exchanges (dex) with automated market maker (AMM) protocols.  _arXiv preprint arXiv:2103.12732_ (2021).
  * Zhang et al. (2023) Zhuo Zhang, Brian Zhang, Wen Xu, and Zhiqiang Lin. 2023.  Demystifying Exploitable Bugs in Smart Contracts. ICSE.
  * Zheng et al. (2022) Peilin Zheng, Zibin Zheng, and Xiapu Luo. 2022.  Park: accelerating smart contract vulnerability detection via parallel-fork symbolic execution. In _Proceedings of the 31st ACM SIGSOFT International Symposium on Software Testing and Analysis_. 740–751.

##  Appendix A Functions of Curve.Fi Y Pool Contract

To extend the discussion about the complexity of _(_ Curve.Fi Y Pool) contract
in Section 3 , we include another three functions
_exchange_underlying_ , __exchange_ , and _get_y_ in Figure 4, Figure 5, and
Figure 6 respectively.

_exchange_underlying_ is the public function usually called by users to
exchange _dx_ amount of underlying asset _i_ to _j_ , and _min_dy_ represents
the minimum quantity expected to receive from the exchange. Once
_exchange_underlying_ is called, it will internally execute a private function
__exchange_ , which will call another private _get_y_. _get_y_ first calls
_get_D_ to calculate a constant $D$ iteratively. Then it calculates an updated
value of $y$ iteratively based on $D$ and other constants. This iterative
Calculation impedes symbolic execution since it results in too complicated
non-linear constraints.

⬇

1function exchange_underlying( int128 i, int128 j,

2 uint dx, uint min_dy)

3{

4 uint[] memory rates = _stored_rates();

5 uint N_COINS = rates.length;

6 uint[] memory precisions = PRECISION_MUL;

7 uint rate_i = rates[i] / precisions[i];

8 uint rate_j = rates[j] / precisions[j];

9 uint dx_ = (dx * PRECISION) / rate_i;

10 // key step: call get_y and then call get_D

11 uint dy_ = _exchange(i, j, dx_, rates);

12 uint dy = (dy_ * rate_j) / PRECISION;

13 assert(dy >= min_dy, "...");

14 bool[] memory tethered = TETHERED;

15 uint ok = 0;

16 if (tethered[i])

17 USDT(u_coins[i]).transferFrom(

18 msg.sender, address(this), dx);

19 else

20 assert_modifiable(

21 ERC20(u_coins[i]).transferFrom(

22 msg.sender, address(this), dx)

23 );

24 ERC20(u_coins[i]).approve(coins[i], dx);

25 yERC20(coins[i]).deposit(dx);

26 yERC20(coins[j]).withdraw(dy_);

27 dy=ERC20(u_coins[j]).balanceOf(address(this));

28 assert(dy >= min_dy, "...");

29 if (tethered[j])

30 USDT(u_coins[j]).transfer(msg.sender, dy);

31 else assert_modifiable(ERC20(u_coins[j])

32 .transfer(msg.sender, dy));

33 log.TokenExchangeUnderlying(msg.sender, i, dx, j, dy);

34}

Figure 4. Source code of exchange_underlying(). Original code is in Vyper,
rewritten in Solidity.

⬇

1function _exchange(int128 i, int128 j,

2 uint dx, uint[] calldata rates)

3{

4 uint[N_COINS] xp = _xp(rates);

5 uint x = xp[i] + dx * rates[i] / PRECISION;

6 uint y = get_y(i, j, x, xp);

7 uint dy = xp[j] - y;

8 uint dy_fee = dy * self.fee / FEE_DENOMINATOR;

9 uint dy_admin_fee = dy_fee * self.admin_fee / FEE_DENOMINATOR;

10 balances[i] = x * PRECISION / rates[i];

11 balances[j] = (y + (dy_fee - dy_admin_fee)) * PRECISION / rates[j]

12 uint _dy = (dy - dy_fee) * PRECISION / rates[j]

13 return _dy;

14}

Figure 5. Source code of exchange(). Original code is in Vyper, rewritten in
Solidity.

⬇

1function get_y( int128 i, int128 j,

2 uint x, uint[] calldata _xp) returns (uint)

3{

4 uint N_COINS = _xp.length;

5 assert(

6 i != j && i >= 0 && j >= 0 &&

7 uint(i) < N_COINS && uint(j) < N_COINS

8 );

9 uint D = get_D(_xp);

10 uint c = D;

11 uint S_ = 0;

12 uint Ann = A * N_COINS; // A is a constant

13 uint _x = 0;

14 for (uint _i = 0; _i < N_COINS; _i = _i + 1) {

15 if (_i == uint(i)) {

16 _x = x;

17 } else if (_i != uint(j)) {

18 _x = _xp[_i];

19 } else continue;

20 S_ += _x;

21 c = (c * D) / (_x * N_COINS);

22 }

23 c = (c * D) / (Ann * N_COINS);

24 uint b = S_ + D / Ann; // - D

25 uint y_prev = 0;

26 uint y = D;

27 for (uint _i = 0; _i < 255; _i = _i + 1) {

28 y_prev = y;

29 y = (y * y + c) / (2 * y + b - D);

30 // Equality with the precision of 1

31 if (y > y_prev) {

32 if (y - y_prev <= 1) break;

33 } else {

34 if (y_prev - y <= 1) break;

35 }

36 }

37 return y;

38}

Figure 6. Source code of get_y(). Original code is in Vyper, rewritten in
Solidity.

##  Appendix B Warp Finance Case Study

On Dec. 18, 2020, Warp Finance suffered a flash loan attack which leads to
about $7.8 million loss, according to Rekt (Rekt, 2020). The first attack
happened in the transaction (Etherscan, 2020h). A detailed postmortem analysis
(SlowMist, 2021) is written by SlowMist on Medium.

Attack Root Cause: The core of Warp attack is a design flaw of calculating the
price of LP tokens. The price of LP token is calculated as (amount(WETH) in
the pool * WETH price + amount(DAI) in the pool * DAI price) / total supply of
LP. Even though the developer uses Uniswap official price oracle to
(correctly) calculate the prices of WETH and DAI, they failed to realize the
amounts of WETH and DAI can also be manipulated by flash loans. The exploiter
took advantage of this point, pumped up the LP price, and falsely borrow
excessive USDC and DAI from the pool.

Real Attack Vector in History:
Action 1: _mint(2900030e18)_
Action 2: _swap(WETH, DAI, 341217e18)_
Action 3: _provideCollateral(94349e18)_
Action 4: _borrowSC(USDC, 3917983e6)_
Action 5: _borrowSC(DAI, 3862646e18)_
Action 6: _swap(DAI, WETH, 47622329e18)_
Adjusted profit: 1,693,523 USD (DAI + USDC + WETH)

First the exploiter flash loaned WETH and DAI and _mint_ 2900030 DAI and
equivalent WETH to Uniswap’s WETH-DAI pair. Then the attacker swapped a huge
amount of WETH into DAI via the pair to increase the total value of the WETH-
DAI pool, pumping up the unit price of LP token. The exploiter then mortgages
the previously obtained LP Token through the _provideCollateral_ function. As
the unit price of LP Token becomes higher, the LP tokens mortgaged by the
attacker give an abnormally high borrow limit thus the attacker can borrow
more make profit.

Best Attack Vector from FlashSyn:
Action 1: _swap(WETH, DAI, 480069e18)_
Action 2: _mint(322007e18)_
Action 3: _provideCollateral(65937e18)_
Action 4: _borrowSC(USDC, 3862530e6)_
Action 5: _borrowSC(DAI, 3917914e18)_
Action 6: _swap(DAI, WETH, 48862671e18)_
Adjusted profit: 3,368,718 USD (DAI + USDC + WETH)

It is quite surprising that the attack vector from FlashSyn gets a higher
profit compared to the attacker in history. The reason behind this is the
attack vector given by FlashSyn spends more on manipulating Uniswap
pair(Action 1 and Action 6) and spends less on the LP Token mortgaged(Action 2
and Action 3). In this attack, to get the same borrow limit(which can be used
to borrow USDC and DAI in Action 4 and Action 5), it is more economical to
spend on manipulating the Uniswap pair than collateralizing more LP tokens.

##  Appendix C Annotate Action Candidates

As discussed in Section 3, FlashSyn makes use of annotations of prestates and
poststates to drive the approximations. This section provides more details
about the annotation process.

In principle, states refer to read-only functions or contract variables that
contribute to the calculation of token transfers. A prestate refers to the
state before the execution of an action candidate. If two executions share
identical prestates and related inputs, their token transfers must also be the
same. FlashSyn approximates a function which maps (prestates, inputs) to token
transfers. Executing an action will also alter states, which are denoted as
poststates. Poststates of an action will be the prestates of the next action.
FlashSyn also approximates a function which maps (prestates, inputs) to
poststates. By utilizing these two types of approximations, FlashSyn
automatically builds a constrainted optimization problem to search for the
optimal parameters.

Here we use the Vault contract in Figure 7 as an example to illustrate how we
annotate _deposit_ and _withdraw_ functions.

⬇

1function totalSupply() public view returns (uint256) {

2 return _totalSupply;

3}

4

5function underlyingBalanceInVault() view public returns (uint256) {

6 return IERC20(underlying()).balanceOf(address(this));

7}

8

9function underlyingBalanceWithInvestment() view public returns (uint256) {

10 if (address(strategy()) == address(0)) {

11 return underlyingBalanceInVault();

12 }

13 return underlyingBalanceInVault()

14 .add(IStrategy(strategy()).investedUnderlyingBalance());

15}

16

17function deposit(uint256 amount) external {

18 _deposit(amount, msg.sender, msg.sender);

19}

20

21function _deposit(uint amount, address sender, address beneficiary) internal
{

22 uint toMint = totalSupply() == 0 ? amount:

23 amount.mul(totalSupply()).div(underlyingBalanceWithInvestment());

24 _mint(beneficiary, toMint);

25 IERC20(underlying()).safeTransferFrom(sender, address(this), amount);

26 emit Deposit(beneficiary, amount);

27}

28

29function withdraw(uint numberOfShares) external {

30 uint totalSupply = totalSupply();

31 _burn(msg.sender, numberOfShares);

32 uint underlyingAmountToWithdraw = underlyingBalanceWithInvestment()

33 .mul(numberOfShares)

34 .div(totalSupply);

35 if (underlyingAmountToWithdraw > underlyingBalanceInVault()) {

36 if (numberOfShares == totalSupply) {

37 IStrategy(strategy()).withdrawAllToVault();

38 } else {

39 uint missing = underlyingAmountToWithdraw.sub(

40 underlyingBalanceInVault()

41 );

42 IStrategy(strategy()).withdrawToVault(missing);

43 }

44 // recalculate to improve accuracy

45 underlyingAmountToWithdraw = Math.min(

46 underlyingBalanceWithInvestment().mul(numberOfShares).div(

47 totalSupply

48 ),

49 underlyingBalanceInVault()

50 );

51 }

52 IERC20(underlying()).safeTransfer(msg.sender, underlyingAmountToWithdraw);

53 emit Withdraw(msg.sender, underlyingAmountToWithdraw);

54}

Figure 7. The Vault _deposit_ and _withdraw_ methods.

Function _deposit_ moves two tokens. First, it transfers amount USDC from
msg.sender, which is exactly the input argument. No further annotation is
needed for this token transfer. Second, it mints and transfers toMint fUSDC
tokens to the msg.sender. We also find toMint is calculated using the input
amount and two functions totalSupply() and underlyingBalanceWithInvestment().

totalSupply() returns contract variable totalSupply so it is not further
expandable. underlyingBalanceWithInvestment() can be further expanded to
another two read-only functions underlyingBalanceInVault() and
investedUnderlyingBalance(). Both functions are not further expandable because
they are external read-only function calls.

It is also observed that totalSupply(), underlyingBalanceInVault() are changed
after the execution of _deposit_ , while investedUnderlyingBalance() remains
unchanged. Thus, we annotate _deposit_ as follows:

prestates= {totalSupply(), underlyingBalanceInVault(), ,
investedUnderlyingBalance()}, poststates= {totalSupply(),
underlyingBalanceInVault()}, tokenIn = {USDC}, tokenOut = {fUSDC}.

Function _withdraw_ also moves two tokens. First, it transfers and burns
numberOfShares fUSDC tokens from msg.sender. numberOfShares is just the input
argument.

Second, it transfers underlyingAmountToWithdraw USDC tokens to msg.sender.
underlyingAmountToWithdraw is calculated using the input numberOfShares and
two states totalSupply() and underlyingBalanceWithInvestment(). Similarly,
underlyingBalanceWithInvestment() can be further expanded to
underlyingBalanceInVault() and investedUnderlyingBalance().

We also observe that totalSupply(), underlyingBalanceInVault() are changed
after the execution of _withdraw_ , while investedUnderlyingBalance() remains
unchanged. Thus, we annotate _withdraw_ as follows:

prestates= {totalSupply(), underlyingBalanceInVault(), ,
investedUnderlyingBalance()}, poststates= {totalSupply(),
underlyingBalanceInVault()}, tokenIn = {fUSDC}, tokenOut = {USDC}.

In some cases, action A may internally call another function B from a
different contract, which ultimately results in token transfers to/from users.
In such scenarios, we need to annotate function B as the annotations for
action A. Additionally, there may be instances where action C alters the
states of another action D, despite not belonging to the same protocol. For
instance, action D could utilize action C’s contract states as an oracle, and
action C may modify these states. In such situations, it is essential to
include action D’s prestates in action C’s annotations. We would then collect
data points for these state changes and approximate them separately in the
approximation stage.

We believe that the annotating process should not pose significant
difficulties for security analysts. Furthermore, we are optimistic that this
process can be further automated through either static analysis of (open-
source) contracts or dynamic analysis of the EVM level execution traces of
deployed contracts (closed-source), and is left as future work.

##  Appendix D FlashFind: Action Candidates Identification

Flash loan attacks typically focus on victim contracts containing functions
capable of transferring tokens,151515Here, tokens refer to various forms of
DeFi tokens, including stable coins, debt tokens, share tokens, liquidity
tokens, asset tokens, etc. which can be invoked by regular users. The attacker
manipulates the transfer amount under specific conditions. The mathematical
models of victim contracts vary across different protocols.

Specifically, smart contracts with lending, leveraging, or yield-earning
functions are more vulnerable to flash loan attacks. This susceptibility
arises from the involvement of token transfers outside these contract types.
Basic DeFi lego contracts, such as stable coins, Uniswap, and Curve.fi, are
unlikely to be targeted in flash loan attacks due to their fundamental role as
building blocks and infrastructure of nearly all DeFi protocols. These
contracts have undergone exclusive audits and have been in use for several
years.

Given a set of target smart contracts, FlashFind helps users of FlashSyn in
selecting a set of action candidates likely to be involved in an attack
vector.

###  D.1. Selecting Action Candidates from Contract Application Binary
Interfaces (ABIs)

The Application Binary Interface (ABI) serves as an interpreter enabling
communication with the EVM bytecode. For all deployed and verified smart
contracts on the blockchain, their ABIs are made public to facilitate user
interactions by allowing them to call functions and engage with the contracts.
An ABI typically comprises (public or external) function names, argument
names/types, function state mutability, and return types.

During the process of selecting action candidates, certain functions can be
safely ignored for the following reasons:

  * •

Functions with the view or pure mutability can be excluded as they do not
modify the state of contracts.

  * •

Functions that can only be invoked by privileged users, such as
_transferOwnership_ , _changeImplementation_ , and _changeAdmin_ , can also be
disregarded since they are unlikely to be accessed by regular
users161616Previous works (Ghaleb et al., 2023; Liu et al., 2022) have
extensively researched access control vulnerabilities, which are outside the
scope of this work.. This step can also be accomplished by conducting a
lightweight static analysis on the source code of the contracts.

  * •

Token permission management functions/parameters, such as the _approve_
function or parameters like deadline and amountOutMin, are excluded. These
functions/parameters solely control whether a transaction will be reverted or
not and do not affect the functional behaviors of contracts. To simplify the
search process of FlashSyn, these permissions are assumed to be granted
maximally.

###  D.2. Learning Special Parameters from Transaction History

After selecting a set of action candidates from contracts’ ABIs, some non-
integer parameters(eg. bytes, string, address, array, enum) can still be
unknown. FlashFind collects past transactions of the target contracts using
TrueBlocks (Rush, 2023) and Blockchain Explorers((Etherscan, 2023), (BscScan,
2023), (FTMScan, 2023)). Subsequently, FlashFind extracts function level trace
data from these transactions using Phalcon171717Phalcon is a transaction
explorer that provides functional level trace data.(BlockSec, 2023), and
utilizes this data to learn the special parameters from previous function
calls made to the contract.

###  D.3. Local Execution and Intra-dependency Analysis

Following the selection of action candidates and determination of action
parameters, each action candidate is executed in a forked blockchain (foundry
(Foundry Contributors, 2023)) to verify its executability at a given block. An
action candidate may not be executable due to various reasons: (1) the
function is disabled by the owner or admin; (2) internal function calls to
other contracts are disabled by the owners or admins of those contracts; (3)
the function is not valid under current blockchain states. The inexecutability
due to these reasons cannot be identified by static analysis of source code
and can only be determined by executions. All such inexecutable functions are
filtered out.

During this step, we focus solely on ensuring the executability of functions
at the given block, without considering their profitability. FlashFind
automatically collects storage read/write information during the execution of
these functions and infers the Read-After-Write (RAW) dependencies181818This
RAW dependency information is also employed in FlashSyn’s initial data
collection to expand the range of data points. between different action
candidates. An action A has a RAW dependency (or equivalently, is RAW
dependent) on action B if the execution of action A reads the storage written
by action B191919It is important to note that this step excludes any
tx.origin/msg.sender-related storage reads/writes, as such storage accesses do
not alter the state of the protocol and are therefore unlikely to impact the
functional behaviors of actions.. From the RAW dependencies, it is possible to
observe that certain functions behave independently, meaning they do not have
any RAW dependencies on other functions, and other functions do not have any
RAW dependencies on them either. Consequently, these independent functions can
be safely ignored.

After analyzing ABIs, transaction history, and local executions, FlashFind
generates a list of action candidates with only their integer arguments left
undetermined. These action candidates are then input into FlashSyn for further
synthesis.

###  D.4. FlashFind Algorithm

1:procedure FlashFind($\mathsf{contracts}$, $\mathsf{bh}$)

2: $\mathsf{functions}\leftarrow[\ ]$;

3: $\mathsf{traces}\leftarrow[\ ]$;

4: for each $\mathsf{A}\in\mathsf{contracts}$;

5: $\mathsf{functions}[\mathsf{A}]\leftarrow\textsc{AnalyzeABI}(\mathsf{A})$

6:
$\mathsf{transactionHistory}\leftarrow\textsc{CollectTransactions}(\mathsf{A},\mathsf{bh})$;

7:
$\mathsf{functions}[\mathsf{A}].add(\textsc{Filter}(\mathsf{transactionHistory}))$;

8: for each $a\in\mathsf{functions}[\mathsf{A}]$;

9: $\mathsf{storageAccess}[a]\leftarrow\textsc{Execute}(a,\mathsf{bh})$

10: $\mathsf{dependentFunctions}\leftarrow[\ ]$;

11: for each $a\in\mathsf{storageAccess}.\mathsf{keys}$:

12: for each $b\neq a\in\mathsf{storageAccess}.\mathsf{keys}$;

13: if checkDependency($\mathsf{storageAccess}[a]$,
$\mathsf{storageAccess}[b]$)

14: $\mathsf{dependentFunctions}[a].add(b)$

15: return $\mathsf{dependentFunctions}$

Algorithm 3 FlashFind to identify candidate actions. It takes a list of
contract addresses $\mathsf{contract}$, a block height $\mathsf{bh}$, and
outputs a list of candidate actions (functions), along with their RAW
dependencies.

Algorithm 3 describes the overall procedure FlashFind to identify candidate
actions. FlashFind takes as inputs a list of contract addresses
$\mathsf{contracts}$ that are used by a DeFi protocol and a block height
$\mathsf{bh}$. It then produces a list of functions
$\mathsf{dependentFunctions}$ that constitute candidate actions.

The procedure FlashFind first analyzes each contract’s ABIs and identifies a
list of non-privileged202020Privileged functions refer to functions that can
only be called by privileged users, e.g., owners of the contract, or within a
certain range of blocks. Thus, these functions are not likely to be used by an
attacker with an arbitrary address. non-read-only functions with only integer
arguments or no arguments. Then FlashFind inspects the blockchain state and
collects the function level trace data for all historical transactions that
occurred before the block height $\mathsf{bh}$ for every contract listed in
$\mathsf{contracts}$ using the sub-procedures CollectTransactions (line 6).
Using the trace data, we then leverage the sub-procedure Filter to identify
non-integer arguments for other non-priviledged non-read-only functions of
contract $\mathsf{A}$, and these functions, with only their integer parameters
undetermined, are flagged as additional candidate actions (line 7). We then
execute these candidate actions locally to verify their executability via the
sub-procedure Execute, while collecting their storage read/write information
(line 9). For each two functions $a$ and $b$, we check if $a$ is RAW dependent
on $b$ via the subprocedure checkDependency (line 13). If so, we add $b$ to
the list of functions that $a$ depends on (line 14). Finally, FlashFind
returns the list of functions(keys of $\mathsf{dependentFunctions}$), along
with their RAW dependencies (values of $\mathsf{dependentFunctions}$) (line
15).

###  D.5. Evaluation Results

We conducted an evaluation of FlashFind and FlashSyn combined on $14$
historical flash loan attack benchmarks solved by FlashSyn alone. The detailed
results are presented in Table 5 of main text. Notably, FlashFind and FlashSyn
together successfully solved $11$ benchmarks. Surprisingly, for $6$
benchmarks, FlashFind discovered new attack vectors containing new actions
that were not utilized by the original attackers. These new attack vectors
exploit the same vulnerabilities and prove to be profitable as well,
highlighting the effectiveness of FlashFind in identifying action candidates.

However, there were 3 benchmarks where FlashFind failed to identify the
correct set of action candidates. We discuss the reasons behind these failures
below. For ElevenFi, there is a function _addLiquidity_ which requires an
argument amounts of integer array of length 4. For AutoShark, a function
_deposit_ takes an address argument referrer. For CheeseBank, a function
_refresh_ takes an argument symbols which is a array of strings. After
analyzing their past transactions, we find there are too many possible values
for these non-integer arguments. Thus, we cannot learn the special parameters
from transaction history. While experienced security analysts might manually
identify these special parameters and include them in the action candidates,
we view these instances as failures of FlashFind, as our goal is to automate
the process as much as possible.

##  Appendix E Profit Calculation and Flash Loan Payment

As discussed in Section 4 , FlashSyn uses constant token prices to calculate
the profit of an attack vector. A positive profit indicates flash loan
vulnerabilities inside the contracts. We notice two possible concerns
regarding this assumption.

First, the price of a token might be influenced by an attack vector; thus
FlashSyn’s profit calculation might be inaccurate. As a result, there might be
false positives in the results. In fact, hackers typically prefer to keep
their final profit in stable coins or popular blockchain-native tokens such as
Ethereum, Bitcoin, or BNB. This preference arises from the fact that other
derivative tokens associated with victim protocols become worthless after the
hack.

Second, if we require all initial balances of an attacker is from flash loans,
a positive profit then does not necessarily mean the ability to pay back flash
loan, since the final balances could not be strictly larger than the initial
balances. In historical flash loan attacks, the attackers usually choose to
convert some of their profit to what’s being flash loaned, for paying back the
flash loan.

We designed an experiment to validate our results and justify our assumption.
A summary of the experiment is shown in Table 6. For each benchmark, we select
the attack vector with the best profit returned by FlashSyn under all
different settings. We record their final balances under ”Results of FlashSyn”
column. We observe for 8 benchmarks, their final balance can already cover the
initial balance; thus the profit calculation is valid here, since it directly
represents the increase of the attacker’s balances.

Apart from two security challenges(Puppet, PuppetV2), we tried to manually
implement DEX swaps after the attack vectors, to make sure final balances are
strictly larger than initial balances. Practically, we use 1inch (1inch
Network, 2023) and Curve.Finance (Finance, 2022; Egorov, 2019) for Ethereum
benchmarks, and Pancake Swap (Swap, 2022) for Binance benchmarks. Results
after swapping are listed under ”Results after Swapping” column. For $6$
benchmarks, we successfully implement DEX swaps so that their final balances
are strictly larger than initial balances. We observe the profit calculation
does not change a lot after swapping, which represents the attack vectors
found by FlashSyn do yield positive profit and indicate flash loan
vulnerabilities.

Overall, among $16$ historical flash loan attack benchamrks, FlashSyn
synthesized attack vectors with positive profit for $14$ cases. And $13$ of
them are valid even under the consideration of flash loan payment.

Table 6. Summary of Repaying Flash Loan(Legends: “Initial Balance” represents initial token balances at the start of FlashSyn. “Profit” represents adjusted calculated using constant token prices. “Pay Back?” represents whether final token balances are strictly greater than initial balances.) benchmark | Initial Balance | Results of FlashSyn | Profit | Pay Back? | Result after Swapping | Profit | Pay Back?
---|---|---|---|---|---|---|---
bZx1 |  | 112 WBTC
---
4500 ETH
| 59 WBTC
---
9009 ETH
2438 | ✗* | / | / | /
Harvest_USDT |  | 50000000 USDT
---
20000000 USDC
| 52635352 USDT
---
17502461 USDC
137813 | ✗ |  | 50000000 USDT
---
20139106 USDC
139106 | ✓
Harvest_USDC |  | 18308555 USDT
---
50000000 USDC
| 15106415 USDT
---
53312192 USDC
110051 | ✗ |  | 18415434 USDT
---
50000000 USDC
106878 | ✓
Warp |  | 500000 WETH
---
5000000 DAI
| 3917914 USDC
---
493733 WETH
8472025 DAI
3368718 | ✗ |  | 504549 WETH
---
5000000 DAI
2918865 | ✓
ValueDeFi |  | 116000000 DAI
---
100000000 USDT
| 102223937 DAI
---
69829957 USDT
32023919 USDC
20300381 CRV
8378194 | ✗ |  | 116000000 DAI
---
108225064 USDT
8225064 | ✓
Yearn |  | 130000000 DAI
---
134000000 USDC
/ | / | / | / | / | /
Eminence | 15000000 DAI | 1601468 DAI | 1601468 | ✓ | / | / | /
CheeseBank | 21000 ETH |  | 20550 ETH
---
1435304 USDC
710427 USDT
0 DAI
1946291 | ✗ | 25493 ETH | 1991297 | ✓
InverseFi | 27000 WBTC | / | / | / | / | / | /
ElevenFi | 130001 BUSD | 259742 BUSD | 129741 | ✓ | / | / | /
bEarnFi | 7804239 BUSD | 7818022 BUSD | 13783 | ✓ | / | / | /
ApeRocket | 1615000 CAKE |  | 16849 WBNB
---
1276757 CAKE
1333 | ✓ | 1553 WBNB 1615000 CAKE | 1553 | ✓
AutoShark | 100001 WBNB | 101373.63 WBNB | 1372 | ✓ | / | / | /
Novo | 2000 WBNB | 25084 WBNB | 23084 | ✓ | / | / | /
Wdoge | 3000 WBNB | 3078 WBNB | 78 | ✓ | / | / | /
OneRing | 150000000 USDC | 151893085 USDC | 1893085 | ✓ | / | / | /
Puppet |  | 1000 DVT
---
25 ETH
100000 DVT 15 ETH | 89000 | ✗** | / | / | /
PuppetV2 |  | 10000 DVT
---
20 ETH
| 886996 DVT
---
1 ETH
0 WETH
857996 | ✗** | / | / | /

##  Appendix F FlashSyn Results under Different Settings

We applied FlashSyn to $18$ benchmarks, we set a time limit of 1 hour for
initial data collection and another time limit of 2(resp., 3) hours for the
rest of the synthesis procedure. In Section 7, due to page limit, we are only
able to show a summary of our experiment results. Here we show all the results
of our experiment under different settings and for all benchmarks. The profit
of best attack vectors found by FlashSyn under different settings is listed in
Table 7. The synthesis time is listed in Table 8. The initial data collection
time is listed in Table 9.

Note in Section 7, we add synthesis time and initial data collection time
together to get the total time, while Table 7 and Table 8 list them
separately.

Table 7. Profit Summary under Different Settings (N and N+X represent running
FlashSyn with $N$ initial data points for each action, with CEGDC disabled and
enabled respectively. )

| FlashSyn-poly
---|---
benchmark | historyProfit | 200 | 200+X | 500 | 500+X | 1000 | 1000+X | 2000 | 2000+X
bZx1 | 1194 | 2228 | 2443 | 2393 | 2336 | 2372 | 2446 | 2339 | 2392
Harvest_USDT | 338448 | 117137 | 121132 | 136993 | 119232 | 137606 | 120713 | 137813 | 110139
Harvest_USDC | 307416 | 53890 | 73021 | 88922 | 79355 | 90186 | 75377 | 59614 | 59614
Warp | 1693523 | 2778266 | 2969630 | 3368718 | 3368718 | 3290458 | 3290458 | 2773345 | 2773345
ValueDeFi | 8618002 | 5512992 | 5512992 | 6919868 | 8088716 | 4831255 | 8307800 | 2562183 | 8378194
Yearn | 56924 | / | / | / | / | / | / | / | /
Eminence | 1674278 | 1524534 | 1601468 | 1116830 | 1387119 | 1258248 | 1121077 | 585029 | 1507174
CheeseBank | 3270347 | 1675958 | 1675958 | 1675958 | 1675958 | 1675958 | 1675958 | 1675958 | 1946291
InverseFi | 2515606 | / | / | / | / | / | / | / | /
ElevenFi | 129741 | 118025 | 129741 | 129741 | 129741 | 104279 | 105149 | 129741 | 129658
bEarnFi | 18077 | 13783 | 13730 | 13783 | 13756 | 13783 | 13715 | 13783 | 13770
ApeRocket | 1345 | 704 | 704 | / | 1323 | 700 | 700 | 1333 | 1333
AutoShark | 1381 | / | / | 1346 | 1346 | / | / | / | 1372
Novo | 24857 | 14907 | 14907 | 17146 | 17146 | 14835 | 14835 | 14835 | 20210
Wdoge | 78 | 75 | 75 | 75 | 75 | 75 | 75 | 75 | 75
OneRing | 1534752 | 1673425 | 1673425 | 1814877 | 1814877 | 628440 | 628440 | 590506 | 1814882
Puppet | 89000 | 85093 | 85092 | 84095 | 84096 | 89000 | 78200 | 89000 | 89000
PuppetV2 | 953100 | 760543 | 835148 | 326400 | 400830 | 647894 | 857996 | 400965 | 747799
Solved: | 15 | 15 | 15 | 16 | 15 | 15 | 15 | 16
Avg. Normalized. Profit: | 0.793 | 0.829 | 0.846 | 0.922 | 0.762 | 0.786 | 0.717 | 0.945

| FlashSyn-inter
---|---
benchmark | historyProfit | 200 | 200+X | 500 | 500+X | 1000 | 1000+X | 2000 | 2000+X
bZx1 | 1194 | 2018 | 2383 | 2364 | 2364 | 2231 | 2294 | 2301 | 2302
Harvest_USDT | 338448 | 739 | 10759 | 6981 | 13944 | 12043 | 72597 | 1544 | 86798
Harvest_USDC | 307416 | 506 | 14338 | 65670 | 506 | 505 | 2125 | 504 | 110051
Warp | 1693523 | / | / | 596570 | 596570 | / | / | / | /
ValueDeFi | 8618002 | 5415559 | 5415559 | 8348059 | 8348059 | 287732 | 3468019 | 6428341 | 6428341
Yearn | 56924 | / | / | / | / | / | / | / | /
Eminence | 1674278 | / | / | / | / | / | / | / | /
CheeseBank | 3270347 | 659895 | 659895 | 952455 | 1068853 | 1045789 | 1339468 | 1101547 | 1101547
InverseFi | 2515606 | / | / | / | / | / | / | / | /
ElevenFi | 129741 | 57510 | 57510 | 65090 | 86687 | 94456 | 94456 | 85811 | 85811
bEarnFi | 18077 | 11448 | 11448 | 12695 | 11787 | 11576 | 12059 | 11335 | 12329
ApeRocket | 1345 | 1323 | 1323 | 1333 | 1333 | 1135 | 1135 | 1037 | 1037
AutoShark | 1381 | / | / | / | / | / | / | / | /
Novo | 24857 | 14317 | 14317 | 12196 | 13891 | 14065 | 14065 | 23084 | 23084
Wdoge | 78 | 74 | 74 | 78 | 78 | 75 | 75 | 75 | 75
OneRing | 1534752 | 1893085 | 1893085 | 1830059 | 1891589 | 1888510 | 1888510 | 1814877 | 1942188
Puppet | 89000 | 81576 | 82560 | 78818 | 78821 | 81172 | 81172 | 87266 | 87266
PuppetV2 | 953100 | 344943 | 224177 | 459980 | 459980 | 397256 | 397256 | 362540 | 362541
Solved: | 13 | 13 | 14 | 14 | 13 | 13 | 13 | 13
Avg. Normalized. Profit: | 0.539 | 0.555 | 0.630 | 0.634 | 0.535 | 0.580 | 0.594 | 0.641

Table 8. FlashSyn’s Synthesis Time Summary under Different Settings.  Time(s) | FlashSyn-poly | FlashSyn-inter
---|---|---
benchmark | 200 | 200+X | 500 | 500+X | 1000 | 1000+X | 2000 | 2000+X | 200 | 200+X | 500 | 500+X | 1000 | 1000+X | 2000 | 2000+X
bZx1 | 111 | 379 | 115 | 271 | 131 | 454 | 119 | 321 | 159 | 357 | 146 | 327 | 160 | 1634 | 129 | 340
Harvest_USDT | 144 | 636 | 295 | 1176 | 376 | 621 | 320 | 548 | 3981 | 7940 | 5985 | 8380 | 5363 | 7867 | 5616 | 7457
Harvest_USDC | 188 | 554 | 365 | 991 | 350 | 451 | 420 | 561 | 3662 | 7611 | 5845 | 8400 | 5526 | 7845 | 5476 | 8233
Warp | 593 | 1484 | 1319 | 1542 | 1175 | 1428 | 965 | 1069 | / | / | 3320 | 5446 | / | / | / | /
ValueDeFi | 1098 | 1079 | 826 | 5339 | 927 | 3669 | 1145 | 4402 | 10800 | 10800 | 10800 | 10800 | 10800 | 10800 | 10800 | 10800
Yearn | / | / | / | / | / | / | / | / | / | / | / | / | / | / | / | /
Eminence | 468 | 1525 | 461 | 1251 | 1025 | 1209 | 460 | 1094 | / | / | / | / | / | / | / | /
CheeseBank | 4311 | 4080 | 4811 | 5586 | 4648 | 6379 | 5022 | 4249 | 9840 | 10800 | 10800 | 10800 | 10800 | 10800 | 10800 | 10800
InverseFi | / | / | / | / | / | / | / | / | / | / | / | / | / | / | / | /
ElevenFi | 131 | 298 | 156 | 300 | 139 | 1352 | 132 | 288 | 457 | 875 | 463 | 834 | 374 | 2443 | 381 | 777
bEarnFi | 123 | 359 | 118 | 601 | 155 | 731 | 162 | 439 | 352 | 673 | 569 | 950 | 664 | 666 | 517 | 657
ApeRocket | 230 | 409 | / | 610 | 224 | 529 | 416 | 652 | 2057 | 3132 | 2342 | 3724 | 1921 | 3047 | 1920 | 3157
AutoShark | / | / | 4485 | 5762 | / | / | / | 5348 | / | / | / | / | / | / | / | /
Novo | 239 | 420 | 524 | 721 | 330 | 512 | 383 | 630 | 468 | 740 | 796 | 879 | 482 | 848 | 657 | 789
Wdoge | 89 | 203 | 170 | 299 | 145 | 377 | 136 | 237 | 117 | 263 | 226 | 427 | 106 | 385 | 217 | 254
OneRing | 92 | 192 | 183 | 378 | 120 | 309 | 159 | 526 | 110 | 259 | 194 | 485 | 97 | 383 | 169 | 308
Puppet | 36 | 68 | 37 | 65 | 21 | 41 | 32 | 83 | 86 | 197 | 72 | 158 | 89 | 146 | 65 | 118
PuppetV2 | 45 | 133 | 48 | 132 | 35 | 75 | 37 | 103 | 233 | 484 | 196 | 456 | 218 | 437 | 220 | 497
Avg.Time(s) | 527 | 788 | 928 | 1564 | 653 | 1209 | 661 | 1284 | 2486 | 3395 | 2982 | 3719 | 2815 | 3639 | 2844 | 3399
Table 9. FlashSyn’s Initial Data Collection Time Summary under Different Settings.  Initial Data Collection(s) |  |  |  |
---|---|---|---|---
benchmark | 200 | 500 | 1000 | 2000
bZx1 | 49 | 73 | 91 | 101
Harvest_USDT | 37 | 49 | 74 | 122
Harvest_USDC | 62 | 76 | 68 | 116
Warp | 33 | 45 | 60 | 95
ValueDeFi | 80 | 113 | 172 | 289
Yearn | 168 | 189 | 217 | 299
Eminence | 56 | 63 | 73 | 97
CheeseBank | 91 | 94 | 107 | 142
InverseFi | 52 | 62 | 91 | 152
ElevenFi | 69 | 72 | 95 | 121
bEarnFi | 15 | 15 | 23 | 31
ApeRocket | 29 | 36 | 48 | 81
AutoShark | 99 | 97 | 123 | 136
Novo | 36 | 42 | 51 | 72
Wdoge | 10 | 14 | 21 | 35
OneRing | 17 | 22 | 36 | 59
Puppet | 220 | 633 | 686 | 1120
PuppetV2 | 773 | 1482 | 1218 | 2338
Avg. Time: | 105 | 176 | 181 | 300
Table 10. Number of Total Data Points under Different Settings( N(M)
represents the number of data points is N after M rounds of CEGDC. )

| FlashSyn-poly
---|---
benchmark | 200 | 200+X | 500 | 500+X | 1000 | 1000+X | 2000 | 2000+X
bZx1 | 600 | 1788 | 1500 | 2273 | 3000 | 3892 | 5192 | 5849
Harvest_USDT | 800 | 2002 | 2000 | 3704 | 4000 | 5330 | 8000 | 9325
Harvest_USDC | 800 | 3004 | 2000 | 3561 | 4000 | 4695 | 8000 | 8912
Warp | 600 | 604 | 1500 | 1500 | 3000 | 3001 | 6000 | 6000
ValueDeFi | 1200 | 1200 | 3000 | 11138 | 6000 | 13060 | 12000 | 19975
Yearn | / | / | / | / | / | / | / | /
Eminence | 800 | 1525 | 2000 | 2663 | 4000 | 4659 | 8000 | 8780
CheeseBank | 464 | 464 | 942 | 715 | 1534 | 1770 | 2679 | 2937
InverseFi | / | / | / | / | / | / | / | /
ElevenFi | 400 | 460 | 1000 | 1077 | 2000 | 2078 | 4000 | 4070
bEarnFi | 400 | 1444 | 1000 | 2066 | 2000 | 2744 | 4000 | 4854
ApeRocket | 600 | 630 | 1500 | 1739 | 3000 | 3223 | 6000 | 6402
AutoShark | 478 | 478 | 1068 | 1068 | 1645 | 1645 | 2753 | 2753
Novo | 400 | 578 | 1000 | 1110 | 2000 | 2072 | 4000 | 4164
Wdoge | 200 | 201 | 500 | 501 | 1000 | 1001 | 2000 | 2001
OneRing | 400 | 662 | 1000 | 1386 | 2000 | 2188 | 4000 | 4710
Puppet | 600 | 712 | 1500 | 1585 | 3000 | 3111 | 6000 | 6301
PuppetV2 | 600 | 914 | 1396 | 1936 | 2534 | 2664 | 4491 | 4836
Avg. data points: | 584 | 1042 | 1432 | 2376 | 2795 | 3571 | 5445 | 6367

| FlashSyn-inter
---|---
benchmark | 200 | 200+X | 500 | 500+X | 1000 | 1000+X | 2000 | 2000+X
bZx1 | 600 | 1965 | 1500 | 3028 | 3000 | 4413 | 5192 | 6373
Harvest_USDT | 800 | 3367 | 2000 | 4811 | 4000 | 6567 | 8000 | 10289
Harvest_USDC | 800 | 3687 | 2000 | 5240 | 4000 | 7231 | 8000 | 10914
Warp | 600 | 600 | 1500 | 1500 | 3000 | 3000 | 6000 | 6000
ValueDeFi | 1200 | 1200 | 3000 | 5974 | 6000 | 9281 | 12000 | 15758
Yearn | / | / | / | / | / | / | / | /
Eminence | 800 | 923 | 2000 | 2080 | 4000 | 4109 | 8000 | 8104
CheeseBank | 464 | 464 | 942 | 1099 | 1534 | 1635 | 2679 | 2715