PaperlayerView exact revision on arXiv

Source-linked AI summary

On the Just-In-Time Discovery of Profit-Generating Transactions in DeFi Protocols

Liyi Zhou, Kaihua Qin, Antoine Cully, Benjamin Livshits, Arthur Gervais

arXiv:2103.02228v1cs.CR

TL;DR

The paper addresses how to automatically discover profitable transactions across composable DeFi protocols and what those opportunities imply for blockchain security. It develops graph-based arbitrage detection and theorem-prover-based strategy search, estimating substantial revenues and quantifying MEV-driven fork thresholds. The study also identifies scope and scalability constraints arising from block-level state modeling and heuristic path pruning.

  • Problem

    Composable DeFi enables arbitrage and high-revenue trades, creating a need for automated tools that help understand their financial and protocol implications.

  • Method

    The paper develops DEFIPOSER-ARB using negative-cycle detection and DEFIPOSER-SMT using logical DeFi models in a theorem prover.

  • Results

    191.48 ETH and 72.44 ETH are the estimated average weekly revenues of DEFIPOSER-ARB and DEFIPOSER-SMT, respectively, over 150 days with 96 DeFi actions and 25 assets.

  • Takeaways & Limitations

    The tools quantify both revenue opportunities and consensus-security risks, including a 4-block-reward fork threshold for an Ethereum miner with 10% hash rate.

  • Takeaways & Limitations

    The study assumes block-level state changes, so it may miss profitable trades arising from transactions and state updates within the same block.

Abstract

from arXiv · show

In this paper, we investigate two methods that allow us to automatically create profitable DeFi trades, one well-suited to arbitrage and the other applicable to more complicated settings. We first adopt the Bellman-Ford-Moore algorithm with DEFIPOSER-ARB and then create logical DeFi protocol models for a theorem prover in DEFIPOSER-SMT. While DEFIPOSER-ARB focuses on DeFi transactions that form a cycle and performs very well for arbitrage, DEFIPOSER-SMT can detect more complicated profitable transactions. We estimate that DEFIPOSER-ARB and DEFIPOSER-SMT can generate an average weekly revenue of 191.48ETH (76,592USD) and 72.44ETH (28,976USD) respectively, with the highest transaction revenue being 81.31ETH(32,524USD) and22.40ETH (8,960USD) respectively. We further show that DEFIPOSER-SMT finds the known economic bZx attack from February 2020, which yields 0.48M USD. Our forensic investigations show that this opportunity existed for 69 days and could have yielded more revenue if exploited one day earlier. Our evaluation spans 150 days, given 96 DeFi protocol actions, and 25 assets. Looking beyond the financial gains mentioned above, forks deteriorate the blockchain consensus security, as they increase the risks of double-spending and selfish mining. We explore the implications of DEFIPOSER-ARB and DEFIPOSER-SMT on blockchain consensus. Specifically, we show that the trades identified by our tools exceed the Ethereum block reward by up to 874x. Given optimal adversarial strategies provided by a Markov Decision Process (MDP), we quantify the value threshold at which a profitable transaction qualifies as Miner ExtractableValue (MEV) and would incentivize MEV-aware miners to fork the blockchain. For instance, we find that on Ethereum, a miner with a hash rate of 10% would fork the blockchain if an MEV opportunity exceeds 4x the block reward.

DeFi platforms?

DeFi combines interoperable blockchain applications whose composability enables both arbitrage and high-revenue trades exploiting protocol states. The paper presents automated tools to discover such transactions and examines their financial and consensus-security implications.

  • DeFi platforms?: DeFi protocols can be composed across exchanges, lending, borrowing, and other applications, enabling chained trading and arbitrage opportunities.Atomic composition can support risk-free arbitrage, while flash loans enable complex high-revenue trades.
  • DeFi platforms?: The paper presents DEFIPOSER-ARB and DEFIPOSER-SMT to automatically create profit-generating transactions from composable DeFi protocols.The tools are designed to find and execute new transactions at every block.
  • DeFi platforms?: DEFIPOSER-ARB uses a directed market graph and negative-cycle detection, while DEFIPOSER-SMT models DeFi systems in a theorem prover for more demanding trades.The two tools report average search times of 6.43 and 5.39 seconds per block, respectively.
  • DeFi platforms?: DEFIPOSER-SMT identifies the bZx economic attack, while the paper quantifies how profitable transactions can threaten blockchain consensus through MEV-driven forks.The reported bZx opportunity yielded over 0.48M USD, and a 10% hash-rate miner forks above 4 block rewards.
  • DeFi platforms?: The evaluation estimates 4,103.22 ETH and 1,552.32 ETH of profit for DEFIPOSER-ARB and DEFIPOSER-SMT over 150 days.The strategies were validated on a locally deployed blockchain mirroring the real network.

III. DEFI MODELING

The DeFi model represents protocols, assets, trader balances, and blockchain state as a system of actions and transitions. Strategies are parameterized paths executed across platforms, with state considered at block boundaries.

  • III. DEFI MODELING: A strategy is a parameterized path: a sequence of actions across DeFi platforms with an initial model state.Multiple actions can be encapsulated in one transaction and executed atomically in sequence.
  • III. DEFI MODELING: The model considers blockchain state only after all transactions in a block have executed, rather than intermittent within-block states.This block-level assumption excludes state changes occurring between transactions in the same block.
  • III. DEFI MODELING: The trader selects protocol actions and supplies parameters such as cryptocurrency amounts sent to DeFi platforms.The trader’s assets are limited by public flash-loan liquidity, and unconfirmed transactions are not observed.
  • III. DEFI MODELING: The overall system state combines the trader’s asset portfolio with DeFi storage variables read or written by modeled actions.The state after action i is denoted s_i, beginning from initial state s_0.

E. Transitions

DEFIPOSER models DeFi strategies as sequential state transitions and seeks parameters that maximize a chosen base asset while preserving other portfolio balances. Its design combines path pruning, parameter search, and strategy execution.

  • E. Transitions: A transition function maps a state, action, and action parameter to the next state after the trader performs that action.Sequential application of actions produces the final state s_n from s_0.
  • E. Transitions: The trader chooses a base cryptocurrency asset and maximizes its balance while keeping other portfolio balances unchanged.The model assumes a single base asset, although multiple base currencies could increase potential financial results.
  • E. Transitions: DEFIPOSER comprises path pruning, parameter search, and strategy combination or execution components.The parameter search maximizes revenue for a given path, while execution determines how discovered strategies are used.
  • E. Transitions: DEFIPOSER-ARB targets cyclic paths, whereas heuristic pruning can support arbitrary path structures and DEFIPOSER-SMT handles more general strategies.Local search is faster for simple cyclic arbitrage, but it does not provide satisfiability proofs.
  • E. Transitions: Arbitrage detection converts market prices into negative-log edge weights, where a negative cycle represents an arbitrage opportunity.The arbitrage revenue is converted into the base asset through the best connecting market.

B. Negative Cycle Detection Algorithms

Negative-cycle detection provides an efficient route to cyclic arbitrage, but DeFi’s volume-dependent prices require graph updates after each action. DEFIPOSER-SMT extends discovery to profitable non-cyclic strategies through theorem-prover reasoning.

  • B. Negative Cycle Detection Algorithms: The arbitrage algorithm repeatedly detects a negative cycle, extracts a path, searches its parameters, records qualifying revenue, and rebuilds the graph.The loop continues while a negative cycle exists and applies a minimum revenue target.
  • B. Negative Cycle Detection Algorithms: DeFi AMM prices vary with transaction volume, so the market graph must be rebuilt after every action.Larger transaction sizes generally worsen trading prices, unlike fixed bid-ask prices within quoted sizes.
  • B. Negative Cycle Detection Algorithms: DEFIPOSER-SMT uses a theorem prover to explore logical DeFi models and find concrete profitable strategies beyond complete cycles.The bZx strategy sends Ether without receiving assets before executing an arbitrage cycle, so it is not itself a complete cycle.
  • B. Negative Cycle Detection Algorithms: DEFIPOSER-SMT is more general than DEFIPOSER-ARB because it can operate on non-cyclic strategies.DEFIPOSER-ARB cannot identify such strategies through cyclic negative-cycle detection.

A. Choosing an SMT Solver for DEFIPOSER-SMT

DEFIPOSER-SMT uses theorem proving and systematic path exploration to find profitable DeFi strategies beyond complete cycles, while heuristics reduce path-exploration cost. The resulting search is best-effort because pruning can remove profitable strategies and its revenue loss cannot be quantified.

  • A. Choosing an SMT Solver for DEFIPOSER-SMT: DEFIPOSER-SMT logically formulates profitable strategies and uses systematic path exploration to find concrete satisfying instantiations.The state-transition model encodes the initial state, applies actions iteratively, and constrains the objective function.
  • A. Choosing an SMT Solver for DEFIPOSER-SMT: The model requires SMT solvers supporting floating-point arithmetic because it uses the theory of real numbers.The encoding proceeds through initial-state predicates, iterated state-transition predicates, and objective constraints.
  • B. Path Pruning: Heuristics prune paths to address combinatorial path explosion, but they may remove profitable strategies, making DEFIPOSER-SMT a best-effort tool.The heuristics constrain action count, entry and exit structure, action dependence, reversals, branching, and loops.
  • B. Path Pruning: Heuristic 4 retains paths when actions share trader-relevant storage variables, such as both actions reading or writing T.c1.Independent actions have disjoint relevant storage-variable sets and can be pruned.
  • B. Path Pruning: Heuristics can reduce the number of paths, but the resulting revenue reduction cannot be quantified because the optimal revenue is unavailable under combinatorial explosion.The evaluation measures path-count reduction but lacks an avenue to quantify revenue lost through pruning.
  • C. DEFIPOSER-SMT Revenue Optimizer: The revenue optimizer first establishes coarse bounds using multiples of 10 and then applies binary search to find the optimal satisfiable revenue.The SMT solver validates whether free-variable initializations satisfy the specified requirements.

D. Comparing DEFIPOSER-SMT to DEFIPOSER-ARB

DEFIPOSER-SMT is more general than DEFIPOSER-ARB because it can encode non-cyclic strategies, but both remain best-effort tools with important scalability, modeling, and evaluation limitations.

  • Comparison: DEFIPOSER-SMT can encode arbitrary strategies and detect non-cyclic opportunities that DEFIPOSER-ARB cannot capture.The bZx strategy sends Ether without receiving assets before executing an arbitrage cycle, so it is not a complete cycle.
  • Comparison: DEFIPOSER-SMT provides satisfiability proofs for revenue targets, whereas heuristic pruning can omit profitable paths.DEFIPOSER-ARB greedily extracts revenue as opportunities arise, while DEFIPOSER-SMT does not merge paths.
  • Limitations: State-level analysis may miss profitable trades because DeFi state can change multiple times within one blockchain block.The study changes state only when a new block is mined and leaves transaction-level analysis for future work.
  • Limitations: Combinatorial path explosion and sequential graph updates limit real-time capability, especially with multiple or long negative cycles.Heuristics reduce the path space, but negative-cycle detection must precede parameter search and the graph must be updated after each strategy.
  • Limitations: Manual SMT modeling increases code complexity and can introduce solution inaccuracies, requiring validation through concrete execution.DEFIPOSER-ARB instead treats underlying smart contracts and exchange protocols as a black box using spot prices.
  • Limitations: Reported revenue is approximate because the evaluation uses historical states, excludes trades below 0.10 ETH, and models only one trader.Competing traders could divide total revenue, while omitted low-value trades may reduce the estimated financial gain.

A. DEFIPOSER-ARB

DEFIPOSER-ARB models DeFi markets as a graph, extracts profitable negative cycles, and validates discovered strategies through concrete execution. Across 150 days, it generated substantial revenue with low capital requirements, although analysis can exceed the real-time limit when combining many cycles.

  • Graph construction and cycle discovery: DEFIPOSER-ARB represents assets and markets as a directed graph and extracts arbitrage opportunities by identifying negative cycles.Edge weights derive from the highest available market price, after which arbitrage revenue is greedily extracted from detected cycles.
  • Path pruning: Heuristics reduced the impractical action space by at least 99.98% per path length, leaving 600 paths, with 77.67% containing four actions.Paths longer than five actions failed the heuristics despite no explicit maximum-action constraint.
  • Capital requirements: The tools required less than 1.00 ETH (400 USD) with flash loans, compared with mostly less than 150 ETH (60,000 USD) when traders supplied the base asset.Only a small number of strategies exceeded the higher capital thresholds without flash loans.
  • Revenue and validation: 1,552.32 ETH (620,928 USD) was validated for DEFIPOSER-SMT, while DEFIPOSER-ARB generated 191.48 ETH (76,592 USD) in average weekly revenue.Concrete execution validated DEFIPOSER-SMT revenue and estimated weekly revenue for both tools.
  • Performance limits: Average analysis time was 6.43 seconds for DEFIPOSER-ARB and 5.39 seconds for DEFIPOSER-SMT per new block, but DEFIPOSER-ARB exceeded its 10.5-second limit beyond six cycles.The cycle count increases the likelihood that DEFIPOSER-ARB misses the most profitable opportunity.

VII. PROFITABLE TRANSACTIONS AND BLOCKCHAIN SECURITY

The paper connects profitable DeFi transactions to blockchain-consensus risks by analyzing the bZx opportunity and modeling when miners rationally fork to capture MEV. The results show that large opportunities can greatly exceed block rewards and cross the modeled fork threshold.

  • The bZx opportunity: DEFIPOSER-SMT identified the bZx economic attack, whose opportunity window lasted 69 days and reached 916,408 USD approximately one day before exploitation.The replay extended the model with borrowing and shorting actions to analyze the historical opportunity.
  • MEV and block rewards: The bZx opportunity exceeded the average Ethereum block reward by 874×, while other validated DEFIPOSER-ARB and DEFIPOSER-SMT strategies exceeded it by 31× and 8.5×.These comparisons motivate treating profitable DeFi trades as potential consensus-security risks.
  • MEV threat model: The model treats an MEV opportunity as analogous to a double-spending opportunity because an adversary may need to outrun the honest chain with a private fork.The miner decides whether to begin mining privately after an honest miner captures the opportunity.
  • Operational constraints: The analysis time for most strategies remained below the 13.5 ± 0.12-second Ethereum block time, while DEFIPOSER-ARB became too slow when exploiting more than six cycles.The latter condition exceeds the estimated 10.5-second limit after accounting for network propagation.
  • Fork threshold: For Ethereum with a 5.72% stale-block rate, a miner controlling 10% of hash power would fork when an MEV opportunity exceeded four block rewards.The threshold comes from optimal adversarial strategies in the modeled Markov Decision Process.

VIII. RELATED WORK

The related work spans DeFi security, transaction-ordering opportunities, smart-contract vulnerability discovery, and model checking. The paper positions its contribution as automated composability analysis that also quantifies revenue and consensus implications.

  • Existing security research: Prior literature studies blockchain front-running, transaction ordering, market manipulation, and vulnerabilities such as re-entrancy, unhandled exceptions, locked ether, and overflow.These works provide security context but do not cover the paper’s composability analysis claim.
  • Research gap: The paper claims to be the first analysis tool to consider composability analysis across intertwined DeFi protocols.This distinguishes the work from prior studies of traditional smart-contract vulnerabilities and other DeFi security issues.
  • Positioned contribution: The paper presents DEFIPOSER-ARB for arbitrage and DEFIPOSER-SMT for acyclic opportunities, evaluated over 150 days with 96 actions and 25 assets.The reported average weekly revenues were 191.48 ETH for DEFIPOSER-ARB and 72.44 ETH for DEFIPOSER-SMT.
  • Practicality: The tools averaged 6.43 and 5.39 seconds per block and generally required less than 150 ETH without flash loans or less than 1 ETH with them.These results support the paper’s claim that the approaches can operate in real time on sufficiently fast blockchains.
  • Consensus implications: The paper reports that a 10% Ethereum miner would fork above four block rewards, while the bZx opportunity reached 874× the block reward.It frames this contrast as tension between revenue extraction and blockchain security.

APPENDIX A SUMMARY OF THE ERC-20 CRYPTOCURRENCY ASSETS

The appendix describes the supported DeFi assets and actions, then explains how simple multi-action strategies are encoded as state transitions for SMT solving.

  • ERC-20 assets: The asset summary reports that holder and market counts generally increase with transfer-transaction counts for most assets.
  • 96 supported DeFi actions cover exchanges and MakerDAO conversions, with all considered assets trading on Uniswap and Bancor.
  • SMT encoding: A two-action example converts c1 to c2 and then back to c1 through distinct constant-product markets.Using another market avoids reversing the first conversion, which would otherwise produce a zero-sum result before transaction fees.
  • SMT encoding: The encoding represents initial balances and platform states, then applies predicates for sequential state transitions.The first transition converts c1 to c2, while the second converts c2 back to c1.

Objective encoding:

The objective encoding constrains SMT variables to feasible action amounts and searches for revenue targets that increase the trader’s portfolio value.

  • Objective encoding: The revenue target Z is optimized by repeatedly solving the SMT problem with different concrete target values.
  • Objective encoding: For an arbitrary path of length n, the SMT system uses n action-parameter variables bounded by the trader’s cryptocurrency holdings.
  • Objective encoding: The SMT formulation verifies whether free-variable initializations satisfy the combined state, transition, and revenue constraints.
  • Path pruning: Dependency-based state reduction leaves fewer than 100 state-changing paths in 32.71% of evaluated blocks.This reduction lowers the amount of SMT computation required for those blocks.
  • State pruning: The Uniswap DAI market has the highest state-change frequency at 27.01% of blocks, while most markets remain below 2%.

APPENDIX D Z3 PATH PRUNING

The appendix illustrates SMT path construction with a Bancor-to-Uniswap arbitrage and records how market activity determines the relevant state transitions.

  • State pruning: The Uniswap DAI market changes in 27.01% of blocks, whereas 78.72% of markets change in fewer than 2% of blocks.Only 48 of the 600 retained strategies involve the Uniswap DAI market.
  • Running example: The example arbitrage converts ETH to BNT on Bancor and then converts BNT back to ETH on Uniswap at block 9,680,000.
  • Initial state and actions: The SMT encoding initializes both the trader’s balances and the underlying platform states before applying the two transitions.
  • Action encoding: The first transition parameter P1 controls ETH-to-BNT conversion on Bancor and updates the trader and Bancor state.
  • Action encoding: The second transition parameter P2 controls BNT-to-ETH conversion on Uniswap after requiring sufficient BNT and updates Uniswap state.

C. Objective encoding

The objective encoding tests whether a path can achieve a target revenue and uses binary search to maximize the satisfiable revenue, while the appendix visualizes market activity and the bZx attack window.

  • Objective encoding: The example checks whether the two-action path can produce 1 ETH of revenue, encoded as a final ETH balance at least 1001 ETH.
  • Objective encoding: The SMT solver maximizes a path’s revenue through binary search over satisfiable revenue targets.The procedure first checks whether the minimum target is satisfiable, then searches between lower and upper revenue bounds.
  • State-change analysis: Over 950,000 blocks, ETH accounts for 36.76% of state changes, followed by DAI at 14.62%, while POA20 has 0.08%.
  • bZx attack window: The bZx attack opportunity began at block 9,069,000 and lasted 69 days until exploitation at block 9,484,687.The analysis compares solver profits with concrete validation and tracks strategy success rates across 100-block bins.
Loading 2103.02228v1…