FORAY: Towards Effective Attack Synthesis against Deep Logical Vulnerabilities in DeFi Protocols

Hongbo Wen

UC Santa Barbara

Hanzhi Liu

UC Santa Barbara

Jiaxin Song

University of Illinois Urbana-Champaign

Yanju Chen

UC Santa Barbara

Wenbo Guo

UC Santa Barbara

Yu Feng

UC Santa Barbara

for each
S[FOR]ForEach[1] #1

Blockchain adoption has surged with the rise of Decentralized Finance (DeFi) applications. However, the significant value of digital assets managed by DeFi protocols makes them prime targets for attacks. Current smart contract vulnerability detection tools struggle with DeFi protocols due to deep logical bugs arising from complex financial interactions between multiple smart contracts. These tools primarily analyze individual contracts and resort to brute-force methods for DeFi protocols crossing numerous smart contracts, leading to inefficiency.

We introduce , a highly effective attack synthesis framework against deep logical bugs in DeFi protocols.
proposes a novel attack sketch generation and completion framework.
Specifically, instead of treating DeFis as regular programs, we design a domain-specific language (DSL) to lift the low-level smart contracts into their high-level financial operations.
Based on our DSL, we first compile a given DeFi protocol into a token flow graph, our graphical representation of DeFi protocols.
Then, we design an efficient sketch generation method to synthesize attack sketches for a certain attack goal (e.g., price manipulation, arbitrage, etc.).
This algorithm strategically identifies candidate sketches by finding reachable paths in TFG, which is much more efficient than random enumeration.
For each candidate sketch written in our DSL, designs a domain-specific symbolic compilation to compile it into SMT constraints.
Our compilation simplifies the constraints by removing redundant smart contract semantics.
It maintains the usability of symbolic compilation, yet scales to problems orders of magnitude larger.
Finally, the candidates are completed via existing solvers and are transformed into concrete attacks via direct syntax transformation.
Through extensive experiments on real-world security incidents, we demonstrate that significantly outperforms and , the state-of-the-art (SOTA) tools for smart contract vulnerability detection, in both effectiveness and efficiency.
Specifically, out of 34 benchmark DeFi logical bugs happened in the last two years, synthesizes 28 attacks, whereas and only synthesize 13 and 3, respectively.
Furthermore, also finds ten zero-day vulnerabilities in the BNB chain.
Finally, we demonstrate the effectiveness of our key components and 's capability of avoiding false positives.

§ INTRODUCTION

Decentralized Finance (DeFi) applications have driven a surge in blockchain adoption by offering real-world financial services like lending, borrowing, and trading on blockchain networks.
This has brought in a broader user base and increased interest in blockchain technology, with a total funding amount of more than $90 billion locked in DeFi applications as of March 2023 <cit.>.
Nonetheless, the substantial value of digital assets under the management of DeFis renders them an enticing target for potential attacks.
For instance, the recent price manipulation vulnerability <cit.> allows malicious actors to induce DeFi protocols (a set of smart contracts that realize a certain financial model) to execute transactions that are detrimental to user's funds.
Furthermore, attackers can manipulate DeFi protocols to instigate exchanges from lower-valued assets to higher-valued ones or to secure significant loans, often using low-value assets as collateral.
This manipulation is achieved by tampering with the circulation of tokens, thus influencing token prices in the process.
Attacks that exploit logical flaws of financial models behind DeFis (denoted as deep logical bugs) have resulted in a cumulative loss of up to $200 million over the past two years.

Improving the robustness of DeFi protocols is thus a pressing concern and there has been a flurry of research <cit.> in the past few years.
However, the majority of current detection tools primarily concentrate on code vulnerabilities of a single contract, such as re-entrancy, integer overflow, access control, etc.
Therefore, it is unsurprised that these tools cannot be employed effectively to identify DeFi attacks stemming from logic flaws.
The complexity of multiple contracts in DeFi and their interactions dramatically increase the search space that goes beyond the capability of existing analyzers.
To make things even worse, the smart contracts in DeFis are immutable – once they are deployed, fixing their bugs is extremely difficult due to the design of the consensus protocol.

We introduce , a synthesizer for automatically generating exploits against deep logical bugs in DeFi protocols.
introduces an attack sketch generation and completion framework.
It first generates incomplete attack sketches written in our DSL.
Then, it leverages our proposed domain-specific symbolic compilation approach to compile the attack sketches with logical holes into constraints that can be solved by off-the-shelf solvers.
Finally, it fills the holes with a SOTA solver and transforms the complete sketches into concrete attacks through a direct syntax transformation.

The key technical challenges are two-fold.
First, existing tools cannot strategically generate sketches for DeFi beyond random enumeration.
Second, current symbolic compilation tools treat DeFi as a collection of regular smart contracts, disregarding the high-level financial models in DeFi protocols.

To mitigate the first challenge, given a DeFi protocol, first compiles it into a Token Flow Graph (TFG), our proposed high-level semantic representation for DeFi protocols.
Here, nodes represent different tokens (USDC, WETH, USDT, etc.) and edges are labeled with constructs from 's abstract financial language, which provides high-level operators (e.g., lend/borrow/pay/swap) over financial assets.
Now, given a particular attack goal (e.g., price manipulation, arbitrage, etc.) in the form of a logical formula, models the attack sketch generation as a reachability problem in TFG.
Instead of random enumeration, devises an effective sketch generation algorithm that strategically enumerates relevant attack sketches using a type-directed graph reachability algorithm over the TFG.

To tackle the second challenge, employs a domain-specific symbolic compilation strategy, which maintains the usability of symbolic compilation, yet scales to problems orders of magnitude larger.
For each candidate attack sketch, leverages the abstract semantics of our proposed DSL to compile possible completions of the sketch into SMT constraints that can be efficiently solved by off-the-shelf solvers <cit.>.
Here, our domain-specific symbolic compilation can filter out low-level smart contract semantics and thus significantly simplify the constraints.
Because both our sketch generation and sketch completion overapproximate the concrete semantics of DeFis, may generate spurious attacks that fail to achieve the goal.
We mitigate this problem by incorporating a CEGIS (Counter Example-Guided Inductive Synthesis) loop that iteratively adds the root cause of the failed attempt to 's knowledge base, which avoids similar mistakes in future iterations.

We implement and compare it against  <cit.> and  <cit.>, the state-of-the-art tools for analyzing smart contracts and DeFi protocols.
Our experiment shows that our tool is efficient and effective.
On the set of 34 security incidents in the past two years, manages to synthesize attacks for 80% of the benchmarks with an average synthesis time of 249.0 seconds.
On the other hand, Halmos can only solve 10% of the benchmarks with an average running time of 8085.0 seconds, which demonstrates that 's domain-specific symbolic compilation accelerates synthesis several orders of magnitude compared to the general-purpose compilation to an SMT solver.
Furthermore, we also apply to DeFi protocols on the BNB chain <cit.> and uncover ten zero-day vulnerabilities with concrete attacks.
Finally, we verify the effectiveness of sketch generation and completion through an ablation study and demonstrate 's capability in alleviating false positives.
Overall, provides a novel attack synthesis technique against various types of deep logical bugs in DeFis protocols.

In summary, this paper makes the following contributions:

* We propose Abstract Financial Language, a DSL that describes high-level financial operators in DeFis. We also design Token Flow Graph, a semantic representation that summarizes the financial model of a DeFi protocol.

* We propose an effective CEGIS framework for DeFi attack synthesis. In particular, our sketch generation leverages a type-directed graph reachability over a token flow graph and our sketch completion designs a domain-specific symbolic compilation strategy that results in easy-to-solve constraints.

* We implement the proposed ideas in a tool called and demonstrate that it achieves several orders of magnitude speed-up compared to general-purpose symbolic compilation. Furthermore, not only generated 80% security incidents in the past two years (2022-2023) but also detected ten zero-day DeFi vulnerabilities from popular blockchains.

§ BACKGROUND

§.§ Blockchain basis.

Blockchain functions as a decentralized record-keeping platform that chronicles and disseminates transaction data among multiple users.
It is an expand-only chain of interconnected blocks, managed by a consensus mechanism, where each block contains a collection of transactions.

Among various blockchain systems, Ethereum <cit.> is the first blockchain capable of storing, managing, and running Turing-complete scripts, termed smart contracts.
Ethereum operates on a comprehensive state system updated via transaction execution.
The transactions are initiated by and received by users through their accounts.
Ethereum has two principal types of accounts: those owned by users and those governed by smart contracts, each associated with a distinct address.
Besides making transactions, users can also develop customized smart contracts that are programmed to execute transactions autonomously.

Tokens and cryptocurrencies.
Among different types of smart contracts, Tokens are a specific type that represents cryptocurrencies.
Each Token contract must adhere to standardized interfaces like ERC20 <cit.>, ERC721 <cit.>, and ERC1155 <cit.>, which define how users interact with the corresponding token.
For Ethereum, ERC20 is the most widely adopted interface.

To tether the value of cryptocurrencies to fiat currency, stablecoins—like USDT <cit.>, which is implemented as an ERC20 token–have been created.
They are pegged to the dollar reserves held by the issuer, providing a stable reference point for the value of other cryptocurrencies.

§.§ Decentralized Finance (DeFi)

Decentralized Finance (DeFi) refers to a set of financial applications built on blockchain technology.
They aim to recreate traditional financial systems, such as banking and lending, but without the need for intermediaries like banks or brokers.
Instead, each DeFi service is implemented as a protocol that amalgamates various smart contracts.
Users access a DeFi service by engaging with the corresponding protocol through transactions.
According to a recent survey <cit.>, over 200 DeFi applications have been launched on the Ethereum platform.
Here we list three major DeFi applications:

Lending. platforms (such as Aave <cit.>, MakerDAO <cit.>) enable users to obtain on-chain cryptocurrencies as loans by depositing collateral into the system.
The interest rates for borrowing are set by the DeFi protocols while maintaining transparency for users.
As market conditions fluctuate, the collateral's value may fall below or rise above a certain threshold.
When this happens, either the application or other users can liquidate or sell the collateral to gain profits.

Flash loans. (e.g., dYdX <cit.>, Uniswap <cit.>) represent a collateral-free borrowing model.
This enables the borrower to run custom code through a callback function, with the stipulation that the loan must be repaid within the same transaction.
If the borrower fails to return the loaned tokens, the lender will automatically reverse the lending transaction, ensuring that no permanent changes (to storage variables) are made by this transaction.

Decentralized exchanges (DEXs). function as cryptocurrency exchanges that enable users to trade various tokens through direct interaction with smart contracts.
These platforms incentivize users to deposit pairs or multiple tokens into a liquidity pool.
As long as the pool maintains sufficient token volume, users can execute token swaps within it.
The exchange rate for these trades is determined autonomously by the application's built-in pricing algorithm.
Popular DEXs protocols include 1inch <cit.>, PancakeSwap <cit.>.

DeFi vulnerabilities.
At a high level, there are two types of vulnerabilities in DeFi protocols.
The first type refers to vulnerabilities in individual smart contracts, including assertion failures, arbitrary writes, control-flow hijacking, etc (denoted as common vulnerabilities).
These vulnerabilities are similar to traditional software security bugs and are possible to be automatically detected by analyzing the smart contract code.
As discussed in <ref>, existing research works propose a number of tools that utilize static and dynamic program analysis to automatically identify such vulnerabilities.
The second type of vulnerability exploits logical flaws in a DeFi protocol, which we refer to as deep logical bugs in this paper.
As demonstrated in <ref>, these deep logical bugs exploit public functions across multiple smart contracts within the DeFi protocol to maliciously increase an attacker's profits.
Identifying such vulnerabilities is extremely challenging because it requires a deep understanding of the semantics and business logic of the DeFi protocol, as well as the composition of transaction sequences.

As shown in recent studies <cit.>, most existing tools designed for smart contract vulnerabilities fail to detect deep logical bugs.

Illustration of and a concrete exploit against it.
IERC20().transferFrom and IERC20().transfer are standard APIs that enable the withdraw and deposit of tokens for one address.

uniswap.getAmountIn and uniswap.getAmountOut are uniswap APIs that calculate the required amount to swap one type of token for another based on their current reserves.

§ PROBLEM DEFINITION AND EXISTING SOLUTIONS

In this section, we begin by specifying our problem scopes and demonstrating a deep logical bug of a simplified DeFi protocol, , which was hacked in 2022, resulting in the loss of nearly all its stablecoins.
Then, we formally define DeFi attack synthesis and discuss the limitations of existing solutions.

§.§ Problem Scope and Technical Challenges

Threat model.
Our goal is to detect deep logical bugs in a DeFi protocol by synthesizing a sequence of attack transactions that can exploit the DeFi protocol to gain profits maliciously.
We assume an entirely trustless setup where an attacker can access all public information, including but not limited to on-chain blockchain states and the victim contracts' source code.
For contracts with only bytecodes, their source code can be obtained via reserve engineering, which is not our focus.
Additionally, beyond directly interacting with the victim contracts, we assume the attacker can deploy their own contract, which can invoke public transactions of the target victim contracts (either directly or through callbacks).
The attacker's goal is to synthesize a sequence of transactions that exploit the logical flaws in the target DeFi protocol to gain extra profit.
We do not consider the common vulnerabilities.

protocol and an attack.
As shown in <ref>, the protocol is composed of three key smart contracts: a) DeFiLender provides the flashloan function to enable the borrower to get tokens without collateral;
b) Mubank with two functionalities.
The internal function (_mu_bond_quote) manages the sale and price of tokens based on the current reserves of and .
It takes as input the amount of and outputs the corresponding amount of in the same value.
The public function (mu_bond) enables users to withdraw by providing the same value of determined by _mu_bond_quote.
c) Uniswap is a popular protocol, which defines swap pairs for two types of tokens (e.g., and ).
Its swap function enables users to exchange tokens in a swap pair.
These three smart contracts define the DeFi protocol where benign users can borrow, withdraw, and exchange with .

The susceptibility of lies in the pricing mechanism in the Mubank contract (highlighted in <ref>).
Given that the price of is determined by the reveres of and within the swap pair.
A significant fluctuation in the reserve level can result in an unexpectedly high volume of tokens and significantly lower its price.
An attack can leverage the price difference to withdraw the MU bank's stablecoins
A concrete attack is shown in <ref>.
1 Borrow a huge amount of tokens through the flashloan function in DeFiLender.
2 Swap those tokens to a large amount of at the swap pair.
This will dramatically increase the reserve balance ratio of to , devaluing the .
3 Leverage the abnormal reserve balance ratio to swap a tiny amount of for a huge amount of tokens at MuBank.
4 Pay tokens back to the flash loan lender, keeping the majority of acquired at step 2 as the profit.
Through this process, the attacker harvested approximately 57,660 from the MuBank.

Formal definition of attack synthesis for deep logical bugs.
Automatic attack synthesis in DeFi is equivalent to finding a sequence of function calls that exploit deep logical bugs of the DeFi protocol.
This can be formally defined as

A DeFi attack synthesis is a tuple $(L, S_0, \psi)$, where $L$ is the domain-specific language (DSL) for constructing the attack program.
For instance, a list of public functions is provided by the victim DeFi protocol.
$S_0$ is the initial and public blockchain state, and $\psi$ is the attack goal written in a logical formula.
DeFi attack synthesis is equivalent to finding an attack program $P$ written in DSL $L$, such that $P(S_0) \models \psi$ where $P(S_0)$ denotes the resulting state after executing $P$ on $S_0$.

Technical challenges.
It is extremely challenging for the following two reasons.
First, the search space is huge.
In fact, protocol itself contains 26 public functions and the attackers can freely call public functions of other smart contracts (e.g., uniswap.swap).
Even when we constrain the length of the function call sequence, the number of possible sequences is still extremely huge.
Searching a malicious function call sequence in such a huge search space is equivalent to finding a needle in a haystack.
Second, smart contracts and DeFi protocols have complicated semantics.
This imposes extra challenges to automatically represent a DeFi protocol with logical representations, making it hard to reason and synthesize attacks.

§.§ Existing Solutions and Limitations

While attack synthesis is a novel concept in DeFi, it has been explored in traditional software security and program synthesis domains <cit.>.
Without any heavy customization, we can draw inspiration from traditional program synthesis and try to solve the problem with the following two solutions.

Static analysis and symbolic execution based-sketch generation and completion.
Given that synthesizing the entire attack program from scratch is unlikely to scale, existing works in program synthesis usually decompose the synthesis into two phases sketch generation and sketch completion.
Here, an attack sketch refers to a sequence of actions, where each action is a function call to a certain smart contract.
Formally, we define an attack sketch $\tilde{P}$ as a sequence of invocations to constructs in $L$ where some of the constructs contain holes or symbolic variables yet to fill in.

To avoid exploring sketches doomed to fail, existing approaches typically leverage the abstract semantics to only preserve sketches whose abstract semantics are consistent with the attack goal $\psi$, $\tilde{P}(S_0) \Rightarrow \psi$, where $\tilde{P}(S_0)$ corresponds to the program state by abstractly evaluating the sketch $\tilde{P}$ on $S_0$.
Then, the sketch completion step fill in the holes $\hole$ in each feasible sketch $\tilde{P}$ ($P = \tilde{P}[\mu/\hole]$) with language constructs $\mu$ in $L$ using symbolic execution, such that $P(S_0) \models \psi$.

This solution's main challenges are as follows.
First, there are no existing tools in DeFi that can effectively generate feasible attack sketches.
The only way is to randomly select and combine function calls, which is extremely inefficient given the huge search space.
Second, due to the complex semantics of DeFi protocols, the corresponding symbolic constraints of attack goals are intricate and often beyond the reasoning capacity of SOTA SMT solvers.
Specifically, to verify $P(S_0) \models \psi$, existing approaches have to reason about program $P$ by faithfully following the operational semantics of the host language $L$, which contains language features (e.g., gas consumption and memory models in Solidity.) and low-level details irrelevant to the synthesis goal.
As demonstrated in <ref>, it is extremely difficult for Halmos <cit.>, a SOTA symbolic testing tool for Ethereum smart contracts <cit.>, to solve the constraints for common attacks within a feasible time limit.

SOTA fuzzers (e.g., ItyFuzz <cit.> and Smartian <cit.>) in smart contracts support synthesizing sequences of actions that lead to vulnerabilities (violation of DeFi protocol).
Fuzzing is more computationally efficient than symbolic execution-based solutions but it relies more on random generations and mutations.
In addition, due to DeFis' complex semantics, existing fuzzers do not have fitness functions or testing oracles that correspond to specific attack goals and thus cannot provide proper feedback signals of whether the current input is valid, making it even more difficult to find valid attacks through random mutations.

Note that as discussed in <ref>, there are some recent tools for automatically detecting DeFi protocol vulnerabilities.
Most tools rely on summarizing attack patterns from past attack incidents and thus are hindered by the limited scope of these patterns.
They can only detect limited types of vulnerabilities and struggle to identify unseen ones.
Among existing tools, DeFiPoser <cit.> adopts the methodology of automatic sketch generation and completion.
However, its sketches are generated based on limited heuristics, limiting its ability to synthesize anything beyond arbitrage scenarios.

Overall, Due to the lack in effective searching strategies for attack generation and domain-specific attack validation mechanism, existing tools cannot effectively synthesize complicated DeFi attacks.

Overview of with the demonstrated completed sketch for the example in <ref>.
In the sketch, swap$^1$ refers to the mn_bond function. swap$^2$ is achieved through the uniswap.swap function.

§ OVERVIEW OF

To mitigate the limitations of existing solutions, we design and develop , a novel DeFi-specific attack synthesis technique to uncover various deep logical vulnerabilities in DeFi applications.
At a high level, follows the attack sketch generation and completion methodology but includes multiple customized designs to enable more effective sketch search and verification.
As shown in <ref>, we design a domain-specific language to lift the low-level smart contracts into their high-level financial semantics and models (e.g., exchanges, lenders, loans).
Based on our DSL, we first compile DeFi protocols into abstract representations (token flow graph construction), which filter out low-level semantics and constrain the attack sketch space.
We design an efficient sketch generation method based on the graph reachability in the TFG (sketch generation).
Then, we complete a sketch by compiling it into symbolic constraints and replacing the symbolic variables with concrete assignments using an off-the-shelf solver <cit.> (sketch completion).
Finally, we conduct direct syntax transformation to transform the complete sketches into concrete attacks.
Given that the abstraction process may over-simplify blockchain states and concrete smart contract semantics, we conduct an additional validation step to actually run the synthesized attack.
If an attack cannot satisfy the attack goal, our CEGIS loop will add additional constraints corresponding to the root causes to the solver and avoid similar mistakes in future iterations.

Token Flow Graph construction (<ref>).
The insight of this component is to lift the low-level semantics of smart contracts to their high-level financial models.
This process filters out a significant portion of solidity semantics, reducing the synthesis space and simplifying the validation process.
To do so, we first define Abstract Financial Language, a domain-specific language for describing high-level financial operations commonly used by DeFis such as swap, borrow, payback, transfer, etc.
Then given a DeFi protocol, lifts it to a Token Flow Graph (TFG).
As we will show later, this TFG helps develop effective strategies for attack sketch synthesis.
Motivating by prior work <cit.> in type-directed program synthesis, we design each node to represent a certain type of token in DeFi.
To avoid and simplify the complexity due to multi-party communication, we also introduce the $\void$ token, a special node that represents tokens from parties other than the current attacker.
Each edge refers to an operation in our abstract financial language and its source and target nodes represent the tokens that the operation needs to consume and produce, respectively.
<ref> shows the TFG of the protocol.
Here the nodes are , , and $\void$ (i.e., lender of flash loan).
The edges are possible operations invoking the three smart contracts in .
For example, the edge borrow$^1$ from $\void$ to represents one functionality in flashloan function, which enables borrowing a certain amount of tokens from the lender, i.e., DeFiLender.

Sketch generation (<ref>).
Given a TFG of a victim protocol, an attack goal $\psi$ written as constraints in first-order logic, and an initial state $S_0$.
The goal of this step is to synthesize an incomplete program $P$ in abstract financial language such that $P(S_0)\Rightarrow \psi$.
Intuitively, an attack sketch $P$ outlines the key financial steps to achieve the attack goal $\psi$.
Given the huge space, we need to develop an effective search strategy that only enumerates the sketches that are likely to be successful.
To do so, we model the problem of achieving the attack goal as a readability problem in our TFG.
We then design a customized graph readability algorithm to efficiently enumerate candidate sketches that conform with the attack goal.

In our motivating example, the attack goal is $(B^{\mathit{usdce}}_{t_2} - B^{\mathit{usdce}}_{t_1}) \ge 1e6$, stating states the attacker's balance of at the end of the execution ($t_2$) should be greater than his initial balance ($t_1$).
The attack sketch shown in <ref> is a feasible candidate sketch by taking the reachable path of $\void \rightarrow \exampletoken \rightarrow \examplestable \rightarrow \exampletoken \rightarrow \void$ in the TFG.

Sketch completion (<ref>).
After synthesizing feasible attack sketches, our next step is to complete the feasible attack sketches by substituting all symbolic variables with concrete assignments with constants or storage variables.
At a high level, we first design a domain-specific symbolic compilation procedure (motivated by existing solutions <cit.>) that soundly compiles a candidate sketch into a set of constraints that represent the space of all possible concrete attacks.
Then, we conduct the completion by solving the constraints using an off-the-shelf solver <cit.>.
The first challenge in this procedure is to constrain the complexity of symbolic constraints such that they are feasible for existing solvers.
As mentioned above, our abstract financial language and token flow graph are proposed for tackling this challenge.
Representing the victim protocol and attack sketches in our abstract financial language significantly simplifies the constraints.
The second challenge is how to leverage cases that fail to pass the verification.
We tackle this by integrating a CEGIS (Counter Example-Guided Inductive Synthesis) loop into the synthesis process.
This step first conducts direct syntax transformation to map the synthesized attack from our abstract financial language back to solidity code.
It then deploys and executes the attack code using foundry framework <cit.> to test whether the attack goal is achieved in a simulated environment.
It constructs a knowledge base and iteratively adds the root causes of the failed attempts.
We will transform root causes as additional constraints to avoid failed sketches in future attempts.
<ref> demonstrates a complete attack sketch given by a constrained solver, where the symbolic variables are filled with concrete values.

As demonstrated <ref>, also requires inputs $\psi$ and $S_0$ written in first-order logic and a final transformation and validation component (See <ref> for more details of these two parts).

Demonstration of token flow graph construction, graph reachability, and valid attack sketch of in <ref>.
In the TFG, the token nodes (except $\void$) represent tokens owned by the attacker and edges are financial operators (constructs in abstract financial language).

§ TOKEN FLOW GRAPH

In this section, we present a new graph abstraction for modeling flows of tokens within a DeFi environment, which is used to summarize common DeFi behavior, as well as searching for potential program sketches that satisfy a given attack goal.

<prog> ::= <stmt>+

<stmt> ::= <transfer> | <burn> | <mint> | <swap> | <borrow>

<transfer> ::= transfer(token: <token>, from: <addr>, to: <addr>, amt: <expr>)

<burn> ::= burn(token: <token>, from: <addr>, amt: <expr>)

<mint> ::= mint(token: <token>, from: <addr>, amt: <expr>)

<swap> ::= swap(market: <addr>, src: <token>, tgt: <token>, in: <expr>, minout: <expr>, to: <addr>)

<borrow> ::= with borrow(lender: <addr>, to: <addr>, amt: <expr>) {<stmt>+ <payback>}

<payback> ::= payback(lender: <addr>, to: <addr>, amt: <expr>)

<balance> ::= balance(token: <token>, of: <addr>)

<expr> ::= <const> | <op>(<expr>+) | <balance>

\[
\begin{array}{c}
\langle const \rangle \in \textbf{constants} \quad \langle op \rangle \in \textbf{operators} \\ \langle addr \rangle \in \textbf{addresses} \quad \langle token \rangle \in \textbf{tokens}
\end{array}
\]

Syntax for our abstract financial language.

§.§ Abstract Financial Language

As shown in <ref>, abstract financial language is a domain-specific language that is designed to model token flows of common financial operations achieved by DeFi protocols.
A program $\tuple{\it prog}$ written in AFL corresponds to a sequence of statements composed by the following commonly used financial operators:

* $\tuple{\it transfer}$ models a single transfer of a specific amount of a token from one address to another.

* $\tuple{\it burn}$ models the destruction of a certain amount of a token from an address.

* $\tuple{\it mint}$ models the generation of a certain amount of a token from an address.

* $\tuple{\it swap}$ models the exchange of a certain amount of one token to another for an address.

* $\tuple{\it borrow}$ models a temporary transfer behavior of a certain amount of a token from a lender to a borrower's address. A $\tuple{\it payback}$ statement should always be paired at the end to model the return of the borrowed tokens.

Note that $\tuple{\textit{burn}}$ and $\tuple{\textit{mint}}$ functions are implemented to control the total token supply and liquidity, aiming to stabilize its price.
These operations are restricted to specific authorized users.
However, attackers may also leverage these functions via exploitation.

AFL also provides easy syntax and interface for accessing different entities from a DeFi environment, including:

* $\tuple{\it addr}$ for referring to one of all available addresses in a given DeFi environment.

* $\tuple{\it token}$ for referring to one of all available types of tokens in a given DeFi environment.

* $\tuple{\it balance}$ accesses a token's balance in a given address.

Note that AFL can represent both benign and malicious behaviors.
We mainly use it to model attackers in this work.
[AFL attack program]
As shown in <ref>(d), an AFL program may include $\tuple{\it borrow}$ and $\tuple{\it payback}$, interspersed with several $\tuple{\it swap}$ operators in the context.
It represents the following attack behavior: initially, borrowing MU tokens from another party $\epsilon$, then exchanging MU tokens for USDCe tokens, subsequently swapping these back via another exchange contract, and finally, repaying the borrowed MU tokens to the environment $\epsilon$.

§.§ Definition of Token Flow Graph

We propose a Token Flow Graph (TFG) to model changes in amounts of abstract tokens owned by the attacker when interacting with public functions of DeFi protocols.
It helps filter out low-level semantics of smart contracts and guides the synthesis of attack sketches.
To formally define TFG, we first introduce the following domains:

* $\fundom$ is a set of public DeFi functions accessible by the attacker. We assume all non-public functions are resolved by inlining.

* $\afl$ contains AFL operators.

* $\token$ is a set of different tokens appearing in a given DeFi protocol, i.e., nodes in TFG.

* $\edgedom$ is a set of edges in TFG.

* $\constraint$ is a set of behavioral constraints about logical relations between tokens, addresses, and AFL operators.

Given the above domains, we define a token flow graph as a tuple $\tfg(\token, \afl, \edgedom, \constraint)$.
In particular, $\edgedom \subseteq \afl \times \token \times \token$ is a set of edges connecting tokens, where each edge is associated with an AFL operator.
For clarity in presentation, edges are attached with superscripts, denoting different functions that they are inferred from.

Special node $\void$.
Intuitively, the nodes of a token flow graph represent assets of the user currently interacting with the DeFi.
To reflect and simplify the interactions of other participants (e.g., contract owners, other users), each token flow graph has a built-in node $\void \in \token$ that represents tokens of all participants other than the one of interest (i.e., attacker in our problem).
Such tokens are not directly related to the attacker's goal but are necessary for the construction of an attack.

[TFG for an attacker]
<ref>(c) depicts a TFG of the protocol.
For example, an edge labeled with swap$^1$ indicates that the attacker could exchange for through the function mu_bond in <ref>.

§.§ Construction of Token Flow Graph

Given a DeFi protocol, the key to constructing a token flow graph for one specific user is to generate edges among tokens that the user holds or wants to acquire.
employs an edge discovery procedure based on program analysis.
It has two steps, first, we define flow predicate and influence rules for generating flow predicates from concrete programs of a DeFi protocol.
Then, we generate edges from the predicates using edge inference rules.
Each generated edge comes with a semantically equivalent AFL operation with its corresponding constraints.
As illustrated in <ref>, we first identify the flow predicates in the flashloan and mu_bank function, represented as an initial graph.
Then, we apply the edge inference rules to generate the TFG from flow predicates.
For example, the swap$^1$ is deduced from two token flows in mu_bank.
Meanwhile, the borrow$^1$ and payback$^1$ are inferred from the flashloan function.
To avoid the confusion between AFL statements and actual (solidity) program statements, we use “operator” to represent AFL statements $p \in \mathbb{P}$ and “statement” to represent actual program statements $s$.
In what follows, we elaborate on the procedure for flow predicate and edge construction.

Flow predicate.
denoted by

${\sf flow}(u,x,a,b)$,

indicates $x$ amount of token $u$ flows from address $a$ to address $b$.
A flow predicate serves as a basic building block of AFL operators.
<ref> shows the rules for generating flow predicates from actual (solidity) programs.
First, we define a flow state $\mathbb{W}$ that contains a collection of pair $\overrightarrow{s_i:w_i}$ where each pair $s_i:w_i$ represents a statement $s_i$ together with its flow predicate $w_i$.
Note that $\mathbb{W}$ is different from the blockchain state $S$.
For each public function $f \in \fundom$, the func rule processes its statements sequentially by performing a sequence of flow state transitions.
Specifically, given the original state $\mathbb{W}$ and a statement $s$, we model the state transition via

$\mathbb{W} \overset{s}{\rightsquigarrow} \mathbb{W}'$,

which indicates that the analysis of statement $s$ results in a new version $\mathbb{W}'$  by adding the flow predicate corresponding to $s$ to $\mathbb{W}$.
Similar to classical symbolic executions <cit.>, all loops are bounded and unrolled to their corresponding branch statements.
The branch rule then merges updates of $\mathbb{W}$ from both branches.
Other rules that update $\mathbb{W}$ are: flow-from, flow-to, flow-mint and flow-burn, which correspond to public functions in standard interfaces (e.g., ERC20):

* The flow-from rule can be triggered by invocations of ERC20's transferFrom (or other similar) interface, e.g., IERC20(u).transferFrom(a,b,x), which transfers $x$ amount of token $u$ from address $a$ to address $b$.

* The flow-to rule can be triggered by invocations of ERC20's transfer (or other similar) interface, e.g., IERC20(u).transfer(b,x), which transfers $x$ amount of token $u$ from the current caller (i.e., the address pointed by this keyword) to address $b$.

* The flow-mint rule matches invocations of ERC20's mint (or other similar) interface, e.g., IERC20(u).mint(a,x), which produces $x$ amount of $u$ token for address $a$.

* The flow-burn rule matches invocations of ERC20's burn  (or other similar) interface, e.g., IERC20(u).burn(a,x), which destroys $x$ amount of $u$ token from address $a$.

After parsing the programs of a DeFi protocol with rules in <ref>, we get a set of flow predicates that summarize critical financial behaviors within that protocol.
then constructs the token flow graph on top of these predicates.

f ∈
f ≡s_0; ...; s_n
𝕎_0 s_0⇝ 𝕎_1
𝕎_n s_n⇝ 𝕎_n+1

𝕎_0 f⇝ 𝕎_n+1

s ≡if _ then f_0 else f_1
𝕎 f_0⇝ 𝕎_0
𝕎 f_1⇝ 𝕎_1

𝕎 s⇝ 𝕎_0 ∪𝕎_1

s ≡u.transferFrom(a, b, x)
w ≡flow(u, x, a, b)

𝕎 s⇝ 𝕎 ∪{s:w}

s ≡u.transfer(b, x)
a = this
w ≡flow(u, x, a, b)

𝕎 s⇝ 𝕎 ∪{s:w}

s ≡u.mint(a, x)
w ≡flow(u, x, ∙, a)

𝕎 s⇝ 𝕎 ∪{s:w}

s ≡u.burn(a, x)
w ≡flow(u, x, a, ∙)

𝕎 s⇝ 𝕎 ∪{s:w}

Flow predicates inference rules. $\bullet$ indicates a special address. Note that mint and burn has an implicit constraint that $a$ must belong to a set of authorized addresses.

f ≡...; s_1; s_2; ...

s_1 : flow(u, x, a, b) ∈𝕎
s_2 : flow(v, y, b, a) ∈𝕎

Φ≡u[a] ≥x u'[a] ≤u[a] v'[a] ≥y v'[a] ≥v[a]

edge(u, v, swap, Φ)

f ≡...; s_1; ...; s_2; ...
s_3 ∈g
callback(s_2, g)

s_1 : flow(u, x, a, b) ∈𝕎
s_3: flow(u, y, b, a) ∈𝕎

loan(s_1, s_2, s_3)

loan(s, _, _)
s: flow(u, x, b, a) ∈𝕎

Φ≡u'[a] ≥x u'[a] ≥u[a]

edge(ϵ, u, borrow, Φ)

loan(_, _, s)
s: flow(u, x, a, b) ∈𝕎

Φ≡u[a] ≥x u'[a] ≤u[a]

edge(u, ϵ, payback, Φ)

s : flow(u, x, ∙, a) ∈𝕎
Φ≡u'[a] ≥x u'[a] ≥u[a]

edge(ϵ, u, mint, Φ)

s : flow(u, x, a, ∙) ∈𝕎
Φ≡u[a] ≥x u'[a] ≤u[a]

edge(u, ϵ, burn, Φ)

s : flow(u, x, a, b) ∈𝕎
Φ≡u[a] ≥x u'[a] ≤u[a]

edge(u, ϵ, transfer, Φ)

Edge inference rules. We omit the constraint for $b$ in edge-swap, edge-borrow, edge-payback, and $a$, $b$ in loan.

Edge construction.
<ref> shows the rules for constructing edges in a token flow graph.
Recall that the nodes in a TFG are the tokens that the user holds or wants to acquire, as well as the $void$ node, representing all other parties.
The underlying mechanism of the edge construction procedure is to identify semantic patterns of flow predicates for each AFL construct.
An edge is represented by

${\sf edge}(u, v, p, \Phi),$

where $u$ and $v$ are addresses, $p \in \mathbb{P}$ corresponds to an AFL operator and $\Phi$ is a set of $p$'s behavioral constraints.
We have six types of edges corresponding to different financial operators in <ref>.
We elaborate on their inference rules as follows:

* The user could exchange tokens with DeFi functions or third-party APIs from Uniswap, decentralized exchanges, etc.
The edge-swap rule captures such a pattern by looking for a pair of consecutive back-and-forth flows between two addresses.
When a swap edge is fired, e.g.,

${\sf edge}(u, v, {\sf swap}, \Phi)$,

$u$ tokens are sent in exchange for $v$ tokens. We describe such change of tokens for address $a$ using constraints stored in $\Phi$: $\Phi \equiv u[a] \geq x \land u'[a] \leq u[a] \land$, $v'[a] \geq y \land v'[a] \leq v[a]$,
where $u[a]$ and $v[a]$ denote $a$'s balances of token $u$ and $v$ respectively, while $u'[a]$ and $v'[a]$ denote corresponding balances after firing the edge.
This indicates that $a$ needs at least $x$ amount of $u$ token before swapping, and will get at least $y$ amount of $v$ token after. The invocation of such an operation increases $a$'s balance of token $v$ but decreases its balance of token $u$.

* As mentioned in <ref>, many DeFis provide flash loans, a unique feature that enables a (malicious or benign) user to borrow tokens without collateral, as long as the user pays back the loan and its interest within one single transaction. To understand the edge-borrow and edge-payback rules, we first introduce an auxiliary predicate ${\sf loan}(s_1, s_2, s_3)$ for identifying flash loan patterns in DeFi. In particular, the loan rule first looks for a statement $s_1$ together with its corresponding flow. Following $s_1$, a callback statement $s_2$ is then invoked to register a callback function $g$, which allows the borrower to execute dedicated business logic and produce another flow (from statement $s_3$) that pays the original loan. Once a loan pattern is established, the edge-borrow and edge-payback will be triggered simultaneously and generate corresponding borrow and payback edges. As tokens borrowed could come from different sources, we model the type of token to borrow from and return to using the special node $\void$.

* Flows of tokens from the special address $\bullet$ are directly translated into mint edges via the edge-mint rule. The edge goes from $\void$ to $u$ token with constraints ensuring sufficient $u$ tokens after the call. Similarly, flows of tokens to the special address $\bullet$ directly construct burn edges via the edge-burn rule.

* Other flows that do not fall into the above categories will generate transfer edges via the edge-transfer rule. Specifically, give a flow predicate ${\sf flow}(u,x,a,b)$, the rule generates a token flow edge (from token $u$ to other participants' token clustered in $\void$) labeled with the transfer operator. The constraint on the edge asserts that 192 the sender should have sufficient tokens and 193 her remaining $u$ tokens decrease after the call.

[1]
Input: Initial Blockchain State $S_0$
Output: Token Flow Graph $\zeta$
$\Upsilon \gets \{ s \mapsto \phi \mid \Upsilon \VDash s : \phi \}$ Apply rules in <ref> to compute $\Upsilon$
$\Lambda \gets \{ s \mapsto p \mid \Lambda \VDash s: p \}$, $F \gets \{ p \mid \Lambda \VDash s: p \}$ Apply rules in <ref> to compute $\Lambda$ and $F$
$N \gets \{ u \mid \mathsf{token}(u) \}$
$E' \gets \{ (p,u,v) \mid E \VDash s: \mathsf{edge}(u,v),\ \Lambda(s) = p \}$ Apply rules in <ref> to compute $N$ and $E$
$M \gets \mathsf{config}(S_0)$ Get configuration from initial blockchain state
$W \gets \{ (e,x,y) \mid W \VDash e: (x,y) \}$ Apply rules in <ref> to compute $W$

Construction of Token Flow Graph

𝖺𝗅𝗂𝖺𝗌𝖮𝖿(x_1, x_0)
δ∈{ 𝗍𝗈𝗄𝖾𝗇, 𝖺𝖽𝖽𝗋𝖾𝗌𝗌, 𝖿𝗎𝗇𝖼𝗍𝗂𝗈𝗇, 𝗏𝖺𝗋, 𝗇𝗎𝗆, 𝖺𝗍𝗍𝖺𝖼𝗄𝖾𝗋 }

𝖺𝗅𝗂𝖺𝗌𝖮𝖿(a, b)

s ≡𝖨𝖤𝖱𝖢20(u).𝗍𝗋𝖺𝗇𝗌𝖿𝖾𝗋(b,x) ∈f

s ≡𝖨𝖤𝖱𝖢20(u).𝗍𝗋𝖺𝗇𝗌𝖿𝖾𝗋𝖥𝗋𝗈𝗆(a,b,x) ∈f

s ≡𝖨𝖤𝖱𝖢20(u).𝖻𝗎𝗋𝗇(x) ∈f

s ≡𝖨𝖤𝖱𝖢20(u).𝗆𝗂𝗇𝗍(x) ∈f

Flow inference rules.

Λ⊫s: p
𝗉𝗋𝖾𝖼𝖾𝖽𝖾𝖳𝗈(s_i, s_i+1)
s_i ∈f

α⊫f: p⃗

E_a ⊫s: e_1
E_b ⊫s: e_2

W_a ⊫e_1: (I,I_0)
W_b ⊫e_2: (I_0,I)

E_b ⊫s: e

W_b ⊫e: (I,I_0)

E_b ⊫s: e

W_b ⊫e: (I_0,I)

Λ⊫r: 𝗌𝗐𝖺𝗉(a,u,v,x,y,b)
E_a ⊫r: e_1
E_b ⊫r: e_2

W_a ⊫e_1: (I,I)
W_b ⊫e_2: (I,I)

Λ⊫s: 𝖻𝗈𝗋𝗋𝗈𝗐(u,a,b,x)
E_a ⊫s: e_1
E_b ⊫s: e_2

W_a ⊫e_1: (I,I_0)
W_b ⊫e_2: (I_0,I)

Λ⊫s: 𝗉𝖺𝗒𝖻𝖺𝖼𝗄(u,a,b,y)
E_a ⊫s: e_1
E_b ⊫s: e_2

W_a ⊫e_1: (I_0,I)
W_b ⊫e_2: (I,I_0)

Weight inference rules. $W_a$ is shorthand for filtering out weights that process tokens owned by address $a$.

§ ATTACK SYNTHESIS

Like prior sketch-based synthesizers <cit.>, synthesizes candidate attacks through sketch generation and completion.
The core insight behind 's synthesis algorithm is two-folded.
The search space of sketch generation is constrained by graph reachability over a DeFi's TFG (<ref>), and the state explosion problem in sketch completion is mitigated by our domain-specific compilation rules over AFL's properties (<ref>).
In what follows, we first give an overview of 's synthesis algorithm (<ref>), followed by our attack sketch generation (<ref>) and sketch completion (<ref>) algorithms.

Attack Synthesis
[1]
AtkSyn$D, S_0, \psi$
Input: DeFi $D$, Initial State $S_0$, Attack Goal $\psi$
Output: Attack Program $P$ or $\bot$
$\kappa \gets \top$ initialize knowledge base
$\tfg \gets \textsc{GraphGen}(D, S_0)$ construct token flow graph
$\tilde{P} \gets \textsc{SketchGen}(S_0, \psi, \tfg, \kappa)$ enumerate AFL sketch
$\delta \gets \textsc{CnstGen}(\phi, R)$ generate constraints from sketch
$\mu \gets {\sf solve}(S_0 \land \psi \land \kappa \land \delta))$ get model
$P \gets {\sf complete}(S_0, \tilde{P}, \mu)$ attack instantiation
$P(S_0) \models \psi$ validate attack program $P$
$\kappa \gets \kappa \land \lnot {\sf muc}(P(S_0) \models \psi)$ update KB

§.§ Overview of the Synthesis Algorithm

<ref> shows 's top-level attack synthesis algorithm.
Given a DeFi protocol, its initial state, and an attack goal (in first-order logic), the synthesis algorithm incorporates a two-phased loop, where phase one (line 6) enumerates attack sketches and phase two (line 8) completes concrete attack programs.

\begin{align*}
\psi\quad ::=\quad& e\ \mid\ \lnot \psi\ \mid\ \psi \land \psi \\
e\quad ::=\quad& x\ \mid\ c\ \mid\ p(\vec{x_i})\ \mid\ e_1 \diamond e_2 \ \mid e_1 \odot e_2 \\
\end{align*}

\begin{align*}
x \in \textbf{variables}\quad c \in \textbf{constants}\quad p \in \textbf{predicates} \\
\quad \diamond \in \{+,-,*\} \quad \odot \in \{=,\ge, <\}
\end{align*}

Syntax for attack goal language. $\vec{x_i}$ represents multiple parameters.

Initial state and attack goal.
<ref> shows our specification language for expressing initial states and attack goals.
Initial states and attack goals are expressed through logical expressions over storage variables $x_i$ or constants $c$ in the DeFi environment, e.g., user balances ($B^{\mathit{usdce}}_{t_2}$), blockchain timestamps, msg.sender etc.
A complex logical expression $e$ can be composed by arithmetic and logical operators over atomic expressions and custom predicates.
converts attack goals into their corresponding first-order logic formulas via syntax-directed translation.
For queries that refer to symbols and quantifiers in the program, uses skolemization to make them quantifier-free or reject them otherwise.

The main loops.
Using the rules in <ref>, the algorithm first constructs a token flow graph from the given DeFi protocol and initial state (line 5).
It then invokes an enumeration procedure SketchGen (<ref>) that iteratively searches for candidate attack sketches $\tilde{P}$ (line 6).
Each sketch $\tilde{P}$ is then compiled by CnstGen into constraints $\delta$ that form SMT queries whose solution corresponds to the choices of missing arguments in the attack sketch (line 7).
enumerates the solution (a.k.a. model) of these queries (line 8).
Then, completes the attack sketch $\tilde{P}$ and transforms it into a concrete attack program $P$ through direct syntax transformation (line 9).
The algorithm then validates the effectiveness of the attack, by executing it from the initial state and checking whether the attack goal is satisfied (line 10).
It returns the concrete attack program $P$ upon passing the validation; otherwise, it invokes a conflict-driven clause learning (CDCL) call (line 13) and moves to the next available candidate.

Conflict-driven learning and knowledge base.
To avoid past mistakes, the algorithm also incorporates a knowledge base $\kappa$ (line 4) that keeps track of constraint clauses that are responsible for each failed validation (line 13).[${\sf muc}$ stands for “minimum unsat core”. This corresponds to the feature of unsat core computation, which is broadly available in modern SMT solvers.]
Similar to previous works on conflict-driven program synthesis <cit.>, this allows 's synthesis algorithm to avoid previously failed cases (by associating the “root cause” with corresponding constructs in a candidate program) and refine them for better candidates.
As such, the knowledge base $\kappa$ is passed as the argument of sketch generation (line 6).

Attack Sketch Enumeration
[1]
SketchGen$S_0, \psi, \tfg, \kappa$
Input: Initial State $S_0$, Attack Goal $\psi$, TFG $\tfg$, Knowledge Base $\kappa$
Output: Attack Sketch $\tilde{P}$ or $\bot$
Assume: $\tfg = (\token, \afl, \edgedom, \constraint)$

$R \gets \{\}$ initialize reachable path as ordered set
$T, \Omega \gets {\sf init}(\tfg, S_0)$ initialize token worklist $T$ and constraint store $\Omega$

${\sf\bf choose}\ t \in T$ choose and remove a token from $T$
$E \gets \{ e \mid \forall e \in \edgedom\ .\ e \equiv {\sf edge}(t, *, *, *) \}$ neighboring edges
$e \in E$
if ${\sf unsat}(\Omega \land \kappa \land e.\Phi)$ then continue
$T \gets T \cup \{ e.{\sf out} \}$ include output node to worklist
$\Omega \gets \Omega \land e.\Phi$ update constraint store
$R \gets R \cup \{ e \}$ add edge to reachable path
$\alpha(\psi) \subseteq T$
$\tilde{P} \gets (e.{\sf op} \mid \forall e \in R)$ convert graph to sketch

§.§ Attack Sketch Generation via Graph Reachability Analysis

To generate an attack sketch, performs reachability analysis over the TFG and enumerates a reachable path that consists of multiple edges in the TFG.
The path points from some initial token node (typically $void$, indicating the attacker does not hold that token) to a target token node that the attacker aims to acquire.
Here, each edge is attached with an AFL operator $p$ and a behavioral constraint $\Phi$ that encodes the pre- and post-condition of triggering $p$ (<ref>).

Goal-directed reachability analysis.
An attack goal $\psi$ in <ref> specifies a logic formula over account balances with target token(s) of interest to the attacker.
To satisfy the goal, a feasible sketch has to end up with states that “produce" the target token(s) in $\psi$, by firing a sequence of AFL operators in a path $R$.
Formally speaking, a feasible sketch corresponds to a path in the token flow graph that satisfies the following conditions:

* Satisfiability condition: whether the behavioral constraints $\Phi$ along the path $R$ can be satisfied, and

* Coverage condition: whether the path $R$ covers the target token(s) in the attack goal (denoted by $\alpha(\psi)$).

Sketch enumeration.

Given a token flow graph along with its initial state, attack goal, and knowledge base, the algorithm returns an attack sketch $\tilde{P}$ corresponding to a reachable path.
It consists of a sequence of AFL operators on tokens defined in the TFG.
The algorithm's main loop (line 7-16) is based on a worklist mechanism that gradually refines the current path until a reachable one is constructed.
Initially an empty path $R$, together with the token worklist $T$ and constraint store $\Omega$ is created (line 5-6), where $T$ is initialized as tokens that the attacker holds, and $\Omega$ stores constraints converted from initial state $S_0$.
If the attacker does not hold any tokens in the TFG, we initialize $T$ with $\void$.

At each step of the main loop, a token $t$ is first chosen from the worklist $T$ (line 7).
Then, for each edge $e$ that starts from $t$ (lines 8-9), the algorithm ensures the satisfiability condition is met by checking the conjunction of three sets of constraints using the Z3 solver (line 10); otherwise, it continues with the next available edge.
For a satisfiable edge $e$, the algorithm updates the token worklist by adding its output token $e.o$, the constraint store by adding its constraint $e.\phi$ (the constraint of triggering its corresponding operator), and the reachable path set $R$ by adding $e$ (lines 11-13).
Then, it checks for the coverage condition by seeking the existence of target tokens from $R$ (line 14).
The path $R$ is finally converted into an attack sketch $\tilde{P}$ and return if the coverage condition is met (line 15); otherwise, the algorithm keeps trying for the next pair token $t$ and edge $e$ until it finds a satisfiable one or terminate by exhaustion.
Note that every time a valid sketch $\tilde{P}$ is found and returned, the following lines in <ref> will be invoked.
If $\tilde{P}$ fails to achieve the attack goal, the corresponding root cause will be added to $\kappa$ and fed back to SketchGen.
The $R$, $T$, $\Omega$ will be reinitialized for generating a new sketch and $\kappa$ ensures that the algorithm avoids the previously failed sketches.

[Attack sketch generation]
In <ref>(d), a reachable path on the token flow graph begins at the $\void$ node, representing a common scenario where the attacker initially possesses no tokens and must borrow from other entities (182).
Navigating through the graph (183 - 184), the attacker is then required to repay the borrowed tokens to prevent execution failure by ending with calling payback and going back to the start node $\ding{185}$.
The sequence of corresponding operators (borrow -> swap -> payback) along this generated path constitutes a viable sketch candidate for executing the attack.

§.§ Sketch Completion via Domain-Specific Compilation

We aim to compile the sketch into a constraint system whose solution results in the completion
of an attack program.
In particular, using our AFL semantics, we derive a domain-specific compilation that translates the
invocation of each AFL operator into high-level constraints.
Our constraints are much easier to
solve as they only track the side effects of AFL operators over the attacker’s account balances and filter out low-level semantics of the original DeFi.

<ref> shows the inference rules for generating constraints of different AFL operators defined in <ref>.
The rules derive judgments of the form $p \Downarrow C$, where C corresponds to the set of constraints obtained by symbolically evaluating an AFL operator $p$.
For simplicity, we use two macros ${\uparrow}(u, a, x)$ and ${\downarrow}(u, a, x)$ to denote the constraints for describing a balance increase and decrease of amount $x$ of the token $u$ at address $a$, which compiles to $u'[a] = u[a] + x$ and $u'[a] = u[a] - x$, where $u[a]$ and $u'[a]$ denotes the balance of token $u$ for address $a$ before and after evaluating the corresponding operator $p$.

Each inference rule in <ref> models the change of account balances caused by the corresponding AFL operator.
For instance, the c-transfer rule generates constraints to assert the increased and decreased amounts of recipient and sender, respectively.
The c-swap rule states that from a sender's view (address $a$), the balance of its source token will decrease and its target token will increase.
The recipient's (address $b$) case is the inverse.

In addition to modeling balance changes, the rules also model financial features for certain operators.
For example, for swap operator, besides the macro $\varsigma(a,u,v,x,y,b)$ that describes mutual balance changes between address $a$ and $b$,[This compiles to ${\downarrow}(u,a,x) \land {\uparrow}(u,b,x) \land {\downarrow} (v,b,y) \land {\uparrow}(v,a,y)$.] we introduce $\rho(x,y)$ to model the invariant between token pairs in modern automated market makers (e.g., $x \cdot y = k$ in Uniswap).
Meanwhile, for tokens that provide flash loans, an additional fee is also modeled via $\vartheta(x,y)$ (e.g., $y > x$ in most cases meaning additional interest is charged in payback).
Such constraints are inferred in a data-driven way via analysis of massive amounts of real-world transaction data.
Since the arguments of an AFL operator may refer to local variables, we leverage off-the-shelf pointer analysis to resolve their actual locations.

Given a sketch $\tilde{P} = (p_1, p_2, ... )$, the constraints of $\tilde{P}$ are obtained by
1) applying the inference rule on each $p_i$ and then 2) conjoining all the resulting constraints together:

$\textsc{CnstGen}(S_0, \tilde{P}) = \mathsf{foldl}(S_0, \mathsf{map}(\tilde{P}, \Downarrow ), \land)$.

p ≡𝗍𝗋𝖺𝗇𝗌𝖿𝖾𝗋(u,a,b,x)

p ⇓↓(u, a, x) ↑(u, b, x)

p ≡𝖻𝗎𝗋𝗇(u,a,x)

p ⇓↓(u, a, x)

p ≡𝗆𝗂𝗇𝗍(u,a,x)

p ⇓↑(u, a, x)

p ≡𝗌𝗐𝖺𝗉(a,u,v,x,y,b)

p ⇓ς(a, u, v, x, y, b) ρ(x, y)

p ≡𝖻𝗈𝗋𝗋𝗈𝗐(u,a,b,x)

p ⇓↓(u, a, x) ↑(u, b, x)

p ≡𝗉𝖺𝗒𝖻𝖺𝖼𝗄(u,a,b,y)

p ⇓↓(u, a, y) ↑(u, b, y) ϑ(x,y)

Domain-specific constraint compilation rules.

[1]
CnstComp$S_0, \tilde{P}$
Input: Initial Blockchain State $S_0$, Attack Sketch $\tilde{P}=(f_1, ..., f_n)$
Output: Constraints $\Delta$
$S \gets \{ \phi \mid \phi \in \vec{\phi}=\alpha(f), f \in \tilde{P} \}$ Convert the attack sketch to an ordered set of AFL operators
$\Gamma \gets \{ (t,u,a) \mapsto x \mid 1 \leq t \leq |S| \land \mathsf{token}(u) \land \mathsf{address}(a) \land \mathsf{symbolic}(x)\}$ Initialize variable mapping
$\Delta \gets \varnothing$, $t \gets 0$
Initialize set of constraints and execution step counter
$t \leq |S|$
$\Delta \gets \Delta \cup \{ c \in C \mid \Gamma \Downarrow C \}$ Apply constraint inference rules and update constraints
$t \gets t + 1$ Advance execution step counter

Constraint Compilation

§ EVALUATION

We implement in Python with Z3 version 4.12.2 as the backend constraint solver.
Validation of the synthesized attacks is performed using Foundry <cit.>.
All experiments are conducted on an Amazon EC2® instance with an AMD EPYC 7000® CPU, 8 Cores, and 64G of memory running on Ubuntu 20.04.
We set the default timeout for the solver as 3 hours.
This number is obtained by observing the performance of .
In most cases, it either finishes the process at around 2-3 hours or fails completely.
Our evaluation plans to answer the following research questions:

* (RQ1): How does perform compared to SOTA tools?

* (RQ2): Is effective in detecting known vulnerabilities?

* (RQ3): How effective are the two key designs of and whether will introduce false positives?

* (RQ4): Can be useful in detecting zero-day vulnerabilities?

§.§ Detecting Known Vulnerability (RQ1&RQ2)

To evaluate on known vulnerabilities, we select our benchmarks from the DeFiHackLabs dataset <cit.>, which keeps track of all DeFi hack incidents in the past.
The DeFiHackLabs dataset records 389 incidents (at the time of the submission).
We consider a subset of 200 benchmarks from Jan 2022 to July 2023 and exclude old benchmarks before 2022 because they depend on outdated versions of the Solidity compiler.
Furthermore, we exclude benchmarks from one of these categories:
a) closed source,
b) common vulnerabilities (as referred in <ref>) such as integer overflow, reentrancy, access controls, etc.,
c) insider hacks due to losing primary keys or misconfiguration.
Our dataset ends up with 34 representative benchmarks.
To get better insights into the root causes of the benchmarks, we also categorize them into four types of logical flaws:
1 Token Burn (TB), where the attack can indirectly mint or burn the victim's tokens by calling the corresponding mint or burn function through other public functions (similar to privilege escalation);
2 Pump & Dump (P&D): inflating the price of a token through abnormal financial transactions (e.g., spitefully  inflates the token price through substantial purchases);
3 Price Discrepancy (PP), which allows the attack to generate profits based on the price difference of the same token pair in different smart contracts (e.g., );
4 Swap Rate Manipulation (SR): the attack can directly or indirectly influence the swap rate between multiple token pairs in the same smart contract.
In total, the selected benchmark vulnerabilities have cost $>\$21$M of losses.

As discussed in <ref>, there are two possible existing solutions for our problem.
We select one SOTA tool for each solution as our baseline method.
For sketch generation and completion, we use our sketch generation method (given that no existing tool can strategically generate sketches) and use  <cit.>, the SOTA symbolic reasoning tool for DeFi, for sketch completion.
We select <cit.>, the SOTA tool for cross-contract fuzzing, as our baseline method for the fuzzing solution.
Note that an existing DeFi security tool, DeFiPoser <cit.>, also follows the sketch generation and completion methodology but can only be applied to arbitrage (PP in our benchmark).
Due to its limited scope and lack of open-source implementation, we do not include it as our comparison baseline.

We run , , and on the selected benchmarks using the same computational resource and timeout limit mentioned above.
We report the runtime needed for each method to detect each selected vulnerability.
We also report the average rum time over the success cases (the vulnerabilities that are detected within the time limit) and the overall success rate to assess the effectiveness and efficiency of each tool.

?!width 1pt

Running time of vs. and on the selected benchmark. “TO” means the tool cannot find a valid attack for the corresponding vulnerability within the time limit, and “NA” means the benchmark is not supported.

Name     Category
AES      TB     25.0s     27.0s     TO
BGLD     TB     24.6s     172.0s     TO
BIGFI     TB     25.5s     511.0s     TO
BXH     P&D     27.0s     TO     TO
Discover     PP     25.8s     NA     10251.3s

EGD     P&D     327.3s     2.0s     TO
MUMUG     PP     325.6s     NA     7681.7s
NOVO     TB     24.8s     81.0s     TO
OneRing     P&D     26.8s     TO     TO
RADTDAO     TB     24.7s     627.0s     TO

RES     SR     25.7s     3.0s     TO
SGZ     SR     25.6s     TO     TO
ShadowFi     TB     25.8s     1757.0s     TO
Zoompro     SR     28.8s     TO     TO
NXUSD     P&D     626.3s     TO     TO

NMB     P&D     TO     TO     TO
Lodestar     P&D     TO     TO     TO
SafeMoon     TB     27.8s     TO     TO
Allbridge     PP     TO     NA     TO
Swapos V2     SR     26.1s     321.0s     6322.0s

Axioma     P&D     24.1s     123.0s     TO
0vix     PP     TO     NA     TO
NeverFall     P&D     24.8s     TO     TO
SellToken02     P&D     623.2s     TO     TO
LW     PP     1225.5s     NA     TO

ERC20TokenBank     P&D     619.7s     TO     TO
UN     TB     25.3s     10.1s     TO
CFC     TB     326.1s     164.0s     TO
Themis     P&D     TO     TO     TO
Bamboo     TB     341.3s     42.0s     TO

LUSD     P&D     1250.1s     TO     TO
RodeoFinance     PP     TO     NA     TO
Conic     P&D     618.7s     TO     TO
Carson     PP     TO     TO     TO
Succ. rate      79% (27/34)     38% (13/34)     9% (3/34)
Avg. Time      249.0s     295.4s     8085.0s

<ref> shows the main results of the three tools on the selected 34 benchmarks.
Here, the first two columns represent the name and category of each benchmark.
Column 3-5 shows the running time of , , and , respectively.
We treat “TO” and “NA” as failure cases.
successfully synthesizes the attack programs for 79% benchmarks whereas and only solve 9% and 38% benchmarks, respectively.
This result demonstrates that by modeling financial logic, is significantly more effective in synthesizing DeFi logical bugs compared to SOTA tools.
These tools often struggle to capture application logic and rely on brute-force solutions.
Furthermore, is also more efficient than baseline approaches in that it takes an average time of 249.0 seconds to solve 27 benchmarks.
In comparison, takes an average time of 8,085.0 seconds to solve three benchmarks and takes an average time of 295.4 seconds to solve 13 benchmarks from our dataset.
's high efficiency benefits from its strategical sketch generation, which improves the search efficiency, and its domain-specific compilation, which simplifies the constraints.

§.§ Ablation Study and False Positive (RQ3)

Benefit of domain-specific compilation.
Given that and use the same sketch generation, their performance differences in <ref> are mainly due to the different sketch generation mechanisms.
uses a general-purpose compilation to symbolically evaluate each benchmark using concrete semantics of solidity.
It only solves the three easiest benchmarks.
generates 1,360 and 2,179 constraints for Discover and MUMUG, whereas only generates 64 and 120 constraints, respectively.
This confirms that our domain-specific compilation significantly reduces the amount of generated constraints, greatly simplifies the solving process, and thus enables more successful cases.

Benefits of sketch generation.
To further evaluate the effectiveness of our attack generation algorithm, we replace it with a straightforward breadth-first search and keep all other comments the same.
This method brute forces all operators with a certain length, starting from a length of one, where each operator is treated as a program sketch.
Our result shows that times out on all benchmarks.
This is due to the straightforward solution enumerating a huge number of sketches, causing time out.
The result verifies the necessity of our sketch generation method in improving the overall efficiency of the synthesis process.

False positives.
We run on 50 benign DeFi protocols, which contain the 34 benchmarks in <ref> after fixing the bugs and ten popular DeFi protocols from Defillama (Lido <cit.>, MakerDAO <cit.>, Aave <cit.>, etc.).
For the 10 popular protocols, we treat them as benign because they pass the commercial auditing.
Our results show that timed out (even after we increased the timeout time to 6 hours) on all those benchmarks and did not find any attacks.
This result validates 's capability of avoiding false positives.

A zero-day vulnerability detected by . “victim” stands for the address of the token issued by the Victim contract.

§.§ Detecting Zero-day Vulnerability (RQ3)

We utilized on 5,000 high-profile DeFi protocols on the popular BNB chain and uncovered 10 previously unknown vulnerabilities, ranging from different types of logical flaws (TB/P&D/PP/SR)
Bugs are reported to and confirmed by developers of corresponding projects.
This result confirms 's capability of discovering diverse unseen vulnerabilities, which are challenging for existing pattern matching-based approaches (e.g., DeFiRanger <cit.> and DeFiTainter <cit.>).
Furthermore, the attack synthesized by our tool typically involves more than five transaction actions, which are challenging for general-purpose symbolic execution (e.g., and DeFiPoser <cit.>) and fuzzing tools (e.g., ).

Here, we illustrate one major vulnerability belonging to SR to show how synthesizes the exploit.
<ref> shows the buggy protocol and its exploit generated by .
The victim protocol has a logical flaw in its token swap mechanism, i.e., swapBack function that will cause a price change between victim and wBNB.
Specifically, as shown in <ref>(b), generates a program with six concrete function calls.
Here is the logic to trigger the vulnerability:
1 The attacker takes a flash loan of some WBNB tokens by calling DeFiLender.flashloan.
2 The attacker then calls Victim.transfer to trigger the swapBack.
As shown in <ref>(a), the internal function swapBack swaps a certain amount amt_1 of victim to wBNB, causing a devalue of victim and increasing value of wBNB in the Uniswap contract.
3 the attacker leverage the price change to swap more victim with the loaned wBNB.
4 5 Attacker sequentially swaps Victim to bUSD and bUSD to wBNB.
Given that the attacker gets more victim than usual cases after 3
This enables the attacker to get more wBNBs than its original loaned amount.
6 Eventually, attacker calls DeFiLender.payback to pay back the flash loan and keep the extra $0.2e^{16}$ wBNB as the profit.
The exploit program plunderers approximately 11% of the valuable stablecoins (BUSD) in the liquidity pool as the profit.
spent 318.4 seconds synthesizing this program while neither nor synthesizes a comparable solution within the allotted time frame.

§ DISCUSSION

Generalizability and Scalability.
As illustrated in <ref>, can synthesize attacks for various types of logical bugs that current tools cannot detect.
However, we acknowledge that there are more types of deep logical bugs that our tool has not yet addressed <cit.>.
So far, these vulnerabilities have been discovered by highly experienced human auditors.
By extending our TFG construction and compilation rules, can be generalized to address other vulnerabilities as well.
For example, we can introduce a higher order operator that conducts individual AFL operators multiple times to handle erroneous accounting <cit.>, which requires accumulating a small computational discrepancy multiple times.
Similarly, can also be generalized to common vulnerabilities although they are not our focus.
Our future work will extend to more types of deep logical vulnerabilities.

<ref> demonstrates that significantly outperforms existing tools in synthesizing complicated logical bugs (e.g., the zero-day bug in <ref>).
However, we also notice that still fails to synthesize some ultra-complicated cases (<ref>) due to the limited capability of the SOTA solver.
In our future work, we will explore hybrid approaches that leverage symbolic execution and fuzzing for sketch completion to improve scalability.
Note that our sketch generation would still be valuable in that it is challenging for fuzzing to generate valid transaction sequences.

Manual efforts.
So far still requires certain manual efforts for the generation of the attack goal and initial state specification, as well as additional function mappings.
Here, additional function mappings refer to the auxiliary parameters and extra function calls that must be incorporated when mapping an AFL action back to concrete functions.

These manual efforts are still way lower than the amount of effort needed to summarize patterns from historical attacks or manual auditing.
In addition, pattern summarization and matching have limited generalizability.
Our future works will explore automating these steps, such as leveraging deep learning to generate specifications <cit.> and data mining to extract additional function mappings <cit.>.

As an offensive defense work, our ultimate goal is to uncover more attacks before they actually happen and provide such attacks to DeFi developers and users so that they can improve their protocol or transaction safety.
's capability of providing exploits makes it easier for developers to analyze the root cause and apply proper defenses.
In general, we can patch the vulnerable protocol or add run-time assertions.
For example, we can fix the bug in by upgrading the way of deciding converting price between and such that the price is robust against the dramatic changes in their reservations.

§ RELATED WORK

Smart contract vulnerability analysis.
Existing tools for detecting and analyzing smart contract vulnerabilities can be categorized into either static analysis <cit.> or dynamic analysis <cit.> approaches.
Static tools conduct static analysis or symbolic execution to detect the common vulnerability (mentioned in <ref>) that does not require a deep understanding of a DeFi protocol.
Notably, Securify <cit.> analyzes a smart contract's bytecode and finds pre-defined patterns in its control flow graph corresponding to certain bug types.
Slither <cit.> (also used in ) is the most stable and frequently maintained static analysis framework to analyze smart contracts.
Notable symbolic execution tools include Manticore <cit.>, Mythril <cit.>, Solar <cit.>, and  <cit.> (the SOTA).
As demonstrated in <ref>, without effective sketch generation and domain-specific compilation, solely relying on symbolic execution cannot handle deep logical bugs in DeFi protocols.
Most dynamic and hybrid analysis tools are designed to be used within one smart contract <cit.>.
Without an understanding of protocol logic, the fuzzers that support cross-contract fuzzing (e.g., ItyFuzz <cit.>) cannot maintain their effectiveness in DeFi attack synthesis.

DeFi Security.

The key challenge for DeFi security lies in the larger size and broader scope beyond individual smart contracts as well as the complicated semantics and logic involved.
Aside from Zhou et al. <cit.> which conducts a comprehensive summary of existing DeFi attacks, existing works in this domain mainly follow the methodology of summarizing patterns from existing attack instances and building attack detection tools via pattern matching.
Specifically, DeFiRanger <cit.> lifts the low-level smart contract semantics to high-level ones and uses them to summarize and express patterns.
FlashSyn <cit.> leverages numerical approximation to extract patterns from attack transaction sequences and detect suspicious transactions during run time.
UnifairTrade <cit.> identifies fragile swap pair implementations as patterns.
DeFiTainter <cit.> conducts taint analysis with taint source and target summarized from standard smart contract API templates.
The capability and scalability of these approaches are constrained by the pattern extraction step.
In fact, the above approach can only detect a certain type of price manipulation vulnerability that leverages swap to manipulate token prices (e.g., ).
More recent tools also extend this methodology to other vulnerabilities.
For example, DeFiCrisis <cit.> introduces strategies for exploiting DeFi governance mechanisms by arranging funding to gain profits.
TokenScope <cit.> is designed to detect any inconsistent and phishing behaviors in token applications.
The technique that most aligned with is DeFiPoser <cit.>, which proposes two strategies to facilitate the generation of exploit for profit.
The first strategy creates sketches using heuristics and then completes them with an SMT solver, while the second strategy identifies potential trades through a method known as negative cycle arbitrage detection.
Due to the limitation in sketch generation, this tool can only work with arbitrage detection, whereas can be applied to a variety of DeFi protocols, detect different financial flaws, and synthesize complex trading sequences.

Attack synthesis and exploit generation.
The synthesis of cyber-attacks and the automated generation of exploits have been subjects of significant research interest, aiming to understand and mitigate security vulnerabilities.
The seminal work, AEG <cit.>, used symbolic execution techniques to generate the exploit for the shell program.
Attack synthesis techniques have been applied to many domains, such as Mayhem <cit.> using concolic execution for Linux Kernel, Intellidroid <cit.> using dynamic analysis and fuzzing for Android, HeapHopper <cit.> using bounded model checking for Memory allocator, AASFSM <cit.> using NLP techniques for TCP and DCCP protocols and etc.
Symbolic execution is a well-adopted technique to generate a specific exploit, which creates a set of constraints based on the original program and then solves them by delegating SMT solvers.
Compared with a general symbolic execution technique, first benefits from general financial knowledge to eliminate the search space of synthesis efficiently, then do the domain-specific compilation to generate more lightweight constraints for existing SMT solvers to solve, eventually becoming scalable in the DeFi attack synthesis domain.

§ CONCLUSION

We present , a highly effective attack synthesis framework against deep logical bugs in DeFi protocols.
Different from existing tools that only detect common vulnerabilities in individual smart contracts, effectively models the financial logic in DiFi protocols and synthesizes exploits against logical flows accordingly.
Our evaluation on 34 benchmark DeFi security attacks demonstrates the advantage of over existing smart contract bug-haunting approaches.
We further show that can uncover ten zero-day vulnerabilities from the BNB chain.
Finally, we demonstrate the effectiveness of 's two key designs (sketch generation and completion) and its capability of avoiding false positives.
From extensive evaluation, we can safely conclude that with domain-specific modeling and compilation, symbolic reasoning can be an effective approach for exploit synthesis against deep logical bugs in DeFi protocols.

* $f = s_0; ...; s_n = \vec{s}$

* $f \mapsto e_0; ...; e_m = \vec{e}$

* $e = (u,v)$

* $e.{\sf src} = u$

* $e.{\sf tgt} = v$

* $e.{\sf op} = {\sf swap}$

* $u.{\sf balance} = \{ v \mapsto x \}$

* ${\sf path} = \overrightarrow{\langle e, {\sf params} \rangle}$, two sets of semantics for sketch (abstract) and constraint (domain-specific) generation

* ${\sf precedTo}(s_i, s_j)$ can be simplified as $...; s_i; ...; s_j; ...$

* TFG construction: flow IR first, then edge and node; no flow will be generated if a statement doesn't match any.

* Only tokens are on the graph (static program); parameters and caller (from) receiver (to) are bound to operator (dynamic data) — they should not be on the graph

* $\epsilon$ is a special ACCOUNT, not token.

* “sketch” is written in AFL, which CnstGen applies; “program” is in smart contract language (e.g., Solidity), which can be directly executed.

f ≡s_0; s_1; ...

s ≡if * then f_0 else f_1

s ≡u.transfer(b, x)
a = this

s : flow(u, a, b)

s ≡u.transferFrom(a, b, x)

s : flow(u, a, b)

s ≡u.mint(x)

a = this

s : flow(u, ϵ, a)

s ≡b.burn(x)

a = this

s : flow(u, a, ϵ)

Flow inference rules. $\epsilon$ is a special black hole account (NOT TOKEN) that has infinite number of all tokens, used for expressing special transfer like mint and burn. For all rules, $a \neq b$ and $a \neq \epsilon$.

s : flow(u, a, b)

s : edge(u, u, transfer)

s : flow(u, ϵ, a)

s : edge(u, u, mint)

s : flow(u, a, ϵ)

s : edge(u, u, burn)

f ≡...; s_1; ...; s_2; ...
s_1 : flow(u, a, b)
s_2 : flow(v, b, a)

s_1 : edge(u, v, swap)

f ≡...; s_1; ...; s_2; ...
s_3 ∈g
callback(s_2, g)
s_1 : flow(u, a, b)
s_3: flow(u, b, a)

loan(s_1, s_2, s_3)

loan(s, *, *)
s: flow(u, a, b)

s : edge(u, u, borrow)

loan(*, *, s)
s: flow(u, b, a)

s : edge(u, u, payback)

Edge inference rules.

edge(u, u, transfer)
a, b, x ∈Φ
↘(t, u, a, x) ∪↗(t, u, b, x)

edge(u, u, burn)
a, x ∈Φ
↘(t, u, a, x)

edge(u, u, mint)
a, x ∈Φ
↗(t, u, a, x)

edge(u, v, swap)
a, b, x, y ∈Φ
↘(t, u, a, x) ∪↗(t, u, b, x) ∪↘(t, v, b, y) ∪↗(t, v, a, y)

edge(u, u, borrow)
a, b, x ∈Φ
↘(t, u, a, x) ∪↗(t, u, b, x)

edge(u, u, payback)
a, b, y ∈Φ
↘(t, u, a, y) ∪↗(t, u, b, y) ∪{ y > x }

Domain-specific constraint compilation rules.WIP: merge borrow and payback — need edge map; need swap equation, swap fees, and other tiny adjustments.

Token Flow Graph Generation
[1]
GraphGen$D, \phi$
Input: DeFi $D$, Configuration $\phi$
Output: Token Flow Graph $G(N,E)$, Edge Map $Z$
$N, F \gets {\sf tokens}(D), {\sf functions}(D)$
$H \gets \bigcup_{f \in F} \textsc{InferFlows}(\phi, f)$ flow analysis
$Z \gets \textsc{InferEdges}(F, H)$ edge analysis
$E \gets \{ e \mid s : e \in Z \}$ edge collection
$G(N,E)$, $Z$

AFL Attack Sketch Enumeration Change to constraint-based BFS
[1]
SketchGen$G, \phi, \psi$
Input: Token Flow Graph $G(N,E)$, State $S_0$, Attack Goal $\psi$
Output: Attack Sketch $R'$ or $\bot$
$R_0 \gets []$ initialize path and state
$W \gets [\langle R_0, S_0 \rangle]$ initialize worklist
$\langle R, S \rangle \gets W.{\sf deque}()$
$e, \rho \gets {\sf choose}(E), {\sf choose}(\phi)$
$R' \gets R.{\sf extend}(e)$ extend path
$S' \gets \llbracket R' \rrbracket (S, \rho)$ evaluate on abstract semantics
$S' \models \psi$
yield $R'$
$W.{\sf enque}(\langle R', S' \rangle)$

Attack Synthesis
[1]
AtkSyn$D, \phi, \psi$
Input: DeFi $D$, Configuration $\phi$, Attack goal $\psi$
Output: Attack Program $P$ or $\bot$
$S_0 \gets {\sf init}(\phi)$, $\kappa \gets \varnothing$ get initial state and KB
$G, Z \gets \textsc{GraphGen}(D, \phi)$ get token flow graph and edge map
$R \gets \textsc{SketchGen}(G, \phi, \psi)$ enumerate AFL sketch
$\delta \gets \bigwedge \textsc{CnstGen}(\phi, R)$ generate constraints from sketch
$\mu \gets {\sf solve}(\phi \land \psi \land \delta \land \kappa))$ get model
$P \gets {\sf complete}(D, \phi, \mu, R, Z)$ attack instantiation
$P(S_0) \models \psi$ validate attack program $P$
$\kappa \gets \kappa \land (\bigwedge {\sf muc}(P(S_0) \models \psi))$ update KB
$\bot$ return when exhausted

f ≡s_0; ...; s_n
s_0 : e_0
s_n : e_n

f:⇝∪e_0 ∪... ∪e_n

s ≡if * then s_0 else s_1
s_0: e_0
s_1 : e_1

s : ⇝∪e_0 ∪e_1

s ≡u.𝗍𝗋𝖺𝗇𝗌𝖿𝖾𝗋(𝖻,𝗑)

≡e.i ≥x e.o ≥x

s : ⇝∪e

s ≡u.𝗍𝗋𝖺𝗇𝗌𝖿𝖾𝗋𝖥𝗋𝗈𝗆(a,b,x)

≡e.i ≥x e.o ≥x

s : ⇝∪e

s ≡u.𝗆𝗂𝗇𝗍(x)

≡e.i < e.o

s : ⇝∪e

s ≡u.𝖻𝗎𝗋𝗇(x)

≡e.i > e.o

u.𝖻𝗎𝗋𝗇(x) : ⇝∪e

≡e.i  ⊙e.o

e:𝖾𝖽𝗀𝖾(u,v,𝗌𝗐𝖺𝗉,), ⇝∪e ∖e_1 ∖e_2

𝖼𝖺𝗅𝗅𝖻𝖺𝖼𝗄(s_2, g)
f, g ∈
s_1, s_2 ∈f
s_3 ∈g
𝗉𝗋𝖾𝖼𝖾𝖽𝖾𝖳𝗈(s_1, s_2)
𝗉𝗋𝖾𝖼𝖾𝖽𝖾𝖳𝗈(s_2, s_3)

≡e'.i > 0 e'.o > 0

e: 𝖾𝖽𝗀𝖾(, u,𝗍𝗋𝖺𝗇𝗌𝖿𝖾𝗋,_)

e': 𝖾𝖽𝗀𝖾(, u,𝖻𝗈𝗋𝗋𝗈𝗐,), ⇝∪e' ∖e

≡e'.i > 0 e'.o > 0

e: 𝖾𝖽𝗀𝖾(u,,𝗍𝗋𝖺𝗇𝗌𝖿𝖾𝗋,_)

e': 𝖾𝖽𝗀𝖾(u,, 𝗉𝖺𝗒𝖻𝖺𝖼𝗄,),⇝∪e' ∖e

Inference rules for constructing TFG. $e.i$ and $e.o$ denote the input and output node of an edge $e$.
The predicates are defined in Table <ref>.
Each rule can be interpreted as: if the conditions above the line satisfied, the function (left part below the line) is equivalent to a certain set of graph operations (right part below the line), which adds or deletes certain edges from $\tfg$.

f ≡s_0; ...; s_n

⟨𝕎_f, s_0 ⟩⇝⟨𝕎_0, void ⟩
⟨𝕎_n-1, s_n ⟩⇝⟨𝕎_n, void ⟩
⟨𝕎_0, f ⟩⇝⟨𝕎_n , void ⟩ (fun)

s ≡if _ then f_0 else f_1

⟨𝕎_s, f_0 ⟩⇝⟨𝕎_0, void ⟩
⟨𝕎_s, f_1 ⟩⇝⟨𝕎_1, void ⟩
⟨𝕎_s, s ⟩⇝⟨𝕎_0 ∪𝕎_1, void ⟩ (branch)

s ≡u.transfer(b, x)
a = this
w ≡flow(u, x, a, b)

⟨𝕎_s, s ⟩⇝⟨𝕎_s ∪{s:w}, void ⟩ (flow-out)

s ≡u.transferFrom(a, b, x)
w ≡flow(u, x, a, b)

⟨𝕎_s, s ⟩⇝⟨𝕎_s ∪{s:w}, void ⟩ (flow-in)

s ≡u.mint(x)
a = this
w ≡flow(u, x, ∙, a)

⟨𝕎_s, s ⟩⇝⟨𝕎_s ∪{s:w}, void ⟩ (flow-mint)

s ≡b.burn(x)
a = this
w ≡flow(u, x, a, ∙)

⟨𝕎_s, s ⟩⇝⟨𝕎_s ∪{s:w} ⟩ (flow-burn)

Flow inference rules.

s : flow(u, x, a, b) ∈𝕎
Φ≡u[a] ≥x u'[a] ≤u[a]

edge(u, ϵ, transfer, Φ)

s : flow(u, x, ∙, a) ∈𝕎
Φ≡u'[a] ≥x u'[a] ≥u[a]

edge(ϵ, u, mint, Φ)

s : flow(u, x, a, ∙) ∈𝕎
Φ≡u[a] ≥x u'[a] ≤u[a]

edge(u, ϵ, burn, Φ)

f ≡...; s_1; ...; s_2; ...

s_1 : flow(u, x, a, b) ∈𝕎
s_2 : flow(v, y, b, a) ∈𝕎

Φ≡u[a] ≥x u'[a] ≤u[a] v'[a] ≥y v'[a] ≥v[a]

edge(u, v, swap, Φ)

f ≡...; s_1; ...; s_2; ...
s_3 ∈g
callback(s_2, g)

s_1 : flow(u, x, a, b) ∈𝕎
s_3: flow(u, y, b, a) ∈𝕎

loan(s_1, s_2, s_3)

loan(s, _, _)
s: flow(u, x, b, a) ∈𝕎

Φ≡u'[a] ≥x u'[a] ≥u[a]

edge(ϵ, u, borrow, Φ)

loan(_, _, s)
s: flow(u, x, a, b) ∈𝕎

Φ≡u[a] ≥x u'[a] ≤u[a]

edge(u, ϵ, payback, Φ)

Edge inference rules.$u[a]$ is the user $a$'s balance of token $u$ at current time step; $u'[a]$ is the updated balance after executing $e.{\sf op}$. Perspective is fixed to $a$. $\epsilon$ is a token, and $\bullet$ is a special/blackhole account of $\epsilon$ token.

Attack Sketch Enumeration
[1]
SketchGen$S_0, \psi, \tfg, \kappa$
Input: Initial State $S_0$, Attack Goal $\psi$,
Token Flow Graph $\tfg$, Knowledge Base $\kappa$
Output: Attack Sketch $\tilde{P}$ or $\bot$
Assume: $\tfg = (\token, \afl, \edgedom, \constraint)$

$R \gets \{\}$ initialize reachable path as ordered set
$W, \Omega \gets {\sf init}(\tfg, S_0)$ initialize worklist $W$ and constraint store $\Omega$

${\sf\bf choose}\ t \in W$ choose and remove a token from $W$
$E \gets \{ e \mid \forall e \in \edgedom\ .\ e \equiv {\sf edge}(t, *, *, *) \}$ neighboring edges
$e \in E$
if ${\sf unsat}(\Omega \land \kappa \land e.\Phi)$ then continue
$W \gets W \cup \{ e.{\sf out} \}$ include output node to worklist
$\Omega \gets \Omega \land e.\Phi$ update constraint store
$R \gets R \cup \{ e \}$ add edge to reachable path
$\alpha(\psi) \subseteq W$
$\tilde{P} \gets (e.{\sf op} \mid \forall e \in R)$ convert graph to sketch

Attack Synthesis
[1]
AtkSyn$D, S_0, \psi$
Input: DeFi $D$, Initial State $S_0$, Attack Goal $\psi$
Output: Attack Program $P$ or $\bot$
$\kappa \gets \varnothing$ initialize knowledge base
$\tfg \gets \textsc{GraphGen}(D, S_0)$ construct token flow graph
$\tilde{P} \gets \textsc{SketchGen}(S_0, \psi, \tfg, \kappa)$ enumerate AFL sketch
$\delta \gets \textsc{CnstGen}(\phi, R)$ generate constraints from sketch
$\mu \gets {\sf solve}(S_0 \land \psi \land \kappa \land \delta))$ get model
$P \gets {\sf complete}(S_0, \tilde{P}, \mu)$ attack instantiation
$P(S_0) \models \psi$ validate attack program $P$
$\kappa \gets \kappa \land \lnot {\sf muc}(P(S_0) \models \psi)$ update KB

↓(t, u, a, x) ↑(t, u, b, x)

↓(t, u, a, x)

↑(t, u, a, x)

ς(a, u, v, x, y, b) ρ(x, y)

↓(t, u, a, x) ↑(t, u, b, x)

↓(t, u, a, y) ↑(t, u, b, y) ϑ(x,y)

Domain-specific constraint compilation rules. $\varsigma$ denotes constraints for swap, which is $\varsigma(a, u, v, x, y, b): {\downarrow}(t, u, a, x) \land {\uparrow}(t, u, b, x) \land {\downarrow}(t, v, b, y) \land {\uparrow}(t, v, a, y)$, and $\rho$ denotes price exchange model. A typical $\rho$ can be $\rho(x,y): x * y = k$. Other fees can be expressed by $\vartheta$. A typical $\vartheta$ can be $\vartheta(x,y): y > x$, indicating that applying fees on $x$ gets $y$.

\begin{align*}
\psi ::= \exists x. \psi \mid \lnot \psi \mid \psi \land \psi
\end{align*}

Syntax for attack goal.

#1     #1#1#1     #1     #1     #1     #1#1          #1#1

authorperson1inch. year2023.
titleOne-stop access to decentralized finance.

authorpersona16z. year2023.
titleHalmos: A symbolic testing tool for EVM smart contracts.

authorpersonAAVE. year2023.
titleAave: Open Source Liquidity Protocol.

[Albert et al(2020)]
authorpersonElvira Albert, personShelly Grossman, personNoam Rinetzky, personClara Rodríguez-Núñez, personAlbert Rubio, and personMooly Sagiv. year2020.
Taming Callbacks for Smart Contract Modularity.
journalProc. ACM Program. Lang. volume4, numberOOPSLA, Article articleno209 (datenov year2020), numpages30 pages.

[Ammons et al(2002)]
authorpersonGlenn Ammons, personRastislav Bodík, and personJames R Larus. year2002.
Mining specifications. In booktitleProceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages (Portland, Oregon) (seriesPOPL '02). publisherAssociation for Computing Machinery, addressNew York, NY, USA, pages4–16.

[Avgerinos et al(2014)]
authorpersonThanassis Avgerinos, personSang Kil Cha, personAlexandre Rebert, personEdward J Schwartz, personMaverick Woo, and personDavid Brumley. year2014.
Automatic exploit generation.
journalCommun. ACM volume57, number2 (year2014), pages74–84.

[Binance Smart Chain Developers(2017)]
authorpersonBinance Smart Chain Developers. year2017.
titleBinance Smart Chain Whitepaper.

authorpersonblockworks. year2023.
titleMango Markets Mangled by Oracle Manipulation for $112M.

[Bose et al(2022)]
authorpersonPriyanka Bose, personDipanjan Das, personYanju Chen, personYu Feng, and personChristopher Kruegel. year2022.
SAILFISH: Vetting Smart Contract State-Inconsistency Bugs in Seconds. In booktitle2022 IEEE Symposium on Security and Privacy (SP).

[Cha et al(2012)]
authorpersonSang Kil Cha, personThanassis Avgerinos, personAlexandre Rebert, and personDavid Brumley. year2012.
Unleashing mayhem on binary code. In booktitle2012 IEEE Symposium on Security and Privacy. IEEE, pages380–394.

[Chen et al(2023)]
authorpersonJiaqi Chen, personYibo Wang, personYuxuan Zhou, personWanning Ding, personYuzhe Tang, personXiaoFeng Wang, and personKai Li. year2023.
Understanding the Security Risks of Decentralized Exchanges by Uncovering Unfair Trades in the Wild. In booktitle2023 IEEE 8th European Symposium on Security and Privacy (EuroS&P). pages332–351.

[Chen et al(2019)]
authorpersonTing Chen, personYufei Zhang, personZihao Li, personXiapu Luo, personTing Wang, personRong Cao, personXiuzhuo Xiao, and personXiaosong Zhang. year2019.
TokenScope: Automatically Detecting Inconsistent Behaviors of Cryptocurrency Tokens in Ethereum. In booktitleProceedings of the 2019 ACM SIGSAC Conference on Computer and Communications Security (London, United Kingdom) (seriesCCS '19). publisherAssociation for Computing Machinery, addressNew York, NY, USA, pages1503–1520.

[Chen et al(2022b)]
authorpersonYanju Chen, personJunrui Liu, personYu Feng, and personRastislav Bodik. year2022b.
Tree Traversal Synthesis Using Domain-Specific Symbolic Compilation. In booktitleProceedings of the 27th ACM International Conference on Architectural Support for Programming Languages and Operating Systems (Lausanne, Switzerland) (seriesASPLOS '22). publisherAssociation for Computing Machinery, addressNew York, NY, USA, pages1030–1042.

[Chen et al(2020)]
authorpersonYanju Chen, personChenglong Wang, personOsbert Bastani, personIsil Dillig, and personYu Feng. year2020.
Program Synthesis Using Deduction-Guided Reinforcement Learning. In booktitleComputer Aided Verification, editorpersonShuvendu K Lahiri and personChao Wang (Eds.). publisherSpringer International Publishing, addressCham, pages587–610.

[Chen et al(2022a)]
authorpersonZhiyang Chen, personSidi Mohamed Beillahi, and personFan Long. year2022a.
titleFlashSyn: Flash Loan Attack Synthesis via Counter Example Driven Approximation.
[arxiv]2206.10708 [cs.PL]

[Choi et al(2021)]
authorpersonJaeseung Choi, personDoyeon Kim, personSoomin Kim, personGustavo Grieco, personAlex Groce, and personSang Kil Cha. year2021.
SMARTIAN: Enhancing Smart Contract Fuzzing with Static and Dynamic Data-Flow Analyses. In booktitle2021 36th IEEE/ACM International Conference on Automated Software Engineering (ASE). pages227–239.

authorpersonConsenSys. year2020.
titleMythril: Security Analysis Tool for Ethereum Smart Contracts.

[de Moura and Bjørner(2008)]
authorpersonLeonardo de Moura and personNikolaj Bjørner. year2008.
Z3: An Efficient SMT Solver. In booktitleTools and Algorithms for the Construction and Analysis of Systems. publisherSpringer Berlin Heidelberg, pages337–340.

authorpersondecrypt. year2023.
titleZunami Protocol Loses Over $2.1 Million in Price Manipulation Hack.

[DeFi Prime(2023)]
authorpersonDeFi Prime. year2023.
titleEthereum DeFi Ecosystem.

authorpersonDeFiHackLabs. year2023.
titleDeFi Hacks Reproduce - Foundry.

authorpersondefillama. year2023.
titleDefiLlama - DeFi Dashboard.

authorpersonDYDX. year2023.
titledYdX: Trade Perpetuals on the most powerful trading platform.

[Eckert et al(2018)]
authorpersonMoritz Eckert, personAntonio Bianchi, personRuoyu Wang, personYan Shoshitaishvili, personChristopher Kruegel, and personGiovanni Vigna. year2018.
$\{$HeapHopper$\}$: Bringing bounded model checking to heap implementation security. In booktitle27th USENIX Security Symposium (USENIX Security 18). pages99–116.

[Entriken et al(2018)]
authorpersonWilliam Entriken, personDieter Shirley, personJacob Evans, and personNastassia Sachs. year2018.
titleERC-721: Non-Fungible Token Standard.
howpublishedEthereum Improvement Proposals.
[Online serial]. Available: <https://eips.ethereum.org/EIPS/eip-721>.

[Feist et al(2019)]
authorpersonJosselin Feist, personGustavo Grieco, and personAlex Groce. year2019.
Slither: A Static Analysis Framework for Smart Contracts. In booktitle2019 IEEE/ACM 2nd International Workshop on Emerging Trends in Software Engineering for Blockchain (WETSEB). publisherIEEE.

[Feng et al(2018)]
authorpersonYu Feng, personRuben Martins, personOsbert Bastani, and personIsil Dillig. year2018.
Program Synthesis Using Conflict-Driven Learning. In booktitleProceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation (Philadelphia, PA, USA) (seriesPLDI 2018). publisherAssociation for Computing Machinery, addressNew York, NY, USA, pages420–435.

[Feng et al(2017)]
authorpersonYu Feng, personRuben Martins, personJacob Van Geffen, personIsil Dillig, and personSwarat Chaudhuri. year2017.
Component-Based Synthesis of Table Consolidation and Transformation Tasks from Examples. In booktitleProceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation (Barcelona, Spain) (seriesPLDI 2017). publisherAssociation for Computing Machinery, addressNew York, NY, USA, pages422–436.

[Feng et al(2021)]
authorpersonYu Feng, personEmina Torlak, and personRastislav Bodik. year2021.
Summary-Based Symbolic Evaluation for Smart Contracts. In booktitleProceedings of the 35th IEEE/ACM International Conference on Automated Software Engineering (Virtual Event, Australia) (seriesASE '20). publisherAssociation for Computing Machinery, addressNew York, NY, USA, pages1141–1152.

[foundry team(2021)]
authorpersonfoundry team. year2021.
titleFoundry: A Blazing Fast, Portable and Modular Toolkit for Ethereum Application Development.

[Grech et al(2018)]
authorpersonNeville Grech, personMichael Kong, personAnton Jurisevic, personLexi Brent, personBernhard Scholz, and personYannis Smaragdakis. year2018.
MadMax: Surviving out-of-Gas Conditions in Ethereum Smart Contracts.
journalProc. ACM Program. Lang. volume2, numberOOPSLA, Article articleno116 (dateoct year2018), numpages27 pages.

[Grossman et al(2017)]
authorpersonShelly Grossman, personIttai Abraham, personGuy Golan-Gueta, personYan Michalevsky, personNoam Rinetzky, personMooly Sagiv, and personYoni Zohar. year2017.
Online Detection of Effectively Callback Free Objects with Applications to Smart Contracts.
journalProc. ACM Program. Lang. volume2, numberPOPL, Article articleno48 (datedec year2017), numpages28 pages.

[Gudgeon et al(2020)]
authorpersonLewis Gudgeon, personDaniel Perez, personDominik Harz, personBenjamin Livshits, and personArthur Gervais. year2020.
titleThe Decentralized Financial Crisis.
[arxiv]2002.08099 [cs.CR]

[Guo et al(2019)]
authorpersonZheng Guo, personMichael James, personDavid Justo, personJiaxiao Zhou, personZiteng Wang, personRanjit Jhala, and personNadia Polikarpova. year2019.
Program synthesis by type-guided abstraction refinement.
journalProc. ACM Program. Lang. volume4, numberPOPL (dateDec. year2019), pages1–28.

[Jiang et al(2018)]
authorpersonBo Jiang, personYe Liu, and personW. K. Chan. year2018.
ContractFuzzer: Fuzzing Smart Contracts for Vulnerability Detection. In booktitleProceedings of the 33rd ACM/IEEE International Conference on Automated Software Engineering (Montpellier, France) (seriesASE '18). publisherAssociation for Computing Machinery, addressNew York, NY, USA, pages259–269.

[Kong et al(2023)]
authorpersonQueping Kong, personJiachi Chen, personYanlin Wang, personZigui Jiang, and personZibin Zheng. year2023.
DeFiTainter: Detecting Price Manipulation Vulnerabilities in DeFi Protocols. In booktitleProceedings of the 32nd ACM SIGSOFT International Symposium on Software Testing and Analysis (Seattle, WA, USA) (seriesISSTA 2023). publisherAssociation for Computing Machinery, addressNew York, NY, USA, pages1144–1156.

[Le and Lo(2018)]
authorpersonTien-Duy B Le and personDavid Lo. year2018.
Deep specification mining. In booktitleProceedings of the 27th ACM SIGSOFT International Symposium on Software Testing and Analysis (Amsterdam, Netherlands) (seriesISSTA 2018). publisherAssociation for Computing Machinery, addressNew York, NY, USA, pages106–117.

authorpersonLido. year2023.
titleLido - Liquid Staking for Digital Tokens.

[Liu et al(2023)]
authorpersonJunrui Liu, personYanju Chen, personEric Atkinson, personYu Feng, and personRastislav Bodik. year2023.
Conflict-Driven Synthesis for Layout Engines.
journalProc. ACM Program. Lang. volume7, numberPLDI (dateJune year2023).

[Luu et al(2016)]
authorpersonLoi Luu, personDuc-Hiep Chu, personHrishi Olickel, personPrateek Saxena, and personAquinas Hobor. year2016.
Making Smart Contracts Smarter. In booktitleProceedings of the 2016 ACM SIGSAC Conference on Computer and Communications Security (Vienna, Austria) (seriesCCS '16). publisherAssociation for Computing Machinery, addressNew York, NY, USA, pages254–269.

authorpersonMakerDAO. year2023.
titleMakerDAO: An Unbiased Global Financial System.

[Mandelin et al(2005)]
authorpersonDavid Mandelin, personLin Xu, personRastislav Bodík, and personDoug Kimelman. year2005.
Jungloid Mining: Helping to Navigate the API Jungle. In booktitleProceedings of the 2005 ACM SIGPLAN Conference on Programming Language Design and Implementation (Chicago, IL, USA) (seriesPLDI '05). publisherAssociation for Computing Machinery, addressNew York, NY, USA, pages48–61.

[Mossberg et al(2019)]
authorpersonMark Mossberg, personFelipe Manzano, personEric Hennenfent, personAlex Groce, personGustavo Grieco, personJosselin Feist, personTrent Brunson, and personArtem Dinaburg. year2019.
Manticore: A User-Friendly Symbolic Execution Framework for Binaries and Smart Contracts. In booktitle2019 34th IEEE/ACM International Conference on Automated Software Engineering (ASE). pages1186–1189.

[Nguyen et al(2020)]
authorpersonTai D. Nguyen, personLong H. Pham, personJun Sun, personYun Lin, and personQuang Tran Minh. year2020.
SFuzz: An Efficient Adaptive Fuzzer for Solidity Smart Contracts. In booktitleProceedings of the ACM/IEEE 42nd International Conference on Software Engineering (Seoul, South Korea) (seriesICSE '20). publisherAssociation for Computing Machinery, addressNew York, NY, USA, pages778–788.

[Pacheco et al(2022)]
authorpersonMaria Leonor Pacheco, personMax von Hippel, personBen Weintraub, personDan Goldwasser, and personCristina Nita-Rotaru. year2022.
titleAutomated Attack Synthesis by Extracting Finite State Machines from Protocol Specification Documents.
[arxiv]2202.09470 [cs.CR]

authorpersonPancakeSwap. year2023.
titleEveryone's Favorite DEX.

[Phothilimthana et al(2016)]
authorpersonPhitchaya Mangpo Phothilimthana, personMichael Schuldt, and personRastislav Bodik. year2016.
Compiling a Gesture Recognition Application for a Low-Power Spatial Architecture.
journalSIGPLAN Not. volume51, number5 (datejun year2016), pages102–112.

[Radomski et al(2018)]
authorpersonWitek Radomski, personAndrew Cooke, personPhilippe Castonguay, personJames Therien, personEric Binet, and personRonan Sandford. year2018.
titleERC-1155: Multi Token Standard.
howpublishedEthereum Improvement Proposals.
[Online serial]. Available: <https://eips.ethereum.org/EIPS/eip-1155>.

[Shou et al(2023)]
authorpersonChaofan Shou, personShangyin Tan, and personKoushik Sen. year2023.
ItyFuzz: Snapshot-Based Fuzzer for Smart Contract. In booktitleProceedings of the 32nd ACM SIGSOFT International Symposium on Software Testing and Analysis (Seattle, WA, USA) (seriesISSTA 2023). publisherAssociation for Computing Machinery, addressNew York, NY, USA, pages322–333.

[Solar-Lezama et al(2006)]
authorpersonArmando Solar-Lezama, personLiviu Tancau, personRastislav Bodik, personSanjit Seshia, and personVijay Saraswat. year2006.
Combinatorial sketching for finite programs. In booktitleProceedings of the 12th international conference on Architectural support for programming languages and operating systems (San Jose, California, USA) (seriesASPLOS XII). publisherAssociation for Computing Machinery, addressNew York, NY, USA, pages404–415.

authorpersonsolidityscan. year2023.
titleROE Finance hack Analysis — Price Manipulation.

[Tether Developers(2014)]
authorpersonTether Developers. year2014.
titleTether: Fiat currencies on the Bitcoin blockchain.

[Torlak and Bodik(2014)]
authorpersonEmina Torlak and personRastislav Bodik. year2014.
A Lightweight Symbolic Virtual Machine for Solver-Aided Host Languages. In booktitleProceedings of the 35th ACM SIGPLAN Conference on Programming Language Design and Implementation (Edinburgh, United Kingdom) (seriesPLDI '14). publisherAssociation for Computing Machinery, addressNew York, NY, USA, pages530–541.

[Tsankov et al(2018)]
authorpersonPetar Tsankov, personAndrei Dan, personDana Drachsler-Cohen, personArthur Gervais, personFlorian Bünzli, and personMartin Vechev. year2018.
Securify: Practical Security Analysis of Smart Contracts. In booktitleProceedings of the 2018 ACM SIGSAC Conference on Computer and Communications Security (Toronto, Canada) (seriesCCS '18). publisherAssociation for Computing Machinery, addressNew York, NY, USA, pages67–82.

authorpersonUniswap. year2023.
titleThe Uniswap Protocol.

[Vogelsteller and Buterin(2015)]
authorpersonFabian Vogelsteller and personVitalik Buterin. year2015.
ERC-20: Token Standard.
journalEthereum Improvement Proposals number20 (dateNov year2015).
[Online serial]. Available: <https://eips.ethereum.org/EIPS/eip-20>.

[Wong and Lie(2016)]
authorpersonMichelle Y Wong and personDavid Lie. year2016.
Intellidroid: a targeted input generator for the dynamic analysis of android malware.. In booktitleNDSS, Vol. volume16. pages21–24.

[Wood et al(2014)]
authorpersonGavin Wood et al year2014.
Ethereum: A secure decentralised generalised transaction ledger.
journalEthereum project yellow paper volume151, number2014 (year2014), pages1–32.

[Wu et al(2021)]
authorpersonSiwei Wu, personDabao Wang, personJianting He, personYajin Zhou, personLei Wu, personXingliang Yuan, personQinming He, and personKui Ren. year2021.
titleDeFiRanger: Detecting Price Manipulation Attacks on DeFi Applications.
[arxiv]2104.15068 [cs.CR]

[Wüstholz and Christakis(2020)]
authorpersonValentin Wüstholz and personMaria Christakis. year2020.
Harvey: A Greybox Fuzzer for Smart Contracts. In booktitleProceedings of the 28th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering (Virtual Event, USA) (seriesESEC/FSE 2020). publisherAssociation for Computing Machinery, addressNew York, NY, USA, pages1398–1409.

[Zhang et al(2023)]
authorpersonZhuo Zhang, personBrian Zhang, personWen Xu, and personZhiqiang Lin. year2023.
Demystifying exploitable bugs in smart contracts. In booktitle2023 IEEE/ACM 45th International Conference on Software Engineering (ICSE). IEEE, pages615–627.

[Zhou et al(2021)]
authorpersonL Zhou, personK Qin, personA Cully, personB Livshits, and personA Gervais. year2021.
On the just-in-time discovery of profit-generating transactions in DeFi Protocols. pages919–936.

[Zhou et al(2023)]
authorpersonLiyi Zhou, personXihan Xiong, personJens Ernstberger, personStefanos Chaliasos, personZhipeng Wang, personYe Wang, personKaihua Qin, personRoger Wattenhofer, personDawn Song, and personArthur Gervais. year2023.
Sok: Decentralized finance (defi) attacks. In booktitle2023 IEEE Symposium on Security and Privacy (SP). IEEE, pages2444–2461.

Compare against and .

Name     Category                 Loss (USD)
AES      Token Burn     25.0s     27.0s     TO     60K
BGLD     Token Burn     24.6s     172.0s     TO     18K
BIGFI     Token Burn     25.5s     511.0s     TO     30K
BXH     Pump&Dump     27.0s     TO     TO     40K
Discover     Price Discrepancy     25.8s     NA     10251.3s     15K

EGD     Pump&Dump     327.3s     2.0s     TO     36K
MUMUG     Price Discrepancy     325.6s     NA     7681.7s     57K
NOVO     Token Burn     24.8s     81.0s     TO     85K
OneRing     Pump&Dump     26.8s     TO     TO     1.5M
RADTDAO     Token Burn     24.7s     627.0s     TO     94K

RES     Swap Rate Manipulate     25.7s     3.0s     TO     290K
SGZ     Swap Rate Manipulate     25.6s     TO     TO     25K
ShadowFi     Token Burn     25.8s     1757.0s     TO     330K
Zoompro     Swap Rate Manipulate     28.8s     TO     TO     61K
NXUSD     Pump&Dump     626.3s     TO     TO     50K

NMB     Pump&Dump     TO     TO     TO     76K
Lodestar     Pump&Dump     TO     TO     TO     4.0M
SafeMoon     Token Burn     27.8s     TO     TO     8.9M
Allbridge     Price Discrepancy     TO     NA     TO     550K
Swapos V2     Swap Rate Manipulate     26.1s     321.0s     6322.0s     468K

Axioma     Pump&Dump     24.1s     123.0s     TO     5K
0vix     Price Discrepancy     TO     NA     TO     2M
NeverFall     Pump&Dump     24.8s     TO     TO     74K
SellToken02     Pump&Dump     623.2s     TO     TO     197K
LW     Price Discrepancy     1225.5s     NA     TO     50K

ERC20TokenBank     Pimp&Pump     619.7s     TO     TO     111K
UN     Token Burn     25.3s     10.1s     TO     26K
CFC     Token Burn     326.1s     164.0s     TO     16K
Themis     Pump&Dump     TO     TO     TO     370K
Bamboo     Token Burn     341.3s     42.0s     TO     50K

LUSD     Pump&Dump     1250.1s     TO     TO     10K
RodeoFinance     Price Discrepancy     TO     NA     TO     888K
Conic     Pump&Dump     618.7s     TO     TO     934K
Carson     Price Discrepancy     TO     TO     TO     150K
Avg. Time      249.0s     295.4s     8085.0s     Sum: 21.6M