PaperlayerView exact revision on arXiv

Source-linked AI summary

On Identifying Sound Conditions for Frontrunning Resistance

Sebastian Holler, Anna Piscitelli, Jannik Albrecht, Stephan Dübler, Ghassan Karame, Clara Schneidewind

arXiv:2609.11535v1cs.CR

TL;DR

Existing frontrunning criteria lack a precise formal account and miss many audited vulnerabilities. This paper defines Deckstacking Resistance around honest-user interactions, synthesizes sufficient secure interaction conditions, and validates a prototype on real-world contracts.

  • Problem

    Existing frontrunning notions are heuristic or restricted, and 55% of 393 audited vulnerabilities fall outside criteria requiring immediate attacks with monetary goals.

  • Method

    The paper introduces a simulation-based definition of Deckstacking Resistance and an algorithm that computes sound interaction conditions from contract code.

  • Results

    The prototype was validated against a benchmark of real-world smart contracts, identifying two fixes that remained susceptible to frontrunning attacks.

  • Takeaways & Limitations

    Frontrunning resistance depends on both contract code and honest-user interaction strategies, rather than on contract code alone.

  • Takeaways & Limitations

    The existing MEV definition covers immediate attacks completed within the attacker’s transaction-scheduling window, not attacks whose effects emerge later.

Abstract

from arXiv · show

Blockchains enable decentralized applications through smart contracts---interactive programs executed through consensus. However, the inherently asynchronous nature of blockchain transaction ordering introduces a class of vulnerabilities known as frontrunning attacks, which have caused millions of dollars in losses in major blockchains, such as Ethereum. Frontrunning attacks arise because users interact with smart contracts through transactions, which are added to the blockchain by designated nodes called miners. Miners can exploit their ability to reorder, delay, or insert transactions to gain an advantage over honest users, effectively frontrunning them. Yet, to date, the field lacks a rigorous definition of what it even means for a contract to resist such attacks. Worse, we show that existing dynamic detection approaches are fundamentally inadequate: in a large-scale study comprising 287 smart contract audits, 55% of the 393 reported vulnerabilities identified by leading smart contract auditors fall outside the scope of state-of-the-art detection criteria. To address this gap, we propose the first formal definition of frontrunning vulnerability for smart contracts. Our definition captures a key insight: resistance to frontrunning is not an intrinsic property of a contract alone, but depends critically on how honest users interact with it. Grounded in this observation, we develop a sound algorithm for synthesizing secure interaction conditions, alongside a prototype implementation that we apply to audited real-world contracts---revealing previously undiscovered vulnerabilities in two Ethereum contracts.

1 Introduction

Smart contracts face frontrunning because miners can inspect and manipulate transaction ordering, while existing criteria incompletely characterize such attacks. The paper formalizes frontrunning resistance around honest-user interactions, synthesizes secure interaction conditions, and evaluates the approach on real-world contracts.

  • Problem: Miners can inspect mempool transactions and manipulate execution order, enabling targeted attacks such as exploiting exchange slippage or preventing user actions.These capabilities arise because contract-invocation results take effect only after transactions are appended to the ledger.
  • Existing limitations: Existing notions are inadequate because TOD is too broad, whereas MEV captures only attacks producing immediate monetary gains.TOD is a prerequisite for frontrunning attacks but also occurs benignly in realistic contracts.
  • Existing limitations: 55% of 393 vulnerabilities from 287 audits yielded no immediate financial gain and therefore escaped MEV-based detection.Among these, 61 (28%) were critical or major vulnerabilities.
  • Contributions: The paper defines frontrunning resistance as targeted-interference resistance and makes it depend on both contract behavior and honest-user interaction strategies.This definition also covers attacks without immediate monetary attacker gains.
  • Contributions: The authors synthesize secure interaction conditions from contract code and prove that strategies respecting them resist interference by frontrunning attackers.A prototype implements the approach and evaluates it on real-world smart contracts, identifying two previously undiscovered vulnerabilities.

2 Critical Gaps in Frontrunning Detection

Existing frontrunning detectors cover only narrow attack classes, while real-world vulnerabilities also include non-monetary and eventual attacks. A review of 287 audits shows substantial gaps and poor performance from leading static tools.

  • 2.1 Background: Frontrunning arises because miners can inspect pending transactions and manipulate their execution order before blockchain finalization.The hash-puzzle example illustrates an attacker learning a submitted solution from the mempool and taking the reward first.
  • 2.2.1 Dynamic Analysis for Frontrunning Attacks: MEV detects only immediate attacks that produce measurable monetary gains from current mempool information.Eventual attacks may materialize only after the attacker’s scheduling window, while denial-of-service attacks may harm users without directly increasing attacker wealth.
  • 2.2.2 Static Analysis for Frontrunning Detection: Transaction order dependence overapproximates frontrunning because many contracts contain benign order-sensitive interactions under intended usage patterns.Static tools refine TOD with heuristics, often prioritizing attacks involving direct financial effects.
  • 2.2.2 Static Analysis for Frontrunning Detection: The audit study manually reviewed 287 publicly available audits from eight companies and constructed datasets for availability and fixes.The datasets included audits with executable Solidity source code for both vulnerabilities and fixes when available.
  • 2.2.3 Evaluating Frontrunning in the Wild: Sailfish failed on 67% of contracts, while Nyx failed on 21% and each tool detected only two vulnerabilities in the remaining evaluations.Neither tool detected eventual-only attacks, and both missed 89% of non-monetary-only attacks.

3 Defining Deckstacking Resistance

The paper defines Deckstacking Resistance as a simulation-based guarantee about whether miner-like interference with honest contract interactions can be reproduced by a restricted ideal-world simulator. The definition is parameterized by honest-user strategies, execution semantics, and an observable-similarity relation.

  • 3.3 Real-World Blockchain Execution: The formal model represents blockchain states, transaction-driven transitions, runs, block scheduling, and symbolic cryptographic interactions.It is designed to support block-based scheduling and transaction-inclusion guarantees while remaining modular across smart-contract execution semantics.
  • 3.2 Overview & Key Insights: Deckstacking Resistance compares real-world executions under a malicious block generator with ideal-world executions produced by a restricted simulator.The real attacker accesses the mempool and can reorder transactions, whereas the ideal simulator maps prior blockchain execution to a block template with restricted knowledge.
  • 3.2 Overview & Key Insights: A single non-adaptive simulator must reproduce every valid honest-user behavior for each real-world attacker.The simulator cannot adapt to the particular user behavior or mempool contents, and corresponding executions must agree on observable behavior.
  • 3.3 Real-World Blockchain Execution: The resistance guarantee depends on both contract code and a set of legitimate honest-user strategies.Users may need to follow restrictions such as using specified time windows or withholding authentication secrets; strategies that avoid the vulnerable interaction may therefore satisfy the guarantee.
  • 3.5 Definition: The definition uses a real-ideal simulation condition in which every attacker execution must have a similar simulator execution.Deckstacking Resistance is stated relative to a strategy set ΣC, with the attacker and simulator separated from honest-user secrets.
  • 3.5 Definition: The chosen similarity relation determines which deviations from ideal behavior are acceptable for a contract.This allows the notion to be instantiated with different smart-contract semantics, equational theories, and application-specific observability criteria.

4 Interaction Condition Generation

The section treats frontrunning resistance as a property of contract–user interaction and synthesizes conditions that make user transactions predictable and attacker-resistant.

  • Overview & Key Insights: Interaction conditions constrain user strategies so contract interactions satisfy DS Resistance against frontrunning and backrunning attackers.The conditions apply to the interplay between a contract and an honest user rather than to contract code alone.
  • Overview & Key Insights: User strategies typically operate in rounds of k blocks, requiring each transaction’s execution result to remain unchanged regardless of adaptive scheduling.The relevant guarantee is that the result stays the same within the next k blocks.
  • Generation Algorithm: For the TimelockedFeeMinted example, staged fee changes ensure execution cannot affect the fee during the current round, even if an attacker schedules a change.The fee change is constrained to impact a later round.
  • Generation Algorithm: The algorithm refines candidate preconditions and invariants until they persist throughout a round and prevent attacker interference with event data dependencies.It analyzes path conditions, data dependencies, attacker writes, and round-invariant strengthening.
  • Soundness Proof: The soundness theorem states that round-based strategies respecting the synthesized conditions can have every attacker run simulated, implying DS Resistance.The theorem assumes scheduling decisions depend only on relevant variables and also accounts for backrunning constraints.

5 Implementation

NODS implements the synthesis algorithm using symbolic execution and static analysis, then evaluates synthesized conditions for soundness and functionality on audited contract pairs.

  • Implementation: NODS synthesizes frontrunning-resistant interaction conditions for all events in smart-contract functions using symbolic execution, dependency analysis, invariant verification, and Z3.The prototype builds on an existing symbolic execution engine and static analysis framework.
  • Implementation: NODS preserves path-condition precision by applying round-invariant strengthening lazily to disjunctive-normal-form literals and retaining the DNF structure during merging.Already invariant literals remain unchanged to avoid over-strengthening.
  • Evaluation: All computed conditions were sound, while 13 of 22 fixed contracts yielded functional conditions.In two other cases, NODS identified remaining vulnerabilities; seven cases produced no satisfiable condition, including four attributed to symbolic-analysis overapproximations.
  • Zero-day Vulnerabilities: NODS exposed a collateral-liquidation vulnerability in which mempool observers could adapt to a supposedly randomized liquidation start and avoid liquidation.Changing the start to a user-defined salt did not prevent an attacker from precomputing the liquidation effect.
  • Zero-day Vulnerabilities: A staking contract remained vulnerable to denial of service because attackers could frontrun createAgent calls, even after a fix restricted the owner parameter.The modified function still allowed malicious users to prevent new agent registration.

6 Related Work

Related work characterizes frontrunning through empirical taxonomies, MEV, and TOD, or mitigates it through ordering and architectural mechanisms, but these approaches do not provide the paper’s formal interaction characterization.

  • Frontrunning Attacks and Mitigations: Prior taxonomies and mitigation studies examine frontrunning empirically without formally characterizing when smart-contract interactions are vulnerable.These works systematize attack methods and defenses rather than defining the underlying security property.
  • Characterizing Frontrunning: MEV measures an attacker’s maximum monetary gain from a mempool and blockchain state, making it unsuitable for attacks without immediate financial profit.The paper’s audit analysis found many reported vulnerabilities outside this criterion.
  • Characterizing Frontrunning: TOD flags order-dependent contract executions but overapproximates frontrunning vulnerability because most stateful contracts contain benign order dependencies.Static tools use TOD as a basis for detecting potential vulnerabilities.
  • Fair Ordering and Architectural-level Mitigations: System-level alternatives pursue weaker fair-ordering guarantees or cryptographic designs that hide transaction contents until inclusion and limit attacker adaptation.Examples include permissioned BFT protocols, encrypted transactions, and verifiable delay functions.

7 Conclusion

The paper introduces Deckstacking Resistance as a formal characterization of frontrunning robustness and shows that existing MEV-based detection misses more than 55% of audited vulnerabilities. It also provides a simulation-based definition tied to user interactions, soundly synthesized interaction conditions, and a real-world prototype evaluation.

  • More than 55% of audited vulnerabilities with confirmed frontrunning are missed by MEV because existing techniques require immediate attacks with monetary goals.The empirical study identifies these restrictions as the main reason MEV fails to capture many reported vulnerabilities.
  • Deckstacking Resistance formally characterizes robustness by comparing unrestricted attacker executions with executions under an attacker that cannot inspect the mempool.The definition makes resistance depend on the interaction between a contract and an honest user, rather than on contract code alone.
  • The paper proposes sound interaction-condition synthesis from contract code and validates a prototype on a benchmark of real-world smart contracts.

Generative AI Usage

The supplied material documents the paper’s use of generative AI in development and its formal modeling choices for blockchain execution, cryptography, secrets, mempools, and scheduling. It also describes the paper’s scope, artifacts, disclosure process, and generality assumptions.

  • ChatGPT and Grammarly were used for grammar editing, while GitHub Copilot aided NODS development through skeleton implementations and interface bindings.Most generated code was replaced with human-written code; Copilot-authored SMT transformation modules were tested and fuzzed.
  • The work studies Ethereum frontrunning vulnerabilities while emphasizing a precise definition, and releases datasets, NODS code, and evaluation results for reproducibility.The authors also disclosed two susceptible fixes to contract owners and auditors and contributed findings to the Enterprise Ethereum Alliance.
  • The formal model represents blockchain configurations, contract calls, block finalization, symbolic cryptography, secrets, mempools, and attacker scheduling strategies.The model supports contract execution over configurations containing wallet states, contract states, and the current block number.
  • The semantics allow different smart-contract languages and avoid fixing a concrete contract layout, while assuming sound and complete symbolic execution.

D Soundness Proof

The paper proves the soundness of its algorithm for synthesizing secure interaction conditions.

  • The proposed algorithm for synthesizing interaction conditions is proved sound.

D.1 Preliminaries

The preliminaries define contract-state notation and observable events, while assuming a symbolic-execution framework for the subsequent soundness proof. They also represent event outputs through dedicated contract variables.

  • Contract configurations use Γ.SC for contract state, XC for contract variables, and FC for contract functions, with state equality restricted to selected variables.
  • Each transaction is assumed to emit at most one observable, represented as an event-variable/value pair.Per-function event variables record emitted values, and changes to those variables produce observables.
  • The soundness development assumes sound and complete symbolic execution for smart contracts.

D.1.1 Symbolic Execution.

The analysis models smart-contract functions with symbolic execution relations that map configurations and transactions to assignments, under soundness, completeness, agreement, and determinism assumptions.

  • Model scope: The model treats the block number as a global variable and assumes other global blockchain variables can be incorporated as attacker-controlled inputs.The paper notes that dependencies on such variables can force synthesis of the unsatisfiable condition ⊥.
  • Symbolic execution model: Symbolic execution maps a concrete configuration and transaction to an assignment over contract and transaction-context variables.The variable domain includes contract globals, the block number, local variables, function arguments, and sender information.
  • Correctness assumptions: Soundness ensures every satisfiable symbolic execution result corresponds to a concrete transition producing the substituted assignment.The condition must be satisfied under the assignment induced by the starting configuration and transaction.
  • Correctness assumptions: Completeness ensures every concrete transaction execution has a corresponding symbolic result whose condition is satisfied and whose substitution matches the resulting configuration.
  • Correctness assumptions: The framework additionally assumes condition agreement and strong determinism so equivalent assignments satisfy conditions consistently and matching paths yield the same expression.The determinism assumption is stronger than semantic determinism alone because syntactically different but equivalent expressions could otherwise be produced.

D.1.2 Dependency Analysis.

Dependency analysis extracts data and control dependencies from symbolic execution, then uses them to characterize variable preservation across executions and rounds.

  • Dependency extraction: Data and control dependencies identify variables that can affect assignments or determine which expressions are selected for contract variables.Control dependencies exclude irrelevant path-condition variables and retain variables pivotal to assignment choices.
  • Dependency soundness: The dependency analysis is sound: executions agreeing on the relevant dependencies produce the same assignments and observables for the tracked variables.This property is established for configurations that agree on the dependency set associated with the tracked variables.
  • Time progress: The tick transaction models time progression by increasing the block number, and its symbolic execution is sound and complete for that semantics.
  • Round-based strategies: Round-based user strategies repeatedly schedule one transaction during each k-block round until it is included or the round ends.This scheduling discipline lets users wait for processing before selecting the next transaction.
  • Round invariants: Block-oblivious invariants remain true after possible function effects within a round, enabling preservation of round invariants across executions.A round invariant requires a beginning-of-round precondition to imply an invariant throughout the round.

D.2.1 Characteristic Properties.

The paper defines frontrunning and backrunning conditions over transactions, configurations, and protected variables, using symbolic dependencies and invariants to characterize attacker interference.

  • Algorithmic characterization: The characteristic properties of the synthesized conditions are established from Algorithm 1 for frontrunning and Algorithm 3 for backrunning.The lemmas rely on the construction of the algorithms together with round-invariant preservation and merging.
  • Semantic conditions: Frontrunning conditions require that attacker transactions cannot alter how an honest transaction writes a protected variable set Z.The corresponding backrunning conditions constrain attacker writes after the honest transaction, including effects on variables changed by that transaction.
  • Combined conditions: The framework combines individual frontrunning and backrunning predicates into requirements that protect selected global variables from both attack directions.The combined predicates inherit their properties from the individual conditions.
  • Write-set reasoning: Write sets record which variables in Z a transaction modifies, supporting preservation and agreement lemmas for variables outside the set and for configurations with matching control dependencies.

D.2.3 Correctness of Frontrunning and Backrunning Conditions.

The semantic conditions prevent attacker reordering from changing protected writes or observables, and their round-level persistence supports a commutativity result for honest and attacker transactions.

  • Frontrunning correctness: The core correctness lemma states that a frontrunning condition prevents an attacker transaction placed before the honest transaction from changing the honest transaction’s behavior on protected variables.Written variables receive the same values, while unchanged variables remain unaffected under the stated conditions.
  • Backrunning correctness: Backrunning correctness ensures that placing an honest transaction before an attacker transaction does not change the attacker’s effect on protected variables.Analogous correctness holds for tick transactions, which model block-number progress.
  • Write-set separation: Frontrunning conditions imply disjointness between variables written by the honest transaction and those an attacker transaction would write in the protected set.
  • Round persistence: The conditions persist throughout a round under executions of tick and attacker transactions, while backrunning conditions also remain invariant through the honest transaction.
  • Commutativity: When the protected set contains event variables and is closed under data and control dependencies, the combined conditions establish commutativity between honest-user and attacker transactions.

D.2.7 Soundness Proof.

The soundness proof establishes that synthesized interaction conditions guarantee DS Resistance for contracts under qualifying round-based user strategies. The argument constructs a simulator run corresponding to every attacker run and concludes resistance for all user strategies satisfying the stated conditions.

  • Soundness Proof: For every attacker run, the proof constructs a simulator run with matching relevant configurations, transaction structure, and run correspondence.The strengthened soundness lemma provides the inductive basis for this construction.
  • Soundness Proof: The inductive proof handles empty and singleton enabled-transaction cases by preserving simulator validity and the required configuration and run relations.The proof distinguishes whether the synthesized predicate holds and whether the enabled transaction set is empty or contains one transaction.
  • Soundness Theorem: Theorem D.48 proves that a contract and any qualifying round-based user strategy satisfy DS Resistance under synthesized interaction conditions.The strategy must be invariant over configurations agreeing on X* and submit at most one transaction when nonempty.
  • Soundness Theorem: The simulator depends only on the attacker and contract, while the user strategy remains arbitrary among strategies satisfying the required conditions.Thus the theorem applies to every set of user strategies whose members satisfy those conditions.

D.3 Relation to TOD

The paper separates freedom from transaction-order dependence from DS Resistance. Even contracts whose functions do not change state can fail DS Resistance for suitable non-round-based user strategies.

  • Relation to TOD: Contracts with non-round-based user strategies can be free of TOD yet fail to satisfy DS Resistance.The example uses functions that do not change contract state, including a no-op and an event-emitting function.
  • Relation to TOD: An adaptive attacker can place the test transaction in the block parity that triggers the user's follow-up transaction, reliably producing Triggered(u).A non-adaptive attacker must use the same block placement and therefore cannot achieve the same behavior for both strategies.
Loading 2609.11535v1…