On the Just-In-Time Discovery of Profit-Generating Transactions in DeFi Protocols
论及时发现 DeFi 协议中的创利交易

I. INTRODUCTION I.引言

Blockchain-based decentralized finance protocols (commonly referred to as DeFi ) have attracted a recent surge in popularity and value stored exceeding 13 billion USD. The currently most popular DeFi platforms are based on the Ethereum blockchain and its system of smart contracts, which regularly gives nascence to new applications, mirrored and inspired by the traditional centralized finance system. Examples are asset exchanges [24], [58], margin trading [3], [24], lending/borrowing platforms [27], [30], and derivatives [27]. DeFi , moreover, can surprise with novel use-cases such as
基于区块链的去中心化金融协议（通常称为 DeFi）最近大受欢迎，其价值已超过 130 亿美元。目前最流行的 DeFi 平台基于以太坊区块链及其智能合约系统，该系统定期推出新的应用，与传统的中心化金融系统相呼应，并受到其启发。例如，资产交易所[24]、[58]、保证金交易[3]、[24]、借贷平台[27]、[30]和衍生品[27]。此外，DeFi 还能为新的用例带来惊喜，例如

Our contributions are as follows:
我们的贡献如下

• DeFiPoser-ARB: We build a directed DeFi market graph and identify negative cycles with the Bellman-Ford-Moore algorithm. A local search then allows us to discover parameters for profitable arbitrage transactions in near-real-time (average of 6.43 seconds per block).
  DeFiPoser-ARB：我们构建了一个有向 DeFi 市场图，并使用 Bellman-Ford-Moore 算法识别负循环。然后，通过局部搜索，我们可以在近乎实时的时间内（平均每个区块 6.43 秒）发现有利可图的套利交易参数。
• DEFIPoSER-SMT and Space Reduction: To discover more demanding trades than arbitrage, we model the DeFi systems using a state transition model, which we translate to a logical representation in the Z 3 theorem prover. We introduce heuristics to significantly prune the search space to achieve a near real-time transaction discovery (average of 5.39 seconds per block).
  DEFIPoSER-SMT 和空间缩减：为了发现比套利要求更高的交易，我们使用状态转换模型对 DeFi 系统进行建模，并将其转化为 Z 3 定理证明器中的逻辑表示。我们引入了启发式方法来大幅削减搜索空间，以实现接近实时的交易发现（平均每个区块 5.39 秒）。
• Miner Extractable Value (MEV) and Security: We show how DEFIPOSER-SMT discovers the economic attack on bZx, which yields over 0.48 M USD, and that this opportunity window was open for over 69 days. Given optimal adversarial mining strategies provided by a Markov Decision Process, we show quantitatively that MEV opportunities can deteriorate the blockchain security. For example, a rational MEV-aware miner with a hash rate of $10\mathrm{\%}$$10\mathrm{\%}$10%10 \% will fork the blockchain if an MEV opportunity exceeds 4 times the block reward and the
  矿工可提取价值 (MEV) 和安全性：我们展示了 DEFIPOSER-SMT 如何发现对 bZx 的经济攻击，该攻击产生了超过 48 万美元的收益，而且该机会窗口开放时间超过 69 天。考虑到马尔可夫决策过程提供的最佳对抗性挖矿策略，我们从数量上表明，MEV 机会会降低区块链的安全性。例如，一个哈希率为 $10\mathrm{\%}$$10\mathrm{\%}$10%10 \% 的理性MEV感知矿工会在MEV机会超过区块奖励的4倍时分叉区块链，而当MEV机会超过 $10\mathrm{\%}$$10\mathrm{\%}$10%10 \% 时，该矿工就会分叉区块链。
  miner failed to claim the source of MEV.
  矿工未能申报 MEV 的来源。
• Trading Strategy Validation: We validate the trading strategies discovered by DEFIPOSER-ARB and DEFIPOSER-SMT on a locally-deployed blockchain that mirrors the real network. We estimate that the found strategies yield 4,103.22 ETH (1,641,288 USD) and $1,552.32$$1,552.32$1,552.321,552.32 ETH (620,928 USD) of profit between the Ethereum block $9,100,000$$9,100,000$9,100,0009,100,000 to $10,050,000$$10,050,000$10,050,00010,050,000 ( 150 days from December 2019 to May 2020). We demonstrate that our tools’ capital requirements are minimal: the majority of the strategies require less than 150.00 ETH (60,000 USD), and only 0.40 ETH (160 USD) when using flash loans.
  交易策略验证：我们在本地部署的反映真实网络的区块链上验证了 DEFIPOSER-ARB 和 DEFIPOSER-SMT 发现的交易策略。我们估计，在以太坊区块 $9,100,000$$9,100,000$9,100,0009,100,000 到 $10,050,000$$10,050,000$10,050,00010,050,000 之间（从 2019 年 12 月到 2020 年 5 月的 150 天），发现的策略产生了 4,103.22 ETH（1,641,288 美元）和 $1,552.32$$1,552.32$1,552.321,552.32 ETH（620,928 美元）的利润。我们证明，我们的工具对资金的要求极低：大多数策略所需的资金不到 150.00 ETH（60,000 美元），使用闪贷时只需 0.40 ETH（160 美元）。
  Paper organization: The remainder of the paper is organized as follows. Section II elaborates on the DeFi background, discusses stable coins and flash loans. Section III describes how we encode DeFi protocols into state transition models. Section IV applies negative cycle detection to find DeFi arbitrage opportunities. Section V presents our heuristics and techniques to enable the autonomous discovery of adversarial strategies. Section VI presents our empirical evaluation and quantitative analysis of the found strategies on previous Ethereum blockchain blocks. Section VII discusses DEFIPOSER’s blockchain security implication. We discuss related works in Section VIII and conclude the paper in Section IX.
  论文结构：本文的其余部分安排如下。第二节阐述了 DeFi 的背景，讨论了稳定币和闪贷。第三节介绍我们如何将 DeFi 协议编码为状态转换模型。第 IV 节应用负循环检测来寻找 DeFi 套利机会。第五节介绍了我们自主发现对抗策略的启发式方法和技术。第六节介绍我们在以太坊区块链上对发现的策略进行的实证评估和定量分析。第七节讨论 DEFIPOSER 的区块链安全含义。我们在第八节讨论相关工作，并在第九节对本文进行总结。

II. BACKGROUND II.背景情况

A. Decentralized Finance (DeFi)
A.分散式融资（DeFi）

Flash loans, therefore, entail two interesting properties. First, the lender is guaranteed that the borrower will repay the loan. If the repayment is not performed, the loan would not be given. Second, the borrower can technically request any amount of capital, up to the amount of funds available in a flash loan pool, given a constant payment which corresponds to the blockchain transaction fees (about 10 USD for the most common flash loan providers). The borrower hence can have access to millions of USD with just a few initial USD and hence is not exposed to the currency risk of the lent asset.
因此，闪电贷款有两个有趣的特性。首先，贷款人保证借款人会偿还贷款。如果不还款，就不会发放贷款。其次，从技术上讲，借款人可以申请任何金额的资金，只要支付与区块链交易费用（最常见的闪电贷款提供商约为 10 美元）相当的固定费用，就可以获得闪电贷款池中的可用资金。因此，借款人只需支付几美元的初始资金，就可以获得数百万美元的资金，而且不会面临借出资产的货币风险。

III. DEFi MODELING III.定义模型

A. System Model A.系统模型

B. Trader Model B.交易员模式

C. Notation C.符号

D. States D.国家

E. Transitions E.过渡

Our state transition function is ${\mathcal{F}}^{\mathbb{T}}(s\in S,a\in A,x)\to S$${\mathcal{F}}^{\mathbb{T}}(s\in S,a\in A,x)\to S$F^(T)(s in S,a in A,x)rarr S\mathcal{F}^{\mathbb{T}}(s \in S, a \in A, x) \rightarrow S, outputs the next state if action $a$$a$aa with parameter $x$$x$xx is performed on state $s$$s$ss by trader $\mathbb{T}$$\mathbb{T}$T\mathbb{T}. Given a strategy with $n$$n$nn actions, where $a_i$$a_i$a_(i)a_{i} and $x_i$$x_i$x_(i)x_{i} represents the $i^{\text{th}}$$i^{\text{th }}$i^("th ")i^{\text {th }} action and parameter
我们的状态转换函数是 ${\mathcal{F}}^{\mathbb{T}}(s\in S,a\in A,x)\to S$${\mathcal{F}}^{\mathbb{T}}(s\in S,a\in A,x)\to S$F^(T)(s in S,a in A,x)rarr S\mathcal{F}^{\mathbb{T}}(s \in S, a \in A, x) \rightarrow S ，如果交易者 $\mathbb{T}$$\mathbb{T}$T\mathbb{T} 在状态 $s$$s$ss 上执行了参数为 $x$$x$xx 的行动 $a$$a$aa ，则输出下一个状态。给定一个有 $n$$n$nn 行动的策略，其中 $a_i$$a_i$a_(i)a_{i} 和 $x_i$$x_i$x_(i)x_{i} 表示 $i^{\text{th}}$$i^{\text{th }}$i^("th ")i^{\text {th }} 行动，参数为

F. Objective F.目标

G. Base cryptocurrency asset
G. 基础加密货币资产

H. DEFIPOSER Design Choices
H.DEFIPOSER 设计选择

IV. Applying Negative Cycle Detection to DeFi Arbitrage
IV.将负周期检测应用于 DeFi 套利

A. Negative Cycle Detection to Detect Arbitrage
A.检测套利的负循环检测法

B. Negative Cycle Detection Algorithms
B.负循环检测算法

Algorithm 1: Negative cycle arbitrage detection.
    Input:
    \(s_{0} \leftarrow\) Initial state \(;\) target \(\leftarrow\) Minimum revenue target
    Output: revenue \(_{\text {total }}\)
    \(s \leftarrow s_{0} ; g \leftarrow\) buildGraph \((N, E, s) ;\) revenue \(_{\text {total }} \leftarrow 0\)
    while hasNegativeCycle(g) do
        cycle \(\leftarrow\) getNegativeCycle(graph)
        \(p \leftarrow \operatorname{getPath}(\) cycle \()\)
        (revenue, \(s) \leftarrow \operatorname{search}(p)\)
        if revenue \(>\) target then
            revenue \(_{\text {total }} \leftarrow\) revenue \(_{\text {total }}+\) revenue
        end
        \(g \leftarrow \operatorname{buildGraph}(N, E, s)\)
    end
    return revenue \(_{\text {total }}\)
    Function buildGraph \((N, E, s \in S)\) is
        \# fetch the spot price for each \(e \in E\)
        \# build the graph \(g\); where \(w_{c_{i}, c_{j}}=-\log \left(p_{c_{i}, c_{j}}^{\text {spot }}\right)\)
        return \(g\)
    end
    Function hasNegativeCycle \((g)\) is
        return (Detects a negative cycle?)
    end
    Function getPath(cycle) is
        \(p \in P\) connects \(\mathbb{T}\) 's baseasset with cycle.
        return \(p\)
    end
    Function \(\operatorname{search}(p)\) is
        \# find the parameters for path \(p\)
        \(s^{\prime} \leftarrow\) state after executinng the strategy
        return (revenue, \(s^{\prime}\) )
    end

V. DESIGN OF DEFIPOSER-SMT
V.除颤器-SMT 的设计

A. Choosing an SMT Solver for DEFIPOSER-SMT
A.为 DEFIPOSER-SMT 选择 SMT 仿真器