DeFiPoser landing

Fuzzing Smart Contracts the Other Way

DeFiPoser aka as DeFi( Com)Poser

How to compose DeFi transactions to extract value? We've tried that with both, the Bellman Ford Algorithm and an SMT solver. While BF seems quite good at arbitrage, SMT can find attacks that involve more complicated actions than swaps only. IEEE Security & Privacy paper.

We explore two methods for creating profitable DeFi transactions: DefiPoser-ARB, aimed at arbitrage opportunities, and DefiPoser-SMT, designed for more complex transactions, demonstrating potential average weekly revenues of 191.48 ETH and 72.44 ETH, respectively. We also discuss the impact of these trades on blockchain consensus, highlighting the risk of blockchain forks and the incentive for miners to engage in such forks if the profit exceeds a certain threshold.

  • DefiPoser-ARB We build a directed DeFi market graph and identify negative cycles with the BellmanFord-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-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 Z3 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).
  • Miner Extractable Value (MEV) and Security 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% will fork the blockchain if an MEV opportunity exceeds 4 times the block reward and the miner failed to claim the source of MEV.

Our system model features a blockchain infrastructure supporting financial cryptocurrency assets, such as coins or tokens. These assets are utilized on Decentralized Finance (DeFi) platforms, including exchanges, and lending and borrowing services. Each DeFi platform provides various actions that can be initiated through transactions. These actions typically process an asset to produce another type of asset as output. It is possible to bundle multiple actions into a single transaction, allowing for their atomic execution in a predetermined sequence. We define a "path" as a series of actions spread across different DeFi platforms. A "strategy," as illustrated in Figure 2 in the paper, refers to a path that includes specific parameters for each action, like the amounts of coins involved. The state of a DeFi market is considered changed when an action alters the asset balance within the market.

In our framework, we conceptualize a trader, denoted as T, who is computationally limited but capable of conducting transactions across various DeFi platforms. The trader's access to cryptocurrency assets is constrained by the liquidity present in public flash loan pools. Although the trader can access blockchain data, they are not equipped to see unverified transactions on the network layer. We posit that the trader can strategically place transactions to be processed before others in upcoming blockchain blocks by paying higher transaction fees, given that transactions are typically prioritized based on gas prices. We operate under the assumption that the trader does not engage in collusion with miners, though exploring such a scenario could be an intriguing direction for future research. The model assumes that the trader interacts with the most recently mined and valid block on the blockchain. For the sake of simplicity, our model does not delve into the complexities arising from potential blockchain forks.


We introduced and evaluated two groundbreaking approaches, DeFiPoser-ARB and DeFiPoser-SMT, which offer practical solutions for revenue extraction within the dynamic and complex domain of Decentralized Finance. Through rigorous testing over a period of 150 days involving 96 DeFi actions and 25 cryptocurrency assets, these techniques have proven to be not only effective in generating substantial weekly revenue but also efficient in their operation, demonstrating their applicability to real-time blockchain environments.