arXiv CSopen access

On Identifying Sound Conditions for Frontrunning Resistance

arXiv:2609.11535v1 [cs.CR] 10 Sep 2026

On Identifying Sound Conditions for Frontrunning Resistance Sebastian Holler

Anna Piscitelli

Jannik Albrecht

[email protected] MPI-SP Bochum, Germany

[email protected] Ruhr University Bochum Bochum, Germany

[email protected] Ruhr University Bochum Bochum, Germany

Stephan Dübler

Ghassan Karame

Clara Schneidewind

[email protected] MPI-SP Bochum, Germany

[email protected] Ruhr University Bochum Bochum, Germany

[email protected] MPI-SP Bochum, Germany

Abstract 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 realworld contracts—revealing previously undiscovered vulnerabilities in two Ethereum contracts.

CCS Concepts • Security and privacy → Formal security models; Distributed systems security.

Keywords MEV, Frontrunning resistance, Transaction Order Dependence

1

Introduction

Blockchains allow mutually mistrusting entities to jointly maintain a fairly evolving and tamper-resistant ledger of transactions. To extend the ledger, a designated set of nodes, so-called miners, verifies user transactions from a public mempool and include them in blocks that are later appended to the ledger. This mechanism not only supports financial transactions but also the execution of smart contracts; these are (stateful) programs that can manage the

transfer of funds according to some contract code that is invoked on the ledger. Smart contracts give rise to a rich environment for deploying decentralized financial applications (often referred to as DeFi), encompassing lending platforms, currency exchanges, or decentralized autonomous organizations. Although smart contracts enable powerful deployment of such applications, they differ significantly from conventional program execution models, creating opportunities for so-called frontrunning attacks. In particular, since the results of contract invocations only come into effect once the corresponding transaction is appended to the ledger, miners have an unprecedented advantage in inspecting transactions in the mempool and manipulating their execution order [4, 14, 18, 30, 37, 41]. Many real-world incidents show that miners can easily take advantage of slippage opportunities in currency exchanges in a targeted manner [4, 42] or prevent unwanted user actions on demand by outrunning them with speciallycrafted transactions when observing their publication [11, 18]. For instance, Qin et al. [35] report losses of $540.54M over 32 months (Dec 2018–Aug 2021) solely due to arbitrage attacks. Interestingly, despite the prevalence of frontrunning attacks, as of today, there exists no precise formal understanding of when a smart contract is susceptible to such attacks. Several works observed a connection between frontrunning attacks and concurrency bugs, resulting in the notion of transaction order dependence (short TOD). Intuitively, TOD deems contracts vulnerable whose concurrent execution does not safely commute. While TOD is a prerequisite for the existence of frontrunning attacks, almost all realistic smart contracts exhibit benign instances of TOD, making TOD an insufficient criterion for identifying frontrunning vulnerabilities. Several practical works [10, 39] tried to narrow down TOD to identify exploitable instances, but all such attempts are of purely heuristic nature and turn out to be neither sound nor complete. Complementing these attempts towards the static identification of frontrunning vulnerabilities, there exist monitoring approaches that aim to dynamically detect frontrunning attacks. Here, the commonly used criterion to identify frontrunning attacks is the notion of maximal-extractable value [4, 14] (short MEV ). MEV aims to quantify the maximum financial profit that a frontrunning adversary could make when being confronted with a specific set of user transactions to be scheduled. If an attacker has a positive MEV, this indicates an attacker’s ability to carry out a profitable frontrunning attack. This approach, thus, has the advantage of identifying concrete attacks, but disregards a large class of frontrunning attacks

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

TOD

MEV Eventual

Immediate

Our Definition

NonMonetary

Figure 1: Our definition establishes a strong tradeoff between the narrow focus of MEV on monetary and immediate attacks and the too broad notion of TOD. The outer dashed area represents possible benign instances, while the inner gray region indicates where frontrunning attacks are possible.

that do not yield an immediate financial gain for the attacker. Indeed, in a large-scale analysis of 287 smart contract audits conducted by top auditing companies, we found that 55% of the 393 reported vulnerabilities do not yield an immediate financial gain for the attacker and, thus, cannot be captured by MEV (among those, 61 (28%) are critical or major vulnerabilities). These findings reveal a significant gap in current approaches used to characterize a contract’s susceptibility to frontrunning attacks. Motivated by these findings, we set forth in this work to develop the first definition that precisely characterizes when a smart contract is robust against frontrunning attacks. We base our definition on the key observation that frontrunning attacks constitute a malicious interference of an attacker with the way that an honest user interacts with a contract. Consequently, a contract’s resistance to frontrunning attacks cannot be solely determined by the contract code alone, but needs to consider the nature of user interactions. Following this insight, we propose a simulation-based definition of frontrunning resistance that is formulated w.r.t. a contract and the interaction strategy of an honest user. Based on this definition, we then develop an algorithm to synthesize secure interaction conditions that formulate requirements on the user strategy to provably evade frontrunning attacks. In summary, we make the following contributions: Empirical Analysis of Frontrunning Attacks: We study a realworld data set of frontrunning vulnerabilities reported in professional smart contract audits and analyze shortcomings of existing notions to capture these attacks. In particular, we show that existing frameworks cannot capture a significant fraction of reported frontrunning instances by top auditors (cf. Section 2). Novel Definition: We introduce a new formal definition that captures frontrunning resistance as an attacker’s inability to interfere in a targeted manner with the interactions between honest users and smart contracts (cf. Section 3). This definition addresses the shortcomings of the coarse notion of TOD by formally characterizing those scenarios where an attacker with mining capabilities can exploit TOD to purposefully cause interferences with honest user transactions. At the same time, the definition is (as opposed to MEV) general enough to also capture such frontrunning attacks that do not result in immediate monetary attacker gains (cf. Figure 1).

Synthesis of Interaction Conditions: We devise an algorithm to automatically synthesize secure interaction conditions based on the code of a smart contract. We show that user strategies that respect those conditions are provably robust against the interference of a frontrunning attacker (cf. Section 4). Tool Implementation and Evaluation: We implement our approach in a prototype tool and evaluate it on a benchmark of real-world smart contracts (cf. Section 5). In the course of the evaluation, we identified two fixes implemented in response to audit reports to remain susceptible to frontrunning attacks. We responsibly disclosed these findings to the contract owners and the audit companies. We additionally disclosed our results to the Enterprise Ethereum Alliance, resulting in an adjustment of their vulnerability classification in the EEA EthTrust Security Levels Specification [3]. All the code and data of the prototype is available on GitHub [23].

2 Critical Gaps in Frontrunning Detection 2.1 Background Frontrunning attacks pose a significant threat to the fairness and security of smart-contract-based applications. These attacks are enabled due to the specific execution model of smart contracts on public blockchains, which allows adversaries to observe and manipulate pending user transactions before they are finalized on the blockchain. While the considerations in this paper apply to various blockchain platforms, we focus in the following on Ethereum as it is the most widely used platform for smart contracts. Ethereum Smart Contracts. Ethereum smart contracts are written in a high-level language before being compiled into a bytecode representation that is run on the Ethereum blockchain. For simplicity, all examples in this paper are given in the high-level language Solidity. Solidity is a Java-like programming language featuring contracts (instead of classes). We show an example of a Solidity smart contract implementing a hash puzzle in Figure 2. This smart contract is initialized with a challenge, i.e., a hash value, and allows accounts to propose a solution to this challenge by calling the submit function. When submitting a valid solution that is the preimage of the challenge for the first time, the calling account (accessed via msg .sender) is rewarded. This is enforced by the require(...) statement in line 5, which checks that the challenge condition sha256(solution) == challenge is met and reverts the transaction execution otherwise. Frontrunning Attacks. The HashPuzzle contract (cf. Figure 2) is vulnerable to a frontrunning attack: Suppose a user finds the solution to the challenge and submits a corresponding submit(solution) transaction to redeem the reward. Transactions submitted for inclusion in the blockchain enter the mempool. Miners collect the transactions of network users and group them into blocks that extend the blockchain. Hence, an adversarial miner with access to the mempool learns the solution in the honest user transaction before this transaction gets included in the blockchain. Instead, the miner can craft their own submit(solution) transaction and place it in front of the honest user transaction when creating a block. Thus, the adversary will get rewarded for solving the puzzle while the original user who submitted the solution loses their rightful reward.

On Identifying Sound Conditions for Frontrunning Resistance

1 2 3 4 5 6

contract HashPuzzle { bytes challenge ; function submit ( bytes solution ) { require ( sha256 ( solution ) == challenge ); payable ( msg . sender ). transfer ( this . balance );

} // ...

Figure 2: Hash-puzzle contract vulnerable to frontrunning. 1 2 3 4 5 6

contract ProposeVoting is Voting { mapping ( Id => Proposal ) proposals ; function proposeCandidate ( Id id , Proposal prop ){ require ( proposals [ id ] == null ); proposals [ id ] = prop ; } // ...

Figure 3: Voting contract vulnerable to denial-of-service frontrunning attacks.

2.2

Why Static and Dynamic Frontrunning Detection Falls Short

Despite the absence of a precise formal definition of frontrunning vulnerabilities, various approaches have been proposed to detect such vulnerabilities in smart contracts, both statically (based on the contract code) and dynamically (monitoring the blockchain and the mempool). In the following, we analyze the shortcomings of these approaches, starting with dynamic analysis, as these are particularly evident in the case of frontrunning. 2.2.1 Dynamic Analysis for Frontrunning Attacks. A prominent line of work towards dynamic frontrunning detection centers around the notion of Maximal-Extractable Value (MEV) [14]. MEV quantifies the monetary gain for a frontrunning attacker who inspects the current mempool and the blockchain state. In practice, MEV is the basis for the implementation of so-called MEV bots [4, 40], network nodes that monitor the mempool to identify profitable arbitrage and sandwiching opportunities and then bribe miners to enforce their determined order of execution. Formally, MEV is defined as the maximum personal gain that a blockchain participant can obtain by reordering future transactions at a given point in time, provided a concrete mempool [4]. While MEV is effective in characterizing specific profitable attack opportunities, it is only designed to detect attacks with the following characteristics: (1) the adversary’s goal needs to be of monetary nature and measurable as an increase in the attacker’s wealth, and (2) attacks need to be immediate, meaning that an attacker can mount the attack using only the information from the current mempool to create a (limited) sequence of blocks that meets the attack goal. (Non-)Monetary Attacks. MEV identifies quantifiable attacks by measuring value changes in user-owned tokens. However, not all frontrunning attacks incur direct financial gains for an attacker. For example, adversaries can have (personal) incentives to harm specific users even without causing state changes that provide them with benefits. Namely, frontrunning can be used to provoke user- and smart-contract-specific denial-of-service attacks. Such attacks can lead to significant harm, including monetary loss or permanent disincentives for the use of a service. Figure 3 showcases

the candidate proposal functionality of an e-voting contract that is vulnerable to such a DoS-Frontrunning attack. Here, an attacker can prevent a new candidate from being proposed by frontrunning every proposeCandidate call with their own call that uses the same identifier. The attacker call will reserve the candidate identifier id for a dummy proposal, thereby causing the intentionally user-proposed candidate to be dropped. Any re-submission of the candidate with a new identifier could be frontrun again by an attacker monitoring the mempool, continuously preventing specific candidate proposals. Immediate vs. Eventual Attacks. The definition of MEV is inherently immediate in that it identifies attacks that (1) can be completed within the transaction scheduling window, under the control of the attacker, and (2) use transactions from the current mempool or such transactions that the attacker can craft independently. However, some frontrunning attacks may have effects that are only observable after the attacker’s scheduling window, e.g., because they incur a state change that becomes exploitable only in later phases of contract execution. For instance, consider a voting contract in which a frontrunning attacker manipulates the voting settings (e.g., the maximum number of votes a user can cast) to their advantage during the voting phase. The possible effects of such an attack (e.g., winning the election and receiving a payout) may only materialize after the voting phase ends, which could fall outside the attacker’s scheduling window. Such non-immediate attacks lie outside the scope of MEV, and we refer to them as eventual attacks. 2.2.2 Static Analysis for Frontrunning Detection. Approaches to the static analysis of frontrunning vulnerabilities center on the notion of transaction order dependence (TOD), which was first introduced and discussed as a potential source of vulnerabilities in [28]. A smart contract exhibits TOD if the execution order of different contractinvoking transactions can lead to different contract states. In practice, most smart contracts exhibit some form of TOD, since contracts usually maintain state that can be updated by multiple users. TOD coarsely overapproximates the existence of frontrunning vulnerabilities by flagging all contracts that could have conflicting transactions—even if the concurrent execution of those transactions can be avoided when users respect the intended contract usage patterns [10]. To account for this imprecision, current works refer to the original notion of TOD as generalized TOD (G-TOD) or event ordering (EO) bugs and try to apply heuristics to identify exploitable fragments of TOD, e.g., by focusing on concurrency bugs that directly affect the flow of Ether [10, 39]. These heuristics are not formally defined but only evaluated empirically using tools aimed at identifying vulnerabilities that are immediately exploitable for monetary profit—the most recent tools being Sailfish [10] and Nyx [39]. To detect TOD bugs, Sailfish identifies read-write hazards (conflicting read/write accesses to the same variables) in smart contracts that indicate G-TOD bugs. G-TOD bug candidates are then narrowed down to (potential) TOD bugs by applying heuristics to decide whether they can be exploited by a frontrunning attacker to influence a money transfer. Similarly, [39] presents the tool Nyx, which focuses on detecting exploitable (G-)TOD bugs. A (G-)TOD bug is considered exploitable if reordering the invocations of two contract functions increases the profit of one specific user (the attacker) and decreases that of another (the victim).

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

Auditor Trail of Bits ConsenSys Diligence Nethermind Runtime Verification HashEx OpenZeppelin Hacken Quantstamp

#𝐷 full 81 79 11 20 35 65 37 65

#𝐷 avail 2 11 4 0 0 6 0 1

#𝐷 fixes 2 11 4 0 0 6 0 1

Total

393

24

24

Table 1: Overview of our datasets comprised of 287 publicly available smart contract audits by 8 auditors.

Nyx [39] and Sailfish [10] implement this static contract analysis to detect arbitrage and sandwiching opportunities before contract deployment. In this way, they purposefully target monetary frontrunning vulnerabilities to increase analysis precision. However, we observe that the analysis underlying those tools additionally disregards eventual (monetary) frontrunning attacks. Nyx and Sailfish both implement a symbolic validation phase, which verifies that an attack trace candidate (indicating a possible (G-)TOD bug) is indeed executable. Such attack trace candidates consist of two potentially interfering function calls (f1, f2 ), out of which at least one (f2 ) needs to have a direct financial implication (e.g., trigger a money transfer). The validation step then checks that f1 and f2 can be executed consecutively (enabling the critical interference). However, triggering an eventual attack requires the non-consecutive execution of f1 and f2 , e.g., executions in different blocks or such that are separated by other function invocations. 2.2.3 Evaluating Frontrunning in the Wild. To verify the prevalence of the aforementioned attack types, we manually reviewed 287 publicly available professional smart contract audits based on the auditors listed by the Ethereum Foundation [2]. In particular, in our dataset 𝐷 full , we chose the top eight smart contract audit companies with the least number of exploited projects according to the “rekt.news” leaderboard [1]. Subsequently, we analyzed all audits that were publicly accessible and filtered out those that were not related to frontrunning vulnerabilities. Additionally, we curated datasets 𝐷 avail and 𝐷 fixes with executable smart contracts including all those audits where complete Solidity source code is available for both the vulnerability and the fix (𝐷 full ⊇ 𝐷 avail ∼ 𝐷 fixes ), i.e., for each vulnerable audit in 𝐷 avail there is an implemented fix in 𝐷 fixes , and the fixes were seeking to completely repair the described frontrunning vulnerability. Based on 𝐷 full , there were a total of 393 frontrunning vulnerabilities identified by the auditors in question within the analyzed 287 contracts. Of these, 24 vulnerabilities fall in the category of 𝐷 avail and 𝐷 fixes . From the vulnerability descriptions in the audits, we collected attack traces and the exploitable function pairs involved in the attack for further analysis. Additionally, we tagged those vulnerabilities that are non-monetary or eventual. Table 1 provides an overview of our three datasets. Evaluating Static Frontrunning Analysis. To validate our observation on static frontrunning analysis, we ran Nyx and Sailfish

on each vulnerability in 𝐷 avail using the flattened version of the contract, with all contract dependencies included in a single Solidity file that can be statically compiled. We checked whether the exploitable function pair reported in the audit is flagged as vulnerable by the respective tool. Unfortunately, as already hinted in [39], Sailfish’s real-world performance is limited, resulting in execution errors on 67% of the contracts in the dataset. In the remaining portion, Sailfish detected only two vulnerabilities. Nyx failed in considerably fewer cases (21%), but detected only two out of all frontrunning vulnerabilities in 𝐷 avail . In particular, Nyx and Sailfish did not detect any eventual-only attacks, and both failed to detect 89% of non-monetary-only frontrunning attacks. To cross-validate the evaluation results, we ran both tools on 𝐷 fixes to understand their performance on secure contracts. Interestingly, of the 24 fixed contracts, most cases in which a tool correctly labeled a fixed contract as “safe” were those in which the same tool had already misclassified the corresponding vulnerable contract as secure (four instances for Sailfish and 16 for Nyx). Across both tools, only a single contract was correctly classified at both stages: identified as “vulnerable” before the fix and “safe” after it, and this was achieved by Sailfish alone. Evaluating Dynamic Frontrunning Analysis. Lastly, for all 393 frontrunning vulnerabilities in 𝐷 full , we manually applied the MEV definition to the attack traces reported in the audits. We aimed to verify whether the adversary could effectively earn monetary rewards by exploiting the vulnerability. In case MEV was not applicable to the particular vulnerability, we analyzed whether this was due to non-monetary, eventual, or other possible limitations of the MEV definition. Our MEV analysis results on dataset 𝐷 full confirm that the limitations of qualifying frontrunning attacks using MEV are not only theoretical but also affect a significant number of real-world contracts. In particular, (a) among the 393 vulnerabilities, a total of 217 (55.2%) could not be captured by MEV, (b) 18.6% (21.9%) of the vulnerabilities could not be captured by MEV because they are eventual (non-monetary) only, while 14.8% of the vulnerabilities could not be captured by MEV because they are both eventual and non-monetary, and (c) no other limitations (besides eventual and non-monetary vulnerabilities) hindered MEV’s applicability. A summary of these results (and the corresponding severity rating by the respective auditors) is shown in Figure 4.

3

Defining Deckstacking Resistance

Informed by our empirical analysis, we make the following observation: Smart contracts usually play the role of a trusted party that mediates a protocol between multiple mutually distrusting users. Consequently, frontrunning attacks constitute an interference of an attacker with the interaction of a user with this trusted party. Following this intuition, we will set forth a simulation-based security notion similar to security definitions for cryptographic protocols to characterize that user-contract interactions should be ideal. We will

On Identifying Sound Conditions for Frontrunning Resistance

Critical High / Major Medium Low / Minor Not Specified

50% 40% 30% 20% 10% 0%

Total

Eventual

Non-monetary

Eventual and Non-monetary

Figure 4: Summary of the vulnerabilities not captured by MEV due to their eventual or non-monetary nature (in 𝐷 full ). call this notion Deckstacking Resistance (short DS Resistance) accounting for the fact that attackers with miner-like capabilities can not only harm user-contract interactions by literally frontrunning honest user transactions but can also manipulate transaction execution in multiple ways, similar to how a cheating user in a card game may peek into the card deck, drop cards, insert cards, or reorder the entire deck in their favor (so ‘stacking the deck’).

3.1

Blockchain Model

We base our definition on a formal model of smart contract execution. Our model combines and extends concepts from [6], which gives a computationally sound model for executing Bitcoin-based smart contracts, and [7], which defines a core calculus for Solidity. We lift the blockchain execution model from [6] to support block-based scheduling and transaction inclusion time guarantees. Modeling Transactions. To model the blockchain state, we assume a set of blockchain users Hon and a set of contracts where every contract C has a contract state S that maps every variable that occurs in C to its current value. We model the evolution of blockchain states with a transition system on configurations Γ where a configuration describes the current snapshot of the blockchain state. Configurations can be advanced with transactions tx whose execution impacts the states of users and contracts. To capture the effects of executing a transaction tx (which may involve multiple asset tx

transfers or the logging of different events), each transition Γ0 −−→ Γ1 𝑥𝑠

emits a list of observables 𝑥𝑠 and we call a sequence of (valid) state tx0 tx𝑛−1 tx1 transitions Γ0 −−→ Γ1 −−→ · · · −−−−→ Γ𝑛 a run (also denoted by 𝑅). 𝑥𝑠 0

𝑥𝑠 1

Illustrative Example. Consider the example of DoS-frontrunning depicted in Figure 3. To carry out the attack, the attacker observes the call proposeCandidate(Id, Candidate)u by honest user u in the mempool P1 and outruns it with their own transaction, copying the single-use candidate identifier Id.

𝑥𝑠𝑛−1

Since our transaction framework is modular to the exact smart contract execution semantics, it can be instantiated for different formal smart contract languages such as [21, 24, 29]. Additional details about the blockchain model and accompanying formalizations for the following technical subsections on the definition of Deckstacking Resistance are given in Appendix C.

3.2

the (secure) protocol execution. To prove the security of a protocol with respect to such a simulation-based security notion, one needs to construct for each real-world adversary a corresponding idealworld simulator that produces an output in the ideal world that is indistinguishable from the one that would have been produced in the real world. In this way, it is guaranteed that all executions possible in the real world can be mapped to some behavior in the ideal world (which is deemed unproblematic by definition). We adopt this real-ideal paradigm to define DS Resistance of a contract C by contrasting the executions of C in a real world where the attacker is assumed to be a malicious block generator (a.k.a. miner) with full access to the mempool and full reordering capabilities with executions of C in an ideal world where the simulator has restricted knowledge and capabilities to append blocks. We write 𝐴 to refer to the real-world block generator (also called attacker 𝐴), and 𝑆 for the ideal-world block generator (simulator 𝑆). In our model, a real-world block generator 𝐴 is a function that maps a mempool P = [𝑡𝑥 1P , . . . , 𝑡𝑥𝑚P ] of unprocessed transactions and a run 𝑅0 to a valid sequence [tx0, tx1, . . . , tx𝑛−1 ] of blockchain transactions (a block). Transactions within the block are either chosen from P or crafted by the block generator (for better readability, we denote such transactions in the following with tx𝑖𝐴 or tx𝑖𝑆 ). For example, when querying a block generator with 𝐴(𝑅0, [𝑡𝑥 1P ]), both [tx1P ] and [tx𝐴 , tx1P ] could be valid transaction sequences that extend the blockchain execution 𝑅0 . In contrast, an ideal-world block generator 𝑆 is a function that maps the past blockchain execution 𝑅0 directly to a block template without any such access to the mempool. The block template here is a transaction sequence with gaps (wildcards) consisting of simulator-generated transactions. Intuitively, wildcards serve as placeholders for transactions from the mempool. For instance, a simulator 𝑆 (𝑅0 ) can return the template block [tx𝑆 , _] indicating that the first transaction will be its own tx𝑆 followed by some transaction from the mempool. After the simulator has crafted a block template including its own transactions, transactions from the mempool are assigned to the template’s wildcards, and the block is published.

Overview & Key Insights

In cryptography, simulation-based security definitions characterize the security of a cryptographic protocol by comparing real-world interactions with this protocol in the presence of a real-world attacker with interactions in an idealized world. In such an idealized world, the ideal workings of the protocol are characterized by explicitly describing what information an attacker (then usually called the simulator) may learn and in which way they may interfere with

The attacker invalidates the user’s proposal by scheduling their own proposeCandidate transaction with the same identifier (here 1) and a different candidate ¬u at the beginning of their block, causing it to be executed before the honest user’s transaction. As a result, the honest user’s transaction will fail instead of resulting in a valid candidate proposal. The same behavior can be simulated in the ideal world by a simulator that proposes a candidate with identifier 1 (regardless of the mempool) within its block template. However, our DS Resistance definition will require that for each real-world attacker, there is a single ideal-world simulator that can simulate an attacker for all possible user behaviors. This means, in particular, that a real-world attacker may not gain any advantage

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

from observing user actions in the mempool since an ideal-world simulator could not mimic this adaptability of the real-world attacker. Consider, for instance, that the honest user chooses a different identifier Id for their proposeCandidate call:

In this case, the input to the simulator (consisting only of the past blockchain execution) would still be unchanged, making them output the same block template as before. In contrast, the real-world attacker would exploit the transaction observed in the mempool P2 and copy the new identifier. In fact, we cannot find a single simulator that simulates the real-world attacker for all valid user behaviors (proposing different identifiers) for the same initial blockchain run 𝑅0 . Therefore, the smart contract from Figure 3 is not classified to satisfy DS Resistance. Intuitively, we define Deckstacking Resistance as, for every malicious real-world block generator (attacker 𝐴), there exists a non-adaptive ideal-world block generator (simulator 𝑆) such that every valid smart contract execution of the honest user in the real world, can be simulated in the ideal world such that the executions agree on their observable behavior.

3.3

Real-World Blockchain Execution

The DS Resistance of a contract C does not only rely on the contract code but also on the behavior of honest users Hon interacting with C. E.g., in the illustrative example, honest users that refrain from calling the proposeCandidate function, are clearly not subject to the described attack. One can think of DS Resistance as the guarantee given to users Hon on the behavior of C when they interact with C. For example, many frontrunning mitigation techniques rely on honest users complying with restrictions, such as submitting certain transactions only in well-defined time windows or not leaking authentication secrets to the attacker. Thus we define DS Resistance with respect to a set ΣC of honest user strategies that describe the legitimate behavior of the users Hon when interacting with C. Modeling Cryptographic Interactions. To simplify presentation and reasoning, we will in the following treat the security of these building blocks in a symbolic fashion, meaning that we will assume ideal security (e.g., assuming that it is impossible to find the preimage of a hash function without having learned it before). This is a common approach to abstract the security of cryptographic primitives when modeling and analyzing cryptographic protocols (see [9, 17, 31]). We incorporate this notion of cryptography by assuming a dedicated set of secrets NHon of honest users and a concrete smart contract semantics that supports cryptographic operations with respect to an equational theory 𝜀 on symbolic terms. Attackers may only learn and use an honest user secret after it got revealed in the mempool or the previous blockchain run. As a consequence, transactions, as well as observables emitted in runs, may contain symbolic terms. Modeling Mempools. We define a mempool P as a list [tx0, . . . , tx𝑖 ] of valid transactions by honest blockchain users Hon. The choices of all honest users Hon for a contract C are modeled by a set of symbolic user strategies ΣCN . Each strategy Σ ∈ ΣCN is a function mapping the current blockchain run 𝑅 to the next

mempool PΣ expressing the combined strategy of all honest users while only using their shared set of symbolic secrets N . We define a number of correctness properties on a mempool PΣ and user strategy Σ to capture realistic blockchain behavior: A mempool can only contain valid transactions sent by honest users, i.e., transactions must be executable and may be only composed of knowledge available to such honest users. Additionally, the content of mempools must be persistent until inclusion in the run and, correspondingly, the honest user strategy needs to consistently publish the same transactions as long as they are valid (reflecting that a transaction once submitted to the mempool stays there). Real-World Scheduling Strategies. We model the mining of new blockchain blocks (cf. block generators in Section 3.2) with symbolic scheduling strategies that are based on the current blockchain run and mempool and return a valid next block. Formally, a symbolic scheduling strategy is a function 𝐴(𝑅, P) N , parameterized with a set of symbolic secrets N accessible by the function, that produces a valid transaction sequence B = [tx0, . . . , tx𝑛−1, 𝜏 ] where each transaction tx𝑖 ∈ B when sent by an honest user is unique and stems from the mempool, and otherwise needs to be constructible using attacker knowledge. Further, it is guaranteed that each pending transaction tx ∈ P from the mempool is included in block B if the time of its proposal by an honest user dates back at least 𝑘 blocks. Given a scheduling strategy 𝐴 and a user strategy Σ, we can now characterize the blockchain runs 𝑅 that result from the interactions of 𝐴 and Σ (written (𝐴, Σ) ⊢ 𝑅). In this case, we say that 𝑅 conforms to (𝐴, Σ) in the real world. First, it holds that (𝐴, Σ) ⊢ Γinit where Γinit here denotes the run starting in the initial blockchain configuration where no state transitions have been performed. Further, runs with (𝐴, Σ) ⊢ 𝑅 can be derived given that (𝐴, Σ) ⊢ 𝑅 ′ holds, by appending B ∗

a new block 𝐴(𝑅 ′, Σ(𝑅 ′ )) = B with 𝑅 = 𝑅 ′ −→ Γ𝑅 . So, a new xs

block B with observables xs can be added to the blockchain run 𝑅 provided that scheduler 𝐴 selects this block based on its knowledge of 𝑅 and the mempool created by Σ. Note that, for the sake of readability, we only explicitly annotate the symbolic secret sets of strategies when relevant.

3.4

Ideal-World Blockchain Execution

To clearly specify the limits of the ideal world, we define ideal-world scheduling to be a restricted version of real-world block scheduling: Crucially, an ideal-world scheduling should be non-adaptive to the mempool, meaning that its scheduling strategy is not influenced by the content of the mempool. In particular, we use the intuition of template blocks to restrict the set of symbolic scheduling strategies 𝑆 to be translucent towards certain mempool changes and aim to characterize the strongest ideal-world model with a non-adaptive scheduler. Note that comparing against an ideal-world model that is too strong (e.g., one that does not allow for any transaction reordering) yields a security notion that is too restrictive (e.g., forbidding any concurrent interactions with a contract). Similarly, an ideal-world model that is too weak (equipping the simulator with too much knowledge and capabilities) renders smart contracts that are intuitively insecure resistant to deckstacking. Formally, ideal-world scheduling strategies

On Identifying Sound Conditions for Frontrunning Resistance

are symbolic scheduling strategies that fulfill a stability requirement under substitution: We define a set of substitution functions operating on a mempool P or blockchain block B that is defining a sequence of honest user transactions in P/B to be substituted for other valid transactions ({tx/tx′ }) or removing them. Every substitution function 𝜌 is defined such that its application 𝜌 (P) on a mempool P returns a valid mempool P ′ . Such substitutions allow us to define the following stability criterion Π(𝑆) that rules out simulators that create blocks based on length, content and order of the mempool P: ∀𝜌.𝑆 (𝑅, 𝜌 (P)) = 𝜌 (𝑆 (𝑅, P)) This effectively eliminates any adaptive DS capabilities of the simulating scheduler 𝑆 in the ideal-world. In fact, this stability requirement on substitutions is the formalization of the template block intuition in Section 3.2. Intuitively, wildcards in a template are spots that should be filled with arbitrary transactions from the mempool. If the mempool changes (e.g., a transaction tx1 being replaced with a transaction tx2 ), then this change should be reflected when filling the template (by transaction tx2 being filled into the same wildcard slot that tx1 took before). Using this intuition, we define valid blockchain executions in the ideal-world by accepting any simulator 𝑆 that is a non-adaptive real-world attacker w.r.t. the stability requirement on substitutions. In this case, we write (𝑆, Σ) ⊢ 𝑅 and say that 𝑅 conforms to (𝑆, Σ) in the ideal world if 𝑆 is a scheduling strategy that satisfies Π(𝑆). Recall that a complete formalization of the stability requirement on substitutions and previous subsections is available in Appendix C.

3.5

Definition

We next define when a contract C is DS Resistant with respect to a set of symbolic user strategies Σ𝐶N . Each strategy describes one of Hon the legitimate behaviors of the users in Hon when interacting with C and owning secrets NHon . To capture different forms of observables in the most general fashion, we parametrize DS Resistance with a similarity relation ∼ that describes when a run 𝑅𝐴 and a run 𝑅𝑆 are considered to show the same observable behavior. More formally, this leads us to the following characterization: Deckstacking Resistance: A contract C satisfies Deckstacking Resistance w.r.t. a set of honest user strategies ΣCN if Hon

∀𝐴N . ∃𝑆 N with Π (𝑆 N ). ∀Σ ∈ ΣCN

.

Hon

∀𝑅𝐴 . (𝐴, Σ) ⊢ 𝑅𝐴 =⇒ ∃𝑅𝑆 . (𝑆, Σ) ⊢ 𝑅𝑆 ∧ 𝑅𝐴 ∼ 𝑅𝑆

where the scheduling strategies (𝐴 and 𝑆) and the user strategies do not share any secrets (N ∩ NHon = ∅). The simulation-based definition enables us to distinguish aimless, disadvantageous behavior (caused by asynchronous blockchain execution) from targeted malicious behavior. For instance, considering the example from Figure 3, ΣC would contain all strategies Σi invoking the proposeCandidate function with identifier i, so in particular Σ1 invoking proposeCandidate with identifier 1 and Σ8 invoking proposeCandidate with identifier 8. This exemplifies the chosen order of quantification such that a single simulator must be able to simulate every concrete user behavior and to restrain the adaptiveness of the simulator 𝑆 to such untargeted frontrunning.

Discussion. DS Resistance is purposefully defined such that it can be instantiated with any smart contract semantics, equational theory 𝜀 and similarity relation ∼. Indeed, the concrete choice of the similarity relation determines whether a contract is considered resistant to deckstacking or not. This reflects that, depending on the concrete smart contract, certain deviations from the ideal contract behavior caused by DS may be deemed acceptable (e.g., if such deviations can at most benefit honest users). Identifying securitycritical behavior (for which no deviations with respect to the ideal behavior should occur) is part of the contract development process, where developers usually explicitly log critical events in smart contracts. This gives rise to a generic similarity relation requiring that the same sequences of critical events (e.g., modifications of high-integrity contract state) are exhibited in the real- and idealworld execution. DS Resistance, however, is flexible enough to incorporate more fine-grained use-case-specific similarity notions, e.g., assigning and comparing (quantitative) utilities of different contract executions. This flexibility, conversely, implies that there is not one universal instantiation of the similarity relation ∼ that is adequate for all scenarios. E.g., consider a smart contract that allows a user to donate a fraction of their own assets under some miner-controlled condition (e.g., whenever the block number is even at the time of invoking the donation function). With an instantiation of ∼ that considers such runs similar, which provide the same payouts to all users, this contract would be classified as violating DS. This is because a deckstacking attacker could decide upon the execution/blocking of donations by placing calls to the donation function in even or odd blocks, respectively. However, depending on the context, one may argue that the ability to deny donations does not constitute harmful behavior (e.g., as such interference does not induce direct money losses). To reflect this interpretation, one could simply adjust the ∼ relation to ignore financial transfers triggered by invocations of the donation function. This example illustrates how the similarity relation ∼ serves to express the degree of interference of an adaptive, deckstacking attacker that is still deemed acceptable.

4

Interaction Condition Generation

A key insight of the previously presented definition is that DS Resistance is a property that does not concern a smart contract alone but the interplay between a contract and an honest user. This poses the question of how a user can decide whether their intended contract interactions can be subject to deckstacking attacks. To this end, in this section, we propose a procedure to generate provably secure interaction conditions from the code of a smart contract C. More specifically, such interaction conditions formulate requirements on the user strategy and guarantee that C together with any user strategy that meets these requirements satisfies DS Resistance. The key property of a user strategy to resist deckstacking attacks is that it only submits transactions txu to the blockchain that have a predictable effect (meaning that a deckstacking attacker cannot interfere with them). Since transactions can be only guaranteed to be included within a fixed number 𝑘 of blocks, user strategies, to achieve predictable transaction behavior, usually proceed in rounds of length 𝑘: whenever a user u submits a transaction txu , they want

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

1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16

contract TimelockedFeeMinted { function scheduleFeeChange ( uint _newFee ) onlyOwner { bytes32 id = sha256 (" newFee " , _newFee ); timestamps [ id ] = block . number + k; } function executeFeeChange ( uint _newFee ) onlyOwner { bytes32 id = sha256 (" newFee " , _newFee ); require ( timestamps [ id ] > 1) ; require ( timestamps [ id ] <= block . number ); fee = _newFee / 100; timestamps [ id ] = 1; } function mint () { uint minted = msg . value * (1 - fee ); emit Minted ( msg . sender , minted ); } // ...

// ...

Figure 5: Simplified OpenZeppelin TimelockController [33].

to ensure that within the next 𝑘 blocks, independently of how an adaptive attacker includes txu , the execution result will be the same. As an example, consider the smart contract depicted in Figure 5. This contract allows buying (aka minting) contract-specific tokens for a fee, which is determined by the contract owner, using the mint function. Such a contract can be easily prone to deckstacking attacks since a malicious contract owner, when observing a mint transaction, can preempt this transaction with a corresponding transaction that increases the fee, causing the honest user to buy less tokens than expected. The presented contract circumvents this problem by making a fee change subject to a staged process, where a contract owner first needs to invoke the scheduleFeeChange function to announce a fee change. The fee change can only be executed (using the executeFeeChange function) after time 𝑘. Consequently, an honest user can ensure not to be subject to unexpected fee changes by only invoking the mint function in rounds where initially no fee change has been scheduled. More precisely, a condition for securely invoking the mint function would be that ∀𝑖. Γ.S C ( timestamps [𝑖]) ≤ 1. In this case, the blockchain inclusion time ensures that by the end of the round (so after 𝑘 blocks), a mint transaction submitted at the beginning of the round will be included. The contract logic would ensure that the execution of executeFeeChange could only impact the fee in the following round, as Γ.S C ( timestamps [𝑖]) > block.number would hold for the remainder of the current round, even if the attacker executed scheduleFeeChange.

4.1

Overview & Key Insights

Our algorithm makes this reasoning explicit by generating a pair of conditions (𝜙 𝑝 , 𝜙𝑖 ) for the Minted event, which ensure (a) that if the condition 𝜙 𝑝 holds at the beginning of a round, then also the condition 𝜙𝑖 holds throughout the whole round, and (b) 𝜙𝑖 is sufficiently strong to ensure that the attacker cannot interfere with the execution of Minted during the round. For the previous example, ∀𝑖. Γ.S C ( timestamps [𝑖]) ≤ 1 would be such a candidate for 𝜙𝑖 , since it satisfies requirement (b) by excluding that executions of executeFeeChange may change the value of fee, which is the only (global) variable that may influence Minted. However, to satisfy requirement (a), the challenge also lies in (i) finding a condition 𝜙 𝑝 that can be checked at the beginning of the round so that the user can decide based on 𝜙 𝑝 whether it is safe to execute the mint function; (ii) ensuring that 𝜙𝑖 is indeed upheld throughout the whole round, even if the attacker executes arbitrary other transactions;

(iii) finding a formulation of (𝜙 𝑝 , 𝜙𝑖 ) that ideally characterizes all possible situations where it is safe for the user to execute the mint function. For example, the condition ∀𝑖. Γ.S C ( timestamps [𝑖]) ≤ 1 would immediately violate requirement (ii) since after the attacker executes scheduleFeeChange, it is no longer valid. Further, the condition is not sufficiently general (violating requirement (iii)), since it does not capture that executing mint would also always be safe if it could be excluded that the attacker is the owner of the contract. To solve these challenges, our algorithm proceeds by first generating candidate conditions (𝜙 𝑝 , 𝜙𝑖 ), which are then stepwise refined to satisfy requirements (a) and (b). We first illustrate the algorithm with the example: Synthesis Example. The algorithm starts from an event, which shall not be influenced by the attacker (here the Minted event) and uses the condition for reaching this event (also called the path condition) as the first candidate condition 𝜙𝑖0 . In our example, 𝜙𝑖0 = ⊤ since the Minted event can be reached unconditionally. We next check if 𝜙 𝑝0 set to 𝜙𝑖0 is a reasonable candidate for a round precondition, by checking whether 𝜙 𝑝0 holding at the beginning of the round (so for some value 𝑏 of block.number such that 𝑏 mod 𝑘 = 0) implies that 𝜙𝑖0 also holds during the round (so for values 𝑏 + 𝑖 of block. number such that 𝑖 < 𝑘). In this case, we say that (𝜙 𝑝0 , 𝜙𝑖0 ) is a round invariant. Indeed, (⊤, ⊤) trivially is a round invariant since it is fully independent of block.number. In the next step, we refine (𝜙 𝑝0 , 𝜙𝑖0 ) towards satisfying requirement (b): To this end, we determine the part of the global state (global contract variables and blockchain variables like block.number) that may directly impact the arguments of the Minted event, i.e., Minted’s data dependencies. In the example, the variable fee is the only data dependency of Minted. The algorithm then strengthens (𝜙 𝑝0 , 𝜙𝑖0 ) to enforce that fee cannot be written by the attacker by adding the following condition to both 𝜙 𝑝0 and 𝜙𝑖0 : 𝜙 NW = ∀_newFee ¬u , sender¬u . sender¬u ≠ u → ( sender¬u ≠ owner ) ∨ ( timestamps [ sha256 ( "newFee", _newFee ¬u ) ] ≤ 1) ∨ ( timestamps [ sha256 ( "newFee", _newFee ¬u ) ] > block.number )

The condition 𝜙 NW is derived from the function executeFeeChange by forming the no-write condition, so the disjunction of the path conditions of all execution paths that leave fee unchanged (also executeFeeChange denoted by NoWrite ( fee ←−−−−−−−−− ·)). 𝜙 NW further adds the pre¬u condition sender ≠ u, which requires that the sender (indicated by the variable sender¬u ) of the transaction invoking executeFeeChange shall be different from the honest user (represented by variable u). Note that we use the superscript ¬u to index variables that are local to the execution of an attacker transaction (such as the function argument _newFee ¬u and the transaction sender sender¬u ). Intuitively, 𝜙 NW states that if executeFeeChange is invoked by a user different from u, its execution will never write fee. Thus, the refinement leaves us with the new candidate condition (𝜙 𝑝1 , 𝜙𝑖1 ) = (𝜙 NW, 𝜙 NW ). Note, however, that (𝜙 𝑝1 , 𝜙𝑖1 ) does not constitute a round invariant, since incrementing the block number within the round can cause the third disjunct timestamps [ sha256 (. . . )] > block.number to become false. To correct this, we apply a generic strengthening to 𝜙 𝑝1 , replacing occurrences of block.number with block.number + 𝑘 − 1:

On Identifying Sound Conditions for Frontrunning Resistance

Notation f

FRu (𝑥

f

Description

Algorithm 1 Simplified synthesis of condition FRu (𝑥 ← − 𝑒)

𝑒 ) Procedure: a round invariant (𝜙𝑝 , 𝜙𝑖 ) ensuring that f deterministically assigns variable 𝑥 to expression 𝑒 Set of functions of contract C Global variables of contract C Local variables of function f (e.g., arguments) for user u Universal quantification over all local variables L ¬u

← −

FC GC Lu

f

∀Lg¬u .

f

Symbolic Execution Operations f

PathCondu (𝑥 ← − 𝑒 ) Path condition where executing f assigns 𝑥 to 𝑒 f

DDepsu (𝑥 ← − ·) Data dependencies of variable 𝑥 being written in f g − ·) Condition ensuring that executing g does not write 𝑦 NoWriteu (𝑦 ← u Inv ( g,𝜓, 𝜙 𝑝 ) Checks whether 𝜙𝑝 is an invariant under executions of function g that initially satisfy predicate 𝜓 getRI (𝜙 ) mergeRI (𝑟 1 , 𝑟 2 )

Round Invariant Operations Constructs a round invariant (𝜙 𝑝 , 𝜙 ) from 𝜙 by checking 𝜙 and possibly strengthening 𝜙 to 𝜙𝑝 Conjoins components of two round invariants

Require: Contract C, user u, function f ∈ FC , symbolic execution relation SEg for g ∈ FC , variable 𝑥 ∈ GC , and expression 𝑒 in f f

1:

f

2: 𝑊 ← ∅; 𝐷 ← DDepsu (𝑥 ← − ·) \ L u

Table 2: Legend for Section 4 and Algorithm 1

4:

∨ ( timestamps [ sha256 ( "newFee", _newFee ¬u ) ] ≤ 1) ∨ ( timestamps [ sha256 ( "newFee", _newFee ¬u ) ] > block.number + 𝑘 − 1)

This strengthening ensures that if timestamps [ sha256 (. . . )] > block.number + 𝑘 − 1 holds at the beginning of the round, then also timestamps [ sha256 (. . . )] > block.number (and thus 𝜙𝑖1 ) holds through-

out the whole round. After verifying that the strengthening estab′ ,𝜙 lishes a round invariant, we can use (𝜙 𝑝2 , 𝜙𝑖2 ) = (𝜙 NW NW ) as new round invariant. Finally, we check towards ensuring requirement (ii) whether ′ 𝜙 NW is indeed upheld when executing other contract functions ′ by users different from u, so whether 𝜙 NW is an invariant w.r.t. ′ these functions. This check holds because 𝜙 NW could only be invalidated by writes to the timestamps array, which may only occur in scheduleFeeChange and executeFeeChange. For executeFeeChange, the write to timestamps is already excluded due to the require state′ ments given that 𝜙 NW holds. In contrast, scheduleFeeChange may ′ write timestamps unconditionally. However, 𝜙 NW ensures that even after updating any timestamps [𝑖] to block.number + 𝑘, the condition timestamps [ sha256 (. . . )] > block.number + 𝑘 − 1 will hold. At this point, the algorithm terminates with the round invariant (𝜙 𝑝2 , 𝜙𝑖2 ), which cannot be invalidated by any attacker transaction in the same round (satisfying requirement (a)). Note that (𝜙 𝑝2 , 𝜙𝑖2 ) is constructed such that 𝜙𝑖2 enforces the path condition of Minted (so as long as 𝜙𝑖2 holds, Minted gets executed) and such that it prevents concurrent writes to data dependencies of Minted. For the given example, this ensures that a concurrent attacker transaction cannot change the way Minted is triggered (satisfying requirement (b)).

(𝜙 𝑝 , 𝜙𝑖 ) ← mergeRI ((𝜙 𝑝 , 𝜙𝑖 ),

 g − ·) ) getRI ∀L ¬u . sender¬u ≠ u → NoWrite¬u (𝑦 ← g 5: 𝑊 ← 𝑊 ∪ {(𝑦, g)} 6: done ← false 7: while Vars((𝜙 𝑝 , 𝜙𝑖 )) × FC ⊈ 𝑊 ∧ done = false do 8: done ← true 9: for all g ∈ FC do 10: if Inv¬u (g, sender¬u ≠ u, 𝜙 𝑝 ) then 11: continue 12: done ← false choose

14:

𝑦 ← Vars((𝜙 𝑝 , 𝜙𝑖 )) \ {𝑧 | (𝑧, g) ∈ 𝑊 } (𝜙 𝑝 , 𝜙𝑖 ) ← mergeRI ((𝜙 𝑝 , 𝜙𝑖 ),

 g getRI ∀L ¬u . sender¬u ≠ u → NoWrite¬u (𝑦 ← − ·) ) g 15: 𝑊 ← 𝑊 ∪ {(𝑦, g)} 16: return (𝜙 𝑝 , 𝜙𝑖 )

4.2 ′ 𝜙 NW = ∀_newFee ¬u , sender¬u . sender¬u ≠ u → ( sender¬u ≠ owner )

f

3: for all 𝑦 ∈ 𝐷, g ∈ FC do

13:

𝐷 Initial set of global data dependencies 𝑊 = { (𝑦, g ), . . . Set of pairs where writes to 𝑦 by g have been excluded Vars(·) Returns the set of variables occurring in a condition

(𝜙 𝑝 , 𝜙𝑖 ) ← getRI (PathCondu (𝑥 ← − 𝑒))

Generation Algorithm

Technically, we build the synthesis generation algorithm illustrated in the previous subsection upon a symbolic execution engine for smart contracts. The symbolic execution engine provides a logical description for the execution logic of a contract. More formally, for each contract function g, it describes a relation of tuples of the form ⟨𝜃, 𝜑⟩ which indicate the state updates 𝜃 that g will conduct along the execution path enabled by path condition 𝜑. To this end, state updates map contract variables to symbolic expressions 𝑒 (over global state variables). Our algorithm (described in Algorithm 1) takes as arguments the symbolic execution relations SEg for the functions g of a contract C, a contract function f, a user variable u, a contract variable 𝑥 and f an expression 𝑒 and generates conditions FRu (𝑥 ← − 𝑒) = (𝜙𝑝 , 𝜙𝑖 ). f

The generated condition FRu (𝑥 ← − 𝑒) will then ensure that if the user (indicated by variable u) executes a transaction txu that invokes function f at the beginning of a round where 𝜙 𝑝 holds, then executing txu will deterministically assign the variable 𝑥 according to the symbolic expression 𝑒. The expression 𝑒 here represents the concrete execution path that shall be taken when executing f. In the example generation, we showed mint

FRu ( Minted ←−− ( msg.sender, msg.value ∗ (1 − fee))) i.e., the conditions for deterministically assigning the Minted event according to the expression ( msg.sender, msg.value ∗ (1 − fee)), when executing mint. The expression ( msg.sender, msg.value ∗ (1 − fee)) is obtained by inlining the local assignments in the mint function. The symbolic execution relations allow us to formally define the notions of path conditions, data dependencies, no-write conditions, invariants, and round invariants used in the previous example. We

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

additionally assume two functions getRI and mergeRI that abstract the generation of round invariants: The function getRI , provided a condition 𝜙, generates a round invariant (𝜙 𝑝 , 𝜙𝑖 ) such that 𝜙 ≡ 𝜙𝑖 . In particular, getRI may attempt to strengthen the invariant as described in the example, or default to (⊥, 𝜙) in case the strengthening fails. The latter case would indicate that there is no safe interaction condition. The function mergeRI , provided two round invariants (𝜙 𝑝1 , 𝜙𝑖1 ) and (𝜙 𝑝2 , 𝜙𝑖2 ), creates a new round invariant (𝜙 𝑝 , 𝜙𝑖 ) such that 𝜙 𝑝 ≡ 𝜙 𝑝1 ∧ 𝜙 𝑝2 and 𝜙𝑖 ≡ 𝜙𝑖1 ∧ 𝜙𝑖2 , and, in particular, may simplify the conditions in the process. We overview these notions and functions in Table 2. Algorithm 1 proceeds as follows: It first computes a round inf

variant (using getRI ) from the path condition PathCondu (𝑥 ← − 𝑒) for writing 𝑥 to 𝑒 using function f (line 1). Then, it iteratively refines (𝜙 𝑝 , 𝜙𝑖 ) by ensuring that for all contract functions g and all variables 𝑦 that 𝑒 directly depends on (as per its data dependencies u

f

DDeps (𝑥 ← − ·)), no transaction executing g by a user different from u can write to 𝑦 (lines 3–5). This is realized by conjoining (using mergeRI ) the current condition with round invariants derived from g the conditions NoWrite¬u (𝑦 ← − ·), which ensure that function g cannot write to 𝑦. Here, the universal quantification over all local g variables of g in NoWrite¬u (𝑦 ← − ·) and the premise sender¬u ≠ u ensure that writes to 𝑦 are excluded regardless of the call parameters of g as long as g is invoked by a user different from u. Next, the algorithm enters a loop (lines 7–15) where it checks for all contract functions g whether the current 𝜙 𝑝 is an invariant under executions of functions g by a user different from u (checked by Inv¬u (g, sender¬u ≠ u, 𝜙 𝑝 ), line 10). If this is not the case, (𝜙 𝑝 , 𝜙𝑖 ) is further refined by selecting a variable 𝑦 from (𝜙 𝑝 , 𝜙𝑖 ) that had not yet been recorded in 𝑊 for function g (line 13) and conjoining the g corresponding condition NoWrite¬u (𝑦 ← − ·) (line 14) to the current invariant. The set 𝑊 here tracks pairs (𝑦, g) for which it has been excluded that g writes 𝑦. The algorithm terminates if all contract functions have been checked to maintain 𝜙 𝑝 or if all variables in (𝜙 𝑝 , 𝜙𝑖 ) got included in 𝑊 for all contract functions g. Note that also in the latter case, (𝜙 𝑝 , 𝜙𝑖 ) is ensured to be an invariant under all possible adversarial invocations of any g, since all variables in (𝜙 𝑝 , 𝜙𝑖 ) have been shown unalterable by any function g. Backrunning. A deckstacking attacker may not only interfere with user transactions through frontrunning (changing the behavior of honest transactions txu by placing adversarial transactions before them) but also through backrunning. Backrunning refers to the ability of an attacker to cause divergent behavior of an attacker transaction tx𝐴 by placing it strategically after honest user transactions. To avoid backrunning, we devise an algorithm similar to Algorithm 1 (specified in Appendix D). This algorithm generates conditions, which ensure that the way an honest transaction txu writes to a variable 𝑥 cannot change how an attacker transaction tx𝐴 writes variables from a set 𝑍 . The resulting condition f

(𝜙 𝑝 , 𝜙𝑖 ) = BRu (𝑍 ⊥[𝑥 ← −]) constitutes a round invariant enforcing that attacker transactions cannot change the values of variables in 𝑍 based on an update to 𝑥 provoked by the honest user executing f. In other words: the assignments to variables in 𝑍 are independent of how the honest user interacts with f to write 𝑥.

Figure 6: Illustration of generic simulator construction: The generic simulator publishes the complete honest user mempool = P0 in its first block. Afterwards, the simulator inspects the already published block " " to catch up ( ) with the attacker and to simulate the remaining blocks ( , , ) that it generates (by querying the attacker internally).

4.3

Soundness Proof

To formally reflect the round-based nature of user strategies, we define round-based user strategies Σ𝑟→ . Round-based user strategies (identifiable by the over-arrow) schedule new transactions only at the beginning of a round and keep on submitting the transactions throughout the whole round until they are published. They are derived from a round strategy Σ𝑟 which determines the transactions to be submitted during the round based on the round’s initial configuration Γ𝑟 . In the following construction, we restrict individual users to only submit a single transaction txu per round, i.e., only after 𝑘 blocks, they will submit consecutive transactions (as only then txu got certainly executed). However, the results naturally extend to multiple transactions per user and round for independent transactions or blockchains that enforce transaction ordering of multiple transactions with a nonce mechanism (such as Ethereum). We show that the interaction conditions generated by Algorithm 1 (and the corresponding backrunning algorithm from Appendix D) are sound, meaning that any user strategy Σ𝑟→ that abides by these conditions ensures that the contract C together with Σ𝑟→ satisfies DS Resistance. To this end, we construct a generic sim𝜙 ulator 𝑆 𝐴 that relies on the attacker 𝐴 as a black box, as well as on the contract code C. This simulator will feature two modes of operation: Based on the interaction conditions (computed from 𝜙 𝜙 the code of C, and provided to 𝑆 𝐴 via 𝜙), 𝑆 𝐴 will decide whether there exist transactions that can be safely executed by user u in 𝜙 the current round. If this is not the case, then 𝑆 𝐴 knows that the mempool at this point will be empty (and will stay empty for the 𝜙 whole round), and 𝑆 𝐴 can simulate the attacker 𝐴 perfectly. If there 𝜙

do exist transactions that can be safely executed by u, then 𝑆 𝐴 will enter a second mode where it first publishes the whole mempool P in its first block and then subsequently reconstructs the attacker’s run based on this initial mempool publication, exploiting its access to the previous run. An overview of this behavior is illustrated in Figure 6, and we defer the full simulator definition to Appendix D. After publishing the initial mempool P in the first block, 𝑆 proceeds by invoking 𝐴 on the empty run with mempool P0 = P that 𝑆 reads from the run. From this, 𝑆 obtains B0𝐴 , the last block published by 𝐴. Due to the round-based nature of Σ𝑟→ , 𝑆 can also reconstruct the mempool P1 = P0 \B0𝐴 that 𝐴 used as input for generating the current block and hence also generate the next attacker block B1𝐴 . From this point on, 𝑆 exactly mimics the actions of 𝐴 except

On Identifying Sound Conditions for Frontrunning Resistance

for excluding mempool transactions from P already published in the first block of the round. This construction ensures (due to the required blockchain inclusion time) that at the end of each round both 𝑅𝐴 and 𝑅𝑆 contain all transactions of the original mempool, as well as all the attacker actions scheduled by 𝐴 during this run.

an attacker from influencing the values of 𝑋 ∗ through the positioning of attacker transactions within a round. An attacker may use such power to perform changes to 𝑋 ∗ based on their mempool knowledge, which would break DS Resistance.

Observable Behavior. The interaction conditions will enforce a strong observable relation ∼𝑆 between the attacker run 𝑅𝐴 produced in the presence of 𝐴 and the simulated run 𝑅𝑆 produced in 𝜙 the presence of 𝑆 𝐴 that covers many practical use cases. We give a formal definition of ∼𝑆 in Appendix D. Intuitively, 𝑅𝐴 ∼𝑆 𝑅𝑆 denotes that 𝑅𝐴 and 𝑅𝑆 executed the same number of rounds and in each completed round all observables (produced by the contract semantics) agree up to reordering.

Proof Sketch. At the beginning of each round, the simulator 𝜙 𝑆 𝐴 decides whether to simulate the attacker based on the empty mempool (in case that 𝜙 does not hold) or to publish the mempool in the first block of the round (in case that 𝜙 holds). In the first case, by the definition of 𝜙 it is indeed ensured that Σ𝑟 will not schedule any transaction for the whole round. Consequently, the simulator can perfectly mimic the attacker 𝐴 since no honest user transactions need to be scheduled. In the second case, it is still guaranteed that 𝜙 the transactions scheduled by 𝑆 𝐴 at the end of each round are a permutation of those scheduled by 𝐴 such that the transaction sequences in both runs can be transformed into each other by pairwise swapping of either (i) the honest user transactions tx and attacker transactions tx𝐴 ; or (ii) honest user transactions tx and block-finalizing transactions 𝜏 ; or (iii) block-finalizing transactions 𝜏 and attacker transactions tx𝐴 . In all three cases, we can show that the transactions commute pairwise in that the transactions will still produce the same observables and the variables in 𝑋 ∗ will remain unchanged when swapping the transactions. This follows from FRu (Γ, tx, 𝑋 ∗ ), BRu (Γ, tx, 𝑋 ∗ ) and BRu (Γ, 𝜏, 𝑋 ∗ ), which enforce that tx and tx𝐴 only write variables if their critical dependencies are ensured to be left untouched by the other transactions of the round. In this way, 𝑋 ∗ stays unchanged, ensuring (by its definition) that also observables produced from events are the same independently of the transaction ordering. □

Soundness. Henceforth, we assume contracts C where all critical behavior is explicitly marked by an event. Concretely, invocations of the function f by u will write a specific event variable 𝑥 f , which is assigned all relevant information to be recorded. We denote the set of all variables that may influence event variables by 𝑋 ∗ . To state soundness, we make use of the predicate FRu𝜌 (Γ, tx, 𝑋 ∗ ) that checks whether executing tx in a round starting in configuration Γ will have a deterministic effect on variables in 𝑋 ∗ (so either write them to the same value or leave them unchanged). Intuitively, FRu𝜌 (Γ, tx, 𝑋 ∗ ) checks that if symbolically executing tx in Γ results in f

assigning a variable 𝑥 from 𝑋 ∗ to an expression 𝑒 then FRu (𝑥 ← − 𝑒) holds. Similarly, we use a predicate BRu𝜌 (Γ, tx, 𝑋 ∗ ) checking whether for all variables 𝑥 from 𝑋 ∗ , which will be written when executing f

tx in Γ, it holds that BRu (𝑋 ∗ ⊥[𝑥 ← −]). So, intuitively, BRu𝜌 (Γ, tx, 𝑋 ∗ ) ensures that an attacker may not rely on variable changes induced by tx to provoke changes in 𝑋 ∗ (through backrunning).

5 Theorem 4.1 (Soundness of Interaction Conditions). Let C be a contract, u be a user and 𝑋 ∗ be the set of variables influencing event variables in contract C. Let SEg be sound and complete symbolic execution relations for functions of C. Let Σ = Σ𝑟→ be the user strategy for a round strategy Σ𝑟 (for u and C) such that for all (1) configurations Γ, Γ ′ with Γ ≈𝑋 ∗ Γ ′ it holds that Σ𝑟 (Γ) = Σ𝑟 (Γ ′ ) (2) configurations Γ, Σ𝑟 (Γ) ≠ ∅ implies that Σ𝑟 (Γ) = {tx} for some tx and FRu𝜌 (Γ, tx, 𝑋 ∗ ), BRu𝜌 (Γ, tx, 𝑋 ∗ ) and BRu𝜌 (Γ, 𝜏 , 𝑋 ∗ ) hold. Further, let 𝜙 be defined as 𝜙 (Γ) :⇔ BRu (Γ, 𝜏 , 𝑋 ∗ ) ∧ ∃tx. FRu (Γ, tx, 𝑋 ∗ ) ∧ BRu (Γ, tx, 𝑋 ∗ ) Then for all runs 𝑅𝐴 such that (𝐴, Σ) ⊢ 𝑅𝐴 there exists a run 𝑅𝑆 such 𝜙 that (𝑆 𝐴 , Σ) ⊢ 𝑅𝑆 and 𝑅𝐴 ∼𝑆 𝑅𝑆 . The (slightly simplified) theorem states that for any round-based user strategy that makes scheduling decisions only based on variables in 𝑋 ∗ while respecting the interaction conditions, every at𝜙 tacker run can be simulated by our simulator 𝑆 𝐴 . In particular, this implies DS Resistance for the set of all user strategies that satisfy this requirement. The complete theorem and soundness proof can be found in Appendix D. Note that the theorem, in addition to respecting the frontrunning and backrunning conditions for the honest user transaction, also requires that BRu (Γ, 𝜏 , 𝑋 ∗ ), so that attacker transactions may not impact variables in 𝑋 ∗ by backrunning the block finalizing transaction 𝜏 . This requirement excludes

Implementation

We implemented the synthesis Algorithm 1 and refer to this prototype implementation as NODS (short for No Deckstacking Synthesizer). NODS synthesizes frontrunning-resistant interaction conf

ditions FRu (𝑥 ← − 𝑒) for an honest user u for all events in a smart contract function f. The implementation of NODS builds on top of the existing symbolic execution engine from [39] and the static analysis framework in [19]. In particular, we used the symbolic execution engine to implement the path condition generation, dependency analysis and the invariant verification from Section 4. The implementation is agnostic to the actual symbolic execution engine, closely follows the description of the algorithm and uses Z3 [15] as its underlying constraint solver. NODS utilizes smart strategies during round-invariant strengthening (getRI ) and merging (mergeRI ): To avoid over-strengthening of path conditions and losing precision, round-invariant checks and strengthening attempts materialize only on subterms of a path condition. In detail, we (lazily) compute the disjunctive normal form (DNF) of a path condition and enforce round invariants on every literal of that DNF—literals that are already round-invariant remain unchanged and will thereby not be over-strengthened. Within bounds, NODS keeps the DNF structure intact during the merging of conditions to produce more naturally structured output conditions. For example the output condition in Figure 7 for the TimelockedFeeMinted contract from Figure 5 closely resembles the manually derived condition from Section 4. Note that extracting all

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

Contract

Aud.

Issue

Sev.

ID AgentRegistryCore BatchedBancorMM ETHRegistrarContr. Funds KeepRandomBeaconOp. Loans Pool RocketStorage RocketTokenRPL TransactionManager Factory PolygonWorldID PWNSimple StateBridge ChildRegistrar RootRegistrar GnosisSafeRegistry OptionsContract Governance ArroToken AccountingEngine ACOToken LoanProposalImpl SpoolAccessControl

CD CD CD CD CD CD CD CD CD CD N N N N Q Q OZ OZ OZ OZ OZ OZ ToB ToB

5.5 6.2 3.3 6.15 5.7 6.16 3.9 6.5 6.9 4.14 6.7 5.4.4 7.9 5.4.4 QSP-7 QSP-7 C01 M01 Intro M-1 M01 M03 3 2

M C M H M M C H M M M L M L L C M M M M M H

LOC

𝐷 avail

𝐷 fixes

Vuln

Fix

Sat

Sound

Sat

Sound

Func

1394 1982 1313 921 1997 932 1239 108 377 1241 460 1517 218 749 444 689 644 557 1017 104 492 890 993 658

1385 1998 1387 935 2191 937 1111 112 407 1248 460 1527 265 699 479 722 690 927 1317 282 497 912 1031 661

unsat n/a unsat unsat unsat sat unsat sat unsat unsat unsat unsat sat unsat unsat unsat sat unsat sat unsat sat sat sat unsat

✓ ✓ ✓ ✓ ✓ ✓ ✓ ✓ ✓ ✓ ✓ ✓ ✓ ✓ ✓ ✓ ✓ ✓ ✓ ✓ ✓ ✓ ✓

sat n/a sat sat unsat sat unsat sat unsat unsat unsat sat sat sat sat sat sat sat sat unsat sat sat unsat n/a

✓ ✓ ✓ ✓ ✓ ✓ ✓ ✓ ✓ ✓ ✓ ✓ ✓ ✓ ✓ ✓ ✓ ✓ ✓ ✓ ✓ ✓ -

zero-day ✓ ✓ ✓ ✗ ✓ ✗ ✓ ✓ ✓ ✓ ✓ ✓ ✓ ✓ ✗ ✓ zero-day

Auditors (Aud.) CD N Q OZ ToB

ConsenSys Diligence Nethermind Quantstamp OpenZeppelin Trail of Bits

C H M L -

Critical High/Major Medium Low/Minor Unranked

sat unsat ✓ ✗

Satisfiable Unsatisfiable Yes (for soundness & functionality) No (for soundness & functionality) Overapproximation in symbolic exec. Timeout/undecidable by Z3

Severity (Sev.)

Verdict

n/a

-

Table 3: NODS results for datasets 𝐷 avail and 𝐷 fixes for satisfiability, soundness and functionality of synthesized condition.

1 2 3 4 5 6 7 8

ForAll ( ATTACKER_executeFeeChange ( uint256 ) __newFee , Or ( Extract (31 , 1, timestamps [ sha256 ( abi . encodePacked () )(" newFee " , ATTACKER_executeFeeChange ( uint256 ) __newFee ) ]) == 0) , attacker_sender != owner , Not ( ULE ( timestamps [ sha256 ( abi . encodePacked () (" newFee " , ATTACKER_executeFeeChange ( uint256 ) __newFee ))], block_number_honest + (k - 1) ))))

Figure 7: NODS output condition for the TimelockedFeeMinted contract from Figure 5.

but the rightmost bit and checking equivalence with 0 is equivalent to checking that the value is less than or equal to 1. Lastly, NODS has full support for additional user-supplied preconditions on the contract state to compute more situational interaction conditions. E.g., a realistic precondition that would simplify the above condition even further is honest_sender != owner.

5.1

NODS Evaluation

To validate NODS, we run NODS on all 48 contracts in 𝐷 avail and 𝐷 fixes (cf. Section 2) with a time limit of two hours per contract. After that, we manually evaluated the computed interaction conditions of all contract pairs, i.e., the vulnerable and fixed versions, for (1) soundness and whether the conditions (2) do not restrict the intended sound functionality of the fixed contract. Table 3 presents the detailed results of our tool evaluation. For each contract pair, we report the condition and soundness judgments, as well as the functional correctness of the conditions synthesized for the fixed contract. For (1) soundness, we concluded that all computed conditions are indeed sound w.r.t. DS Resistance. Checking soundness, in particular, included checking that the interaction condition for vulnerable contracts does not allow the described frontrunning attack. Regarding (2) functionality, for 13

1 2 3 4 5 6 7 8 9 10 11 12 13 14

contract CollateralProtocol { // from ACOToken mapping ( address = > uint ) members ; mapping ( uint = > uint ) debt ; mapping ( uint = > uint ) collateral ; function sellCollaterals ( uint payoutAmount , uint salt ) onlyOwner { uint start = salt % | collateral |; for ( uint i = start ; payoutAmount > 0; ++ i) if (0 < debt [ i ]) { payoutAmount -= collateral [ i ]; collateral [ i ] = 0; } } // ...

Figure 8: Simplified CollateralProtocol vulnerability [34].

out of 22 fixed contracts, we found the conditions to be functional. In two of the remaining cases, through an investigation of the interaction condition, we found the contract to remain vulnerable to the described attack. Therefore, NODS correctly synthesized non-functional conditions as no sound functional condition for the behavior could exist. NODS was unable to compute a satisfiable condition in seven cases. Four of those seven cases can be attributed to overapproximations in the symbolic analysis, e.g., due to complex language features such as dynamic contract creations. The analysis hit the timeout in the remaining three contract executions. These timeouts can be partially attributed to Z3 being unable to solve satisfiability queries due to the undecidability of the theories used in the symbolic execution (e.g., quantification over arrays). Zero-day Vulnerabilities. Both vulnerable contracts that we found in 𝐷 fixes were zero-day vulnerabilities. The first zero-day vulnerability is present in a collateral protocol DeFi smart contract [34] that provides functionalities to buy options by depositing a collateral that can be liquidated again when

On Identifying Sound Conditions for Frontrunning Resistance

redeeming the option. However, in the given contract, a malicious user can prevent their own collateral from being liquidated using frontrunning. The deployed liquidation algorithm liquidates the collaterals of users (whose deposits are not backed by options) sequentially until an accumulated payoutAmount is reached by iterating through an array of collateral holders starting at some position start. Prior to the audit, this starting position start of the liquidation sequence was a hard-coded constant. This would have enabled malicious users who were monitoring the mempool for liquidation calls to frontrun any liquidation sequence to back users that appear earlier in the liquidation sequence with options, thereby circumventing their liquidation. The auditor identified this DS vulnerability. As a consequence, the developers modified the contract to allow the liquidator to dynamically set the start of the liquidation sequence to a user-defined salt value. We sketched the essence of the modified contract in Figure 8. However, a DS attacker with access to the mempool can precompute all transactions before their inclusion in the blockchain and hence foresee the effect on the liquidation behavior for any given salt provided by the liquidator. Consequently, the malicious user can adapt to the provided salt and continue frontrunning the liquidation sequence to prevent their own liquidation. The second zero-day vulnerability is present in a staking contract [32] where new participants are registered using a createAgent function. The createAgent function takes an agentId, an owner, and additional metadata as parameters and creates a new agent entry in the contract state when the given agentId is not registered yet. This poses a series of denial-of-service risks caused by malicious users monitoring the mempool for createAgent function calls and frontrunning them with duplicated createAgent calls with altered metadata (cf. Figure 3). This effectively reverts the user call as their transaction would register a duplicate agentId. In particular, the malicious user could register their agent with the same owner address as the original transaction. While this strengthens the attack’s impact, it could trick users into thinking that their original transaction has been accepted. This attack vector was pointed out by the audit company. The contract developers implemented a fix ensuring that the owner parameter cannot be frontrun anymore, i.e., the fix adds a condition msg.sender == owner to the createAgent function. A simplified implementation of the allegedly fixed version can be found in Figure 9. However, this does not mitigate the underlying DoS attack on the createAgent function. The malicious user can continue frontrunning createAgent transactions and permanently prevent the registration of new agents. We responsibly disclosed both vulnerabilities to the corresponding contract developers and auditors.

6

Related Work

Frontrunning Attacks and Mitigations. Different forms of frontrunning attacks and defenses have been widely discussed in the literature and systematized by Eskandari et al. [18], Baum et al. [8], and Zhou et al. [43]. In particular, Eskandari et al. [18] provide a taxonomy of frontrunning attack methods as well as techniques to mitigate frontrunning incidents. All these works study the concept

1 2 3 4 5 6 7 8 9

contract StakingProtocol { // from AgentRegistryCore mapping ( uint = > address ) agents ; function createAgent ( address owner , uint agentId , /* ... */ ) { require ( msg . sender == owner ) ; require ( agents [ agentId ] == 0) ; agents [ agentId ] = owner ; // ...

Figure 9: Simplified StakingProtocol vulnerability [32].

of frontrunning empirically and do not aim to provide a formal characterization of the underlying problem. Characterizing Frontrunning. As discussed in Section 2.2, the existing approaches for characterizing a smart contract’s vulnerability to frontrunning attacks center around the concepts of MEV and TOD. MEV [4, 14] has been commonly used as a metric to quantify the monetary gains of frontrunning attackers and has been formally defined in [4]. However, this definition assumes knowledge of the concrete mempool and blockchain state and, hence, cannot be used to statically assess a contract’s susceptibility to MEV extraction. In more recent work, Bartoletti et al. [7] study MEV in a formal model of smart contract execution and introduce the notion of universal MEV, which characterizes the maximal gain that can be achieved by any arbitrary adversary, and study formal proofs of MEV freedom. The limitations of MEV, discussed in Section 2.2, still apply to universal MEV. The notion of TOD has been first introduced in [28] and then formally defined in [20]. Since TOD coarsely overapproximates a contract’s vulnerability to frontrunning attacks, it has been used as a basis of several practical tools (most notably Nyx [39] and Sailfish [10]) for the static detection of frontrunning vulnerabilities. These tools proceed by localizing the causes of transaction order dependencies (e.g., read-write hazards among variables, which could be accessed in concurrent transactions) and then apply heuristics to identify whether an identified cause gives rise to an exploitable frontrunning attack. Since those heuristics are not formally defined, it is unclear which precise security notion the resulting tools are checking. Fair Ordering. An orthogonal line of work is mitigating deckstacking on the system level by enforcing a mining process that provides fair ordering guarantees. In its generality, it has been shown in [27] that a strong fair ordering guarantee cannot be achieved in an asynchronous system. However, multiple works propose protocols to achieve weaker notions of fair ordering both in the context of a permissioned Byzantine Fault Tolerance (BFT) setting (which assumes a fixed set of miners) [26, 27] and in the permissionless blockchain setting (where the set of miners can change dynamically) [13, 25]. These works are orthogonal to the results presented in this paper in that DS Resistance aims to characterize the sensitivity of a smart contract to the influences of a strong reordering miner. If a contract satisfies DS Resistance, then this property would also hold for any miner model that assumes weaker reordering capabilities. Architectural-level mitigations. Alternative approaches to mitigate deckstacking on an architectural level center around proposals

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

for cryptographic protocols that aim to decouple the knowledge of mempool transactions and the attacker’s ability to react upon this knowledge. F3B [38] achieves this goal by encrypting transactions under a secret key that is only revealed by a dedicated decentralized committee upon transaction inclusion. FIRST [36] makes use of verifiable delay functions to ensure that users can only publish contract transactions after an amount of time that allows all pending mempool transactions to be included in the blockchain. Both solutions rely on additional (partially) trusted committees and lack rigorous analysis. In contrast to these architectural-level mitigation attempts, our work targets deckstacking at the smart-contract level, aiding the design of provably secure contracts within the existing blockchain architecture.

7

Conclusion

In this paper, we introduced Deckstacking Resistance, the first formal and precise characterization of a contract’s robustness against frontrunning attacks. The definition is motivated by the fundamental shortcomings of existing frontrunning detection techniques, which we empirically demonstrate. More precisely, we showed that existing notions are particularly restricted to cases where: (1) attacks need to be immediate, and (2) the adversary’s goal needs to be monetary. Our empirical study showed that these limitations prevent MEV from capturing more than 55% of audited vulnerabilities with confirmed frontrunning. Deckstacking Resistance is a simulation-based notion that contrasts how the executions of a contract interacting with an unrestricted block-generating attacker differ from those executions possible in the presence of a limited attacker that makes scheduling decisions without inspecting the mempool. In particular, our definition highlights that resistance to frontrunning attacks depends on user interactions. Based on this insight, we propose an algorithm to compute sound interaction conditions from a contract’s code that are sufficient to prove resistance to frontrunning attacks, and we provide a prototype implementation, which we validate against a benchmark of real-world smart contracts.

Acknowledgments We would like to thank the reviewers for their helpful feedback. This work has been supported by the Heinz Nixdorf Foundation through a Heinz Nixdorf Research Group (HN-RG) and funded by the Deutsche Forschungsgemeinschaft (DFG, German Research Foundation) under Germany’s Excellence Strategy – EXC 2092 CASA – 390781972.

References [1] 2024. Rekt - Leaderboard. Retrieved March 12, 2024 from https://rekt.news/ leaderboard/ [2] 2024. Smart contract auditing services. https://ethereum.org/en/developers/ docs/smart-contracts/security/#smart-contract-auditing-services [3] 2025. EEA EthTrust Security Levels Specification Version 3. https:// entethalliance.org/specs/ethtrust-sl/v3/ [4] Kushal Babel, Philip Daian, Mahimna Kelkar, and Ari Juels. 2023. Clockwork finance: Automated analysis of economic security in smart contracts. In 2023 IEEE Symposium on Security and Privacy (SP). IEEE, 2499–2516. [5] Michael Backes, Matteo Maffei, and Dominique Unruh. 2008. Zero-knowledge in the applied pi-calculus and automated verification of the direct anonymous attestation protocol. In 2008 IEEE Symposium on Security and Privacy (SP). IEEE, 202–215.

[6] Massimo Bartoletti and Roberto Zunino. 2018. BitML: A Calculus for Bitcoin Smart Contracts. In Proceedings of the 2018 ACM SIGSAC Conference on Computer and Communications Security, CCS 2018, Toronto, ON, Canada, October 15-19, 2018, David Lie, Mohammad Mannan, Michael Backes, and XiaoFeng Wang (Eds.). ACM, 83–100. doi:10.1145/3243734.3243795 [7] Massimo Bartoletti and Roberto Zunino. 2025. A theoretical basis for MEV. In International Conference on Financial Cryptography and Data Security. Springer, 225–242. [8] Carsten Baum, James Hsin-yu Chiang, Bernardo David, Tore Kasper Frederiksen, and Lorenzo Gentile. 2022. SoK: Mitigation of Front-Running in Decentralized Finance. In Financial Cryptography and Data Security. FC 2022 International Workshops. 250–271. [9] Bruno Blanchet. 2016. Modeling and verifying security protocols with the applied pi calculus and ProVerif. Foundations and Trends® in Privacy and Security 1, 1-2 (2016), 1–135. [10] Priyanka Bose, Dipanjan Das, Yanju Chen, Yu Feng, Christopher Kruegel, and Giovanni Vigna. 2022. Sailfish: Vetting smart contract state-inconsistency bugs in seconds. In 2022 IEEE Symposium on Security and Privacy (SP). IEEE, 161–178. [11] Lorenz Breidenbach, Philip Daian, Florian Tramèr, and Ari Juels. 2018. Enter the Hydra: Towards Principled Bug Bounties and Exploit-Resistant Smart Contracts. In 27th USENIX Security Symposium, USENIX Security 2018, Baltimore, MD, USA, August 15-17, 2018, William Enck and Adrienne Porter Felt (Eds.). USENIX Association, 1335–1352. https://www.usenix.org/conference/usenixsecurity18/ presentation/breindenbach [12] Sergiu Bursuc and Sjouke Mauw. 2022. Contingent payments from two-party signing and verification for abelian groups. In 2022 IEEE 35th Computer Security Foundations Symposium (CSF). IEEE, 195–210. [13] Christian Cachin, Jovana Mićić, Nathalie Steinhauer, and Luca Zanolini. 2022. Quick order fairness. In International Conference on Financial Cryptography and Data Security. Springer, 316–333. [14] Philip Daian, Steven Goldfeder, Tyler Kell, Yunqi Li, Xueyuan Zhao, Iddo Bentov, Lorenz Breidenbach, and Ari Juels. 2020. Flash boys 2.0: Frontrunning, transaction reordering, and consensus instability in decentralized exchanges. In 2020 IEEE Symposium on Security and Privacy (SP). IEEE, 910–927. [15] Leonardo De Moura and Nikolaj Bjørner. 2008. Z3: An efficient SMT solver. In International conference on Tools and Algorithms for the Construction and Analysis of Systems. Springer, 337–340. [16] Nachum Dershowitz and Jean-Pierre Jouannaud. 1990. Rewrite systems. In Formal models and semantics. Elsevier, 243–320. [17] Danny Dolev and Andrew Yao. 1983. On the security of public key protocols. IEEE Transactions on information theory 29, 2 (1983), 198–208. [18] Shayan Eskandari, Seyedehmahsa Moosavi, and Jeremy Clark. 2019. SoK: Transparent Dishonesty: Front-Running Attacks on Blockchain. In Financial Cryptography and Data Security - FC 2019 International Workshops, VOTING and WTSC, St. Kitts, St. Kitts and Nevis, February 18-22, 2019, Revised Selected Papers (Lecture Notes in Computer Science, Vol. 11599), Andrea Bracciali, Jeremy Clark, Federico Pintore, Peter B. Rønne, and Massimiliano Sala (Eds.). Springer, 170–189. doi:10.1007/978-3-030-43725-1_13 [19] Josselin Feist, Gustavo Grieco, and Alex Groce. 2019. Slither: a static analysis framework for smart contracts. In 2019 IEEE/ACM 2nd International Workshop on Emerging Trends in Software Engineering for Blockchain (WETSEB). IEEE, 8–15. [20] Ilya Grishchenko, Matteo Maffei, and Clara Schneidewind. 2018. A semantic framework for the security analysis of ethereum smart contracts. In Principles of Security and Trust: 7th International Conference, POST 2018, Held As Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Thessaloniki, Greece, April 14-20, 2018, Proceedings 7. Springer, 243–269. [21] Everett Hildenbrandt, Manasvi Saxena, Nishant Rodrigues, Xiaoran Zhu, Philip Daian, Dwight Guth, Brandon Moore, Daejun Park, Yi Zhang, Andrei Stefanescu, et al. 2018. Kevm: A complete formal semantics of the ethereum virtual machine. In 2018 IEEE 31st Computer Security Foundations Symposium (CSF). IEEE, 204–217. [22] Sebastian Holler, Anna Piscitelli, Jannik Albrecht, Stephan Dübler, Ghassan Karame, and Clara Schneidewind. 2026. MEV, Nyx and Sailfish Analysis. https: //github.com/AnnaRub1102/MEV_analysis GitHub repository. [23] Sebastian Holler, Anna Piscitelli, Jannik Albrecht, Stephan Dübler, Ghassan Karame, and Clara Schneidewind. 2026. NODS: No Deckstacking Synthesizer. https://github.com/SebastianHoller/NODS GitHub repository. [24] Jiao Jiao, Shuanglong Kan, Shang-Wei Lin, David Sanan, Yang Liu, and Jun Sun. 2020. Semantic understanding of smart contracts: Executable operational semantics of solidity. In 2020 IEEE Symposium on Security and Privacy (SP). IEEE, 1695–1712. [25] Mahimna Kelkar, Soubhik Deb, and Sreeram Kannan. 2022. Order-Fair Consensus in the Permissionless Setting. In APKC ’22: Proceedings of the 9th ACM on ASIA Public-Key Cryptography Workshop, APKC@AsiaCCS 2022, Nagasaki, Japan, 30 May 2022, Jason Paul Cruz and Naoto Yanai (Eds.). ACM, 3–14. doi:10.1145/ 3494105.3526239 [26] Mahimna Kelkar, Soubhik Deb, Sishan Long, Ari Juels, and Sreeram Kannan. 2023. Themis: Fast, strong order-fairness in byzantine consensus. In Proceedings of the 2023 ACM SIGSAC Conference on Computer and Communications Security,

On Identifying Sound Conditions for Frontrunning Resistance

CCS. [27] Mahimna Kelkar, Fan Zhang, Steven Goldfeder, and Ari Juels. 2020. OrderFairness for Byzantine Consensus. In Advances in Cryptology - CRYPTO 2020 40th Annual International Cryptology Conference, CRYPTO 2020, Santa Barbara, CA, USA, August 17-21, 2020, Proceedings, Part III (Lecture Notes in Computer Science, Vol. 12172), Daniele Micciancio and Thomas Ristenpart (Eds.). Springer, 451–480. doi:10.1007/978-3-030-56877-1_16 [28] Loi Luu, Duc-Hiep Chu, Hrishi Olickel, Prateek Saxena, and Aquinas Hobor. 2016. Making smart contracts smarter. In Proceedings of the 2016 ACM SIGSAC Conference on Computer and Communications Security, CCS. 254–269. [29] Diego Marmsoler and Achim D Brucker. 2021. A denotational semantics of solidity in Isabelle/HOL. In Software Engineering and Formal Methods: 19th International Conference, SEFM 2021, Virtual Event, December 6–10, 2021, Proceedings 19. Springer, 403–422. [30] Patrick McCorry, Alexander Hicks, and Sarah Meiklejohn. 2018. Smart Contracts for Bribing Miners. In Financial Cryptography and Data Security - FC 2018 International Workshops, BITCOIN, VOTING, and WTSC, Nieuwpoort, Curaçao, March 2, 2018, Revised Selected Papers (Lecture Notes in Computer Science, Vol. 10958), Aviv Zohar, Ittay Eyal, Vanessa Teague, Jeremy Clark, Andrea Bracciali, Federico Pintore, and Massimiliano Sala (Eds.). Springer, 3–18. doi:10.1007/978-3-662-58820-8_1 [31] Simon Meier, Benedikt Schmidt, Cas Cremers, and David Basin. 2013. The TAMARIN prover for the symbolic analysis of security protocols. In Computer Aided Verification: 25th International Conference, CAV 2013, Saint Petersburg, Russia, July 13-19, 2013. Proceedings 25. Springer, 696–701. [32] Forta Network. 2022. Mitigate agent creation DOS. https://github.com/fortanetwork/forta-contracts/pull/155/files [33] OpenZeppelin. 2023. OpenZeppelin Contracts Repository. https://github.com/ OpenZeppelin/openzeppelin-contracts/ [34] Auctus Options. 2020. [H01] Collateral owners can skip being exercised. https: //github.com/AuctusProject/aco/pull/25/files [35] Kaihua Qin, Liyi Zhou, and Arthur Gervais. 2022. Quantifying Blockchain Extractable Value: How dark is the forest?. In 43rd IEEE Symposium on Security and Privacy, SP 2022, San Francisco, CA, USA, May 22-26, 2022. IEEE, 198–214. doi:10.1109/SP46214.2022.9833734 [36] Emrah Sariboz, Gaurav Panwar, Roopa Vishwanathan, and Satyajayant Misra. 2025. First: Frontrunning resistant smart contracts. In Proceedings of the 20th ACM Asia Conference on Computer and Communications Security. 873–889. [37] Christof Ferreira Torres, Ramiro Camino, et al. 2021. Frontrunner jones and the raiders of the dark forest: An empirical study of frontrunning on the ethereum blockchain. In 30th USENIX Security Symposium (USENIX Security 21). 1343–1359. [38] Haoqian Zhang, Louis-Henri Merino, Ziyan Qu, Mahsa Bastankhah, Vero EstradaGaliñanes, and Bryan Ford. 2023. F3B: A Low-Overhead Blockchain Architecture with Per-Transaction Front-Running Protection. In 5th Conference on Advances in Financial Technologies (AFT). [39] Wuqi Zhang et al. 2024. Nyx: Detecting Exploitable Front-Running Vulnerabilities in Smart Contracts. In 2024 IEEE Symposium on Security and Privacy (SP). IEEE Computer Society. [40] Zhuo Zhang, Zhiqiang Lin, Marcelo Morales, Xiangyu Zhang, and Kaiyuan Zhang. 2023. Your exploit is mine: Instantly synthesizing counterattack smart contract. In 32nd USENIX Security Symposium (USENIX Security 23). 1757–1774. [41] Liyi Zhou, Kaihua Qin, Antoine Cully, Benjamin Livshits, and Arthur Gervais. 2021. On the Just-In-Time Discovery of Profit-Generating Transactions in DeFi Protocols. In 42nd IEEE Symposium on Security and Privacy, SP 2021, San Francisco, CA, USA, 24-27 May 2021. IEEE, 919–936. doi:10.1109/SP40001.2021.00113 [42] Liyi Zhou, Kaihua Qin, Christof Ferreira Torres, Duc V Le, and Arthur Gervais. 2021. High-frequency trading on decentralized on-chain exchanges. In 2021 IEEE Symposium on Security and Privacy (SP). IEEE, 428–445. [43] Liyi Zhou, Xihan Xiong, Jens Ernstberger, Stefanos Chaliasos, Zhipeng Wang, Ye Wang, Kaihua Qin, Roger Wattenhofer, Dawn Song, and Arthur Gervais. 2023. SoK: Decentralized Finance (DeFi) Attacks. In 2023 IEEE Symposium on Security and Privacy (SP). IEEE, 2444–2461.

Generative AI Usage This paper was edited for grammar using Grammarly and ChatGPT. The development of NODS was aided by GitHub Copilot, which generated skeleton implementations from high-level descriptions of the toolchain and inferred interface bindings for calls into existing codebases used for symbolic analysis. During development, most of this generated code was replaced with human-written implementations. An exception is a set of self-contained modules for SMT formula transformations, authored entirely by GitHub Copilot; these modules underwent thorough testing and fuzzing, with Z3

serving as an external correctness oracle. We additionally developed a hand-crafted test suite to validate the correctness of NODS as a whole.

A

Open Science

We provide three different kinds of artifacts with this paper: (1) Datasets: As described in Section 2.2, we leverage 287 publicly available professional smart contract audits to create three datasets (𝐷 full , 𝐷 avail , 𝐷 fixes ) containing audits mentioning frontrunning vulnerabilities, the source code of those vulnerabilities, and the source code of their respective fixes. (2) Code: The source code of the NODS prototype implementing the synthesis algorithm (cf. Section 4) for frontrunning secure interaction conditions as described in Section 5. (3) Evaluation-Results: The results of the evaluation of static and dynamic frontrunning analysis approaches in Section 2.2 and the evaluation results of NODS in Section 5.1 and Table 3. To ensure reproducibility of our results, our complete datasets (𝐷 full , 𝐷 avail , 𝐷 fixes ), the codebase of NODS, and the evaluation results are available on GitHub here [23] and here [22].

B

Ethical Considerations

This work studies frontrunning vulnerabilities in Ethereum. As these classes of vulnerabilities are already well documented, our emphasis is on developing a precise definition to capture them and to responsibly advance the fairness and security of blockchain systems. Guided by our analysis and definition, we identified that two fixes previously implemented in response to audit reports remain susceptible to frontrunning attacks. We responsibly disclosed these findings to the corresponding Ethereum contract owners and the audit companies. We additionally disclosed our results to the Enterprise Ethereum Alliance and have worked with them to adjust their vulnerability classification in the EEA EthTrust Security Levels Specification [3].

C

Deckstacking Resistance Model

In this section, we provide further details and formalizations that accompany the definition of Deckstacking Resistance presented in Section 3.

C.1

Transaction Semantics

The complete blockchain state is modeled as a configuration Γ = (𝑊, C, 𝑏) where 𝑊 maps users to their wallet states, C maps all contracts to their states, and 𝑏 is the current block number. We also write Γ.𝑏 to access the block number 𝑏 of a configuration Γ. Since DS Resistance is a general definition that applies to smart contracts in different languages, we do not fix the concrete layout of contracts (i.e., the modeling of program execution, functions, constructors, etc.) or of its storage here. We model the evolution of blockchain states with a transition system on such configurations Γ. Configurations can be advanced with transactions tx. Those transactions can either be a contract

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

call tx whose execution impacts the states of users and contracts or the distinct block-finalization transaction 𝜏 that increments the block number. To capture the effects of executing a transaction tx (which may involve multiple asset transfers or the logging of tx

different events), each transition Γ0 −−→ Γ1 emits a list of observables 𝑥𝑠

𝑥𝑠. Formally, transitions are defined by inference rules such as the following rule of contract calls:

𝑅 ↓ T ∪ P ↓ T ∪ N ⊨𝜀 {tx𝐴 }

tx

Γ = (𝑊, C, 𝑏 ) C (C ) = S

(𝑊, S )𝑏 ↦ −→ (𝑊 ′ , S ′ )𝑏 Γ ′ = (𝑊 ′ , C ′ , 𝑏 ) 𝑥𝑠 −−−→ tx = C.f ( txarg) C ′ = C [C := S ′ ]

The notion of secrets enables us to faithfully model knowledgebased deckstacking-attacks when the smart contract logic relies on cryptographic operations.

tx

Γ −→ Γ ′ 𝑥𝑠

The rule states that when transaction tx is a contract call −−−→ −−−→ C.f( txarg) of contract C’s function f with arguments txarg, then the contract state S of C and the wallet state 𝑊 of all blockchain users are updated according to some smart contract execution setx

mantics (𝑊, S)𝑏 ↦−−→ (𝑊 ′, S ′ )𝑏 . The updates are applied to Γ, re𝑥𝑠

tx

sulting in Γ ′ . The smart contract execution semantics ↦−−→ is a for𝑥𝑠

mal way of specifying the smart contract execution behavior and can be instantiated for different smart contract languages such as [21, 24, 29]. Block finalization is modeled by a second inference 𝜏 rule (𝑊, C, 𝑏) → − (𝑊, C, 𝑏 ′ ) that increases the block counter by one tx0 (𝑏 ′ = 𝑏 + 1). We call a sequence of (valid) state transitions Γ0 −−→ 𝑥𝑠 0

tx1

tx𝑛−1

[tx0 ,tx1 ,...,tx𝑛−1 ] ∗

𝑥𝑠 1

𝑥𝑠𝑛−1

𝑥𝑠 0 ·𝑥𝑠 1 ·...·𝑥𝑠𝑛−1

−−−−−−−−−−−−→ Γ𝑛 for Γ1 −−→ · · · −−−−→ Γ𝑛 a run and also write Γ0 − short (where 𝑥𝑠 1 · 𝑥𝑠 2 denotes list concatenation). Note that we will assume in the following that the sender of a transaction tx is always provided in the function arguments and can be accessed via a function sender(tx).

C.2

terms occurring in run 𝑅. These terms can include symbolic secrets and we use the notation T1 ⊨𝜀 T2 to indicate that a set of (symbolic) terms T2 can be derived from a set of terms T1 using theory 𝜀. Additionally, attackers and honest users each have a dedicated set of fresh cryptographic secrets N𝐴 (NHon ). The attacker (honest user) may only use secrets in their own transaction tx𝐴 from N𝐴 (NHon ) or if they are derivable from public knowledge, i.e., if it is revealed in the mempool or the previous blockchain run:

Symbolic Model of Cryptography

The definition of Deckstacking Resistance incorporates a symbolic notion of cryptography by instantiating the smart contract semantics with an equational theory 𝜀. Equational Theory. We assume a standard setup for an equational theory 𝜀 on symbolic terms including functions, equations and constants [16]. Functions are defined as congruent rewriting rules (𝜌, 𝑏, 𝜎) ⊢𝜀 𝛼 → 𝛽 with access to an environment consisting of a variable mapping 𝜌, the current block number 𝑏 and the wallet state 𝜎. The base set of functions of the equational theory is enriched by blockchain-specific access to this environmental information, e.g., (𝜌, 𝑏, 𝜎) ⊢𝜀 now → 𝑏 (𝜌, 𝑏, 𝜎) ⊢𝜀 #T → 𝜎 (T)

C.3

Real-World Blockchain Execution

Modeling Mempools. We define a mempool P as a list [tx0, . . . , tx𝑖 ] of valid transactions by honest blockchain users Hon. The choices of all honest users Hon for a contract C are modeled by a set of symbolic user strategies ΣCN . Each strategy Σ ∈ ΣCN is a function mapping the current blockchain run 𝑅 to the next mempool PΣ expressing the combined strategy of all honest users while only using their shared set of symbolic secrets N . To ensure correctness of every mempool PΣ , for each transaction tx ∈ PΣ it needs to hold that tx is tx

→ Γ ′ (with Γ𝑅 being 𝑅’s last configura(i) valid, i.e., ∃Γ ′ : Γ𝑅 − tion), (ii) authentic, i.e., sender(tx) ∈ Hon, (iii) 𝜀-derivable, i.e., 𝑅 ↓ T ∪ N ⊨𝜀 {tx}, tx′

(iv) persistent, i.e., if tx ∈ Σ𝑖 (𝑅) and Γ𝑅 −−→ Γ𝑅 ′ with tx ≠ tx′ then tx ∈ Σ𝑖 (𝑅 ′ ) (𝑅 ′ extends 𝑅 with tx′ ), Real-World Scheduling Strategies. Formally, a symbolic scheduling strategy is a function 𝐴(𝑅, P) N , parameterized with a set of symbolic secrets N accessible by the function, that produces a valid transaction sequence B = [tx0, . . . , tx𝑛−1, 𝜏 ] where each transaction tx𝑖 ∈ B when sent by an honest user is unique and stems from the mempool (tx𝑖 ∉ P ⇒ sender(tx𝑖 ) ∉ Hon), and otherwise needs to be constructible using attacker knowledge (tx𝑖 ∉ P ⇒ 𝑅 ↓ T ∪ P ↓ T ∪ N ⊨𝜀 {tx𝑖 }). Further, it is guaranteed that a transaction tx ∈ P is included in block B if it was proposed at least 𝑘 blocks earlier by an honest user. Formally, this blockchain inclusion guarantee (for a fixed 𝑘) is ensured by requiring that whenever tx𝑖 ∉ B = 𝐴(𝑅, Σ(𝑅)), then there is also no previous sub-run 𝑅 ′ with Γ𝑅 ′ →∗ Γ𝑅 that is 𝑘 blocks behind (denoted by 𝛿 (𝑅 ′ ) + 𝑘 ≤ 𝛿 (𝑅) where 𝛿 (𝑅) gives the last block number of 𝑅) and where the user strategy already proposed tx𝑖 (tx𝑖 ∈ Σ(𝑅 ′ )). The inductive transition rule for (𝐴, Σ) ⊢ 𝑅 is given in the following rule: (𝐴, Σ) ⊢ 𝑅 ′

𝐴(𝑅 ′, Σ(𝑅 ′ )) = B = [tx0, tx1, . . . , tx 𝑗 ]

where now (#T) is the smart contract language expression to access the current block number (resp. the current token balance of token kind T). Equational theories needed to model cryptographic primitives used in the context of frontrunning protection in smart contracts include hashing, signing and zero-knowledge verification, which have been studied in detail for different domains [5, 12, 31].

C.4

Secrets. Transactions and observables emitted in runs may contain symbolic terms and we write 𝑅 ↓ T to denote the set of all (top-level)

What complicates the definition of non-adaptivity is the fact that while the 𝑆’s scheduling strategy itself should be uniform (w.r.t P),

tx𝑖 = 𝜏 ↔ 𝑖 = 𝑗

tx0

tx1

𝜏

𝑥𝑠 0

𝑥𝑠 1

𝑥𝑠 𝑗

𝑅 = 𝑅 ′ −−→ Γ 1 −−→ . . . −−→ Γ𝑅𝑗 (𝐴, Σ) ⊢ 𝑅

Substitution and Stability Criterion

On Identifying Sound Conditions for Frontrunning Resistance

this does not hold for the strategy’s output. The blocks generated by 𝑆 may include honest user transactions, and hence, immediately depend on P. We will capture this by requiring that any modification P ′ of P, i.e., exchanging transactions with different ones, or shortening P, should similarly be reflected in the block B = 𝑆 (𝑅, P ′ ). To this end, we consider that P can be modified by a sequence of individual substitutions of the form • tx1 → tx2 (indicating that tx1 gets replaced by tx2 ) • tx → ⊥ (indicating that tx in a final position gets removed) such that these substitutions can also be applied to B = 𝑆 (𝑅, P). So, in particular, any transaction tx1 from P that occurs in B should be replaced in the same way in B as it is replaced in P. Similarly, if P is shortened by transaction tx then tx should also be removed from B. Formally, we define the application P [tx → 𝑥] of a substitution tx → 𝑥 on mempool P recursively as follows:   [tx1 ] · ( P ′ [tx → 𝑥 ] )         P [tx → 𝑥 ] := [𝑥 ] · P ′        [] 

P = [tx1 ] · P ′ ∧ tx ≠ tx1 ∧𝑥 ∉ P P = [tx1 ] · P ′ ∧ tx = tx1 ∧𝑥 ≠ ⊥ ∧𝑥 ∉ P P = [tx] ∧ 𝑥 = ⊥

Note that this function is only defined on mempools P that (1) contain the transaction tx to be substituted at least once; (2) contain the transaction tx to be deleted in end position; (3) for which the substitution will not produce collisions (so will not insert a transaction that already exists in P). Further, assuming that all mempools P are free of duplicates also P ′ = P [tx → 𝑥] is duplicate-free (since the substitution is only defined given that it introduces a new transaction). Now, for any two mempools P1 and P2 , there exists a sequence of substitutions that transforms P1 into P2 (or vice versa). We write for such a sequential application ((P [tx1 → 𝑥 1 ]) . . . ) [tx𝑛 → 𝑥𝑛 ] of a sequence of substitutions also P [tx1 → 𝑥 1, . . . , tx𝑛 → 𝑥𝑛 ] for short. To reflect the effects of mempool changes on blocks, we define the application B [tx → 𝑥] B of a substitution tx → 𝑥 on a block B as follows:  [𝜏 ] B = [𝜏 ]     ′ [tx → 𝑥 ] )  [tx ] · ( B B = [tx1 ] · B ′ ∧ tx ≠ tx1 1 B     [𝑥 ] · B ′  B = [tx1 ] · B ′ B [ tx → 𝑥] B :=  ∧ tx = tx1 ∧ 𝑥 ≠ ⊥   ′   B [tx → 𝑥 ] B = [tx1 ] · B ′  B    ∧ tx = tx1 ∧ 𝑥 = ⊥  As opposed to substitution on mempools, block substitution allows for deleting transactions that are not in the end position. This is needed to reflect that shortening a mempool by transactions tx results in the deletion of tx in the block, where it may not necessarily occur as the last element. With these definitions in place, we can formally define the nonadaptiveness of simulators: Definition C.1 (Non-adaptiveness). Let Hon be a set of honest users. An attacker strategy 𝑆 (against Hon) is non-adaptive (written Π(𝑆)) if and only if the following holds: For all runs 𝑅 and

all mempools P and P ′ such that there exist 𝑛 ∈ N and substitutions tx1 → 𝑥 1, . . . , tx𝑛 → 𝑥𝑛 with 𝑥 1, . . . , 𝑥𝑛 ∈ {⊥} ∪ {tx ∈ X | sender(tx) ∈ Hon} and P ′ = P [tx1 → 𝑥 1, . . . tx𝑛 → 𝑥𝑛 ], it holds that 𝑆 (𝑅, P ′ ) = 𝑆 (𝑅, P ) [tx1 → 𝑥 1 , . . . tx𝑛 → 𝑥𝑛 ] B .

Intuitively, this definition requires that if a mempool P ′ resulted from applying a sequence of substitutions tx1 → 𝑥 1, . . . , tx𝑛 → 𝑥𝑛 (which only substitutes honest user transactions) to a mempool P, then the simulator 𝑆 invoked on P ′ will produce the same block that would result from invoking 𝑆 on P and applying substitutions tx1 → 𝑥 1, . . . , tx𝑛 → 𝑥𝑛 afterwards. Note that even in the cases of untargeted frontrunning or when ΣC consists only of a single honest user strategy, the simulator’s capabilities are limited by non-adaptiveness. In contrast to the attacker 𝐴, the simulator 𝑆 can never rely on mempool knowledge to construct transaction tx (tx ∉ P → 𝑅 ↓ T ∪ N ⊨𝜀 {tx}). The non-adaptiveness of the simulator, in particular, requires the simulator to produce a strategy that is uniform w.r.t. the one that was created for an empty mempool (where no information about honest user transactions is available).

D

Soundness Proof

In this section, we prove the soundness of the proposed algorithm for synthesizing interaction conditions.

D.1

Preliminaries

In the following, we are concerned with a concrete contract C and will denote transactions invoking this contract with txC . Further, we will use Γ.S C to refer to the state of contract C in configuration Γ (which maps each contract variable to its value) and will use XC to refer to the set of contract variables of C (constituting the domain of Γ.S C ) and FC to denote the set of functions of C. We will use Γ.S C ≈𝑋 Γ.S C to denote that the states Γ.S C and Γ.S C coincide on all variables from 𝑋 ⊆ XC . We will assume that the observables produced by the semantics record the values of a specific event variable (at the end of transC action execution) and are of the form ⟨𝑥 : 𝑣⟩ where 𝑥 ∈ 𝑋 Ev is the event variable and 𝑣 is its value. For the sake of simplicity, we will assume every transaction emits at most one observable. Note that, effectively, we are not losing generality with this since we can simply assume that there is a specific (local) event variable C 𝑥 f ∈ 𝑋 Ev = {𝑥 f | f ∈ FC } for each function, which contains the list of all events emitted during execution of the function. In particular, −𝑣 ) that this means that if the execution of a transaction txC = C.f(→ writes function f of contract C produces an observable ⟨𝑥 f : 𝑣⟩, then the transaction execution changes the value of the event variable 𝑥 f to 𝑣. Correspondingly, every change of the event variable 𝑥 f results in an observable ⟨𝑥 f : 𝑣⟩ where 𝑣 is the new value of 𝑥 f . We make this assumption more formal in Section D.2.3. D.1.1 Symbolic Execution. In the following, we will assume the existence of sound and complete symbolic execution for smart contracts. To this end, we will assume a set E 𝑖 of programming f expressions over the extended variables X𝑖 = GC ∪ L𝑖 of a conC,f f tract C. The extended variables X𝑖 consist of the global variables C,f

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

GC that contain all contract variables XC and the variable to access the block number (b), as well as the contract’s local variables L𝑖 containing the variables of the function argument and sender f for a function f. Note that we assume all variables in L𝑖 to be f indexed with an index 𝑖 to allow for correct scoping during the analysis. In particular, this will allow us to distinguish between different transactions invoking the same function (and therefore assigning different values to the local variables, such as function arguments). Note that we also write Γ ≈𝑋 Γ for 𝑋 ⊆ GC provided that Γ.S C ≈𝑋 \{b} Γ.S C and if b ∈ 𝑋 also Γ.𝑏 = Γ.𝑏. Remark. For the sake of simplicity, we consider the block number b as sole global variables. Realistic smart contract languages may also provide access to other global variables such as the block timestamp or the state of the wallets of other users. It is easy to extend our analysis to such other global variables, which will need to be considered fully attacker-controlled. This can be done by synthesizing the condition ⊥ when encountering dependencies of critical variables to any such global variable different from ⊥. We will write Vars𝑖 (𝑒) (where Vars(𝑒) ⊆ X𝑖 ) to denote the C,f set of variables occurring in expression 𝑒 ∈ E 𝑖 . Formally, we will f assume that for each function f of a smart contract C that there exists a relation SE𝑖 containing pairs of the form ⟨𝜃, 𝜑⟩ where f 𝜃 ∈ X𝑖 → E 𝑖 is a substitution from variables to expressions and C,f f 𝜑 is a logical condition of the variables in X𝑖 . We will further C,f assume that there exists a function VC𝑖 (Γ, tx) that maps a concrete configuration Γ and a transaction tx to a corresponding assignment V over the extended variables X𝑖 . In particular, we will assume C,f that for the assignment of global variables, VC𝑖 (Γ, tx) is agnostic to the transaction tx. So, more formally: Assumption 1. Let Γ be a configuration, tx1 and tx2 be transactions, C be a contract and 𝑥 ∈ GC be a variable. Then for any index 𝑖 VC𝑖 (Γ, tx1 )(𝑥) = VC𝑖 (Γ, tx2 )(𝑥) In the following, we write V (𝑒) to denote the evaluation of expression 𝑒 ∈ E 𝑖 under assignment V. f In the remainder of the paper, we will assume the symbolic execution relations to be sound and complete. Assumption 2 (Soundness of symbolic execution). Let C be a contract and f ∈ FC . Then the symbolic execution relation SE𝑖 for f function f and indexed by some index 𝑖, satisfies the following soundness property: −𝑣 . tx = C.f(→ −𝑣 ) ∀tx f → ⇒ ∀Γ 𝜃 𝜑. ⟨𝜃, 𝜑⟩ ∈ SE𝑖f ∧ VC𝑖 (Γ, tx) |= 𝜑 tx

⇒ ∃Γ ′ . Γ −→ Γ ′ ∧ VC𝑖 (Γ ′, tx) = VC𝑖 (Γ, tx) ◦ 𝜃 where V ◦ 𝜃 denotes the assignment obtained by first applying the substitution 𝜃 and then evaluating the resulting expression under V (so V ◦ 𝜃 (𝑥) = V (𝜃 (𝑥))). Note that, in particular, it holds that V ◦ 𝜃 (𝑒) = V (𝑒𝜃 ) where 𝑒𝜃 denotes the expression obtained by applying the substitution 𝜃 to the expression 𝑒 ∈ E 𝑖 . f This statement expresses the soundness of the symbolic execution relation SE𝑖 : for each concrete configuration Γ and transaction f

tx invoking function f, if there exists a symbolic execution result ⟨𝜃, 𝜑⟩ such that the condition 𝜑 is satisfied under the assignment corresponding to Γ and tx, then there exists a concrete transition executing tx from Γ to some configuration Γ ′ such that the assignment obtained from Γ ′ corresponds to the application of the substitution 𝜃 to the assignment corresponding to Γ and tx. We define completeness of the symbolic execution relation SE𝑖 f correspondingly: Assumption 3 (Completeness of symbolic execution). Let C be a contract and f ∈ FC . Then the symbolic execution relation SE𝑖 f for function f and indexed by some index 𝑖, satisfies the following completeness property: tx −𝑣 . Γ −→ −𝑣 ) ∀Γ Γ ′ tx → Γ ′ ∧ tx = C.f(→

⇒ ∃𝜃 𝜑. ⟨𝜃, 𝜑⟩ ∈ SE𝑖f ∧ VC𝑖 (Γ, tx) |= 𝜑 ∧ VC𝑖 (Γ ′, tx) = VC𝑖 (Γ, tx) ◦ 𝜃

This statement expresses that for each concrete execution of transaction tx invoking function f from configuration Γ to configuration Γ ′ , there exists a symbolic execution result ⟨𝜃, 𝜑⟩ such that the condition 𝜑 is satisfied under the assignment corresponding to Γ and tx, and the assignment corresponding to Γ ′ corresponds to the application of the substitution 𝜃 to the assignment corresponding to Γ and tx. Note that we also can assume the following property: Assumption 4 (Agreement on condition variables). Let 𝜙 be a condition and V1 and V2 be assignments such that for all 𝑥 ∈ Vars(𝜙) it holds that V1 (𝑥) = V2 (𝑥). Then it holds that V1 |= 𝜙 ⇔ V2 |= 𝜙 This property states that if two assignments agree on the variables occurring in a condition, then they equivalently satisfy the condition. To avoid a full formalization of the concrete formula language with expressions, we assume the correctness of this lemma from now on. Finally, since we consider transaction execution to be deterministic, we will also require the symbolic execution relation to satisfy a strong determinism property, namely that if two path conditions can be satisfied by the same assignment, then they will also be mapped to the same expression. Assumption 5 (Determinism of symbolic execution). Let C be a contract and f ∈ FC . Then the symbolic execution relation SE𝑖 f for function f and indexed by some index 𝑖, satisfies the following property: ∀⟨𝜃 1, 𝜑 1 ⟩, ⟨𝜃 2, 𝜑 2 ⟩ ∈ SE𝑖f . (∃V.V |= 𝜑 1 ∧ V |= 𝜑 2 ) ⇒ ∀𝑥 ∈ XC,𝑖 f .𝜃 1 (𝑥) = 𝜃 2 (𝑥) Remark. This property is not directly a consequence from the soundness of the symbolic execution relation and the determinism of the smart contract semantics because technically a sound symbolic execution could still map path conditions that can be satisfied to the same assignment to syntactically different but semantically equivalent expressions.

On Identifying Sound Conditions for Frontrunning Resistance

D.1.2 Dependency Analysis. We define the data and control flow dependencies of variables in a contract C in terms of the symbolic execution relation SE𝑖 . f Definition D.1 (Data Flow Dependency). Let C be a smart contract and f be a function of C and SE𝑖 be a symbolic execution relation of f f. We define the set of data flow dependencies DDeps𝑖 (𝑥) ⊆ X𝑖 f C,f of variable 𝑥 ∈ X𝑖 in function f of contract C as C,f Ø DDeps𝑖f (𝑥) = Vars(𝜃 (𝑥))

Lemma D.5 (Soundness of Dependency Analysis). Let C be a smart contract and f be a function of C, and SE𝑖 be a symbolic execuf tion relation of f for some index 𝑖. Let Γ1 and Γ1 be two configurations −𝑣 ) be a transaction invoking function f of contract C and tx = C.f(→ and 𝑍 ⊆ XC be a set of contract variables such that 𝑥 ∈ 𝑍 . Further, let Ð 𝐷 = GC ∩ 𝑥 ∈𝑍 DDeps𝑖 (𝑥) ∪ CDeps𝑖 (𝑥) ∪ 𝑍 and assume Γ1 ≈𝐷 Γ1 . f f Then for all configurations Γ2 and Γ2 and observables 𝑥𝑠 and 𝑥𝑠 such tx

tx

𝑥𝑠

𝑥𝑠

that Γ1 −−→ Γ2 and Γ1 −−→ Γ2 , it holds that Γ2 ≈𝑍 Γ2 and 𝑥𝑠 = 𝑥𝑠.

⟨𝜃,𝜑 ⟩ ∈SE𝑖

f

To define control flow dependencies, we first introduce the notions of path conditions and relevant variables. Definition D.2 (Path Condition). Let C be a smart contract and f be a function of C and SE𝑖 be a symbolic execution relation of f. f We define the path condition PathCond𝑖f,𝑒 (𝑥) for variable 𝑥 ∈ X𝑖 , C,f expression 𝑒 and function f of contract C as Ü PathCond𝑖f,𝑒 (𝑥) := 𝜑 ⟨𝜃,𝜑 ⟩ ∈SE𝑖 :𝜃 (𝑥 )=𝑒

f

𝑖

Intuitively, PathCondf,𝑒 (𝑥) is the condition under which variable 𝑥 is assigned the expression 𝑒 in function f of contract C. Definition D.3 (Relevant variables). Let C be a smart contract and 𝜙 be a logical condition over variables in X𝑖 . We define the C,f relevant variables RelVars(𝜙) of condition 𝜑 as RelVars(𝜙) : {𝑥 ∈ Vars(𝜙) | ∃VV ′ . V |= 𝜙 ∧ ¬V ′ |= 𝜙 ∧ ∀𝑦 ∈ Vars(𝜙) \ {𝑥 }. V (𝑦) = V ′ (𝑦)} Intuitively, RelVars(𝜙) denotes all those variables that occur in 𝜙, which may change the satisfiability of 𝜙. We now can define the control dependencies CDeps𝑖 (𝑥) of a f variable 𝑥 in a function f as the relevant variables of the possible path conditions for assigning the variable 𝑥 to different expressions. Definition D.4 (Control Flow Dependency). Let C be a smart contract and f be a function of C, and SE𝑖 be a symbolic execution relaf tion of f. We define the set of control flow dependencies CDeps𝑖 (𝑥) ⊆ f X𝑖 of variable 𝑥 ∈ X𝑖 in function f of contract C as C,f C,f Ø CDeps𝑖f (𝑥) := RelVars(PathCond𝑖f,𝑒 (𝑥))

Proof. This follows directly from the previous definitions as well as the soundness and completeness of symbolic execution. □ Note that the set of dependencies 𝐷 here is defined to (i) also contain the variables 𝑍 itself to account for the case that tx does not change the value variables in 𝑍 and (ii) only considers those dependencies within the global variables GC . This last point accounts for the fact that the dependencies of 𝑥 may also contain local variables (denoting the local transaction execution context, like the sender of the transaction, or the arguments provided to the called function). The values of these local variables are fully determined by the transaction tx, so when considering two executions of tx, then the local variables will be assigned to the same values. D.1.3 Time Progress. We will, in the following, assume the existence of a specific function tick. The function tick models the specific transaction 𝜏 that increases the block number and is used to model the passage of time in the blockchain. We model tick as a function to enable a unified treatment within the symbolic execution framework. We can consider the tick function simply as a special function, with a well-defined semantics that can be freely scheduled by the attacker and that only modifies the block number variable by incrementing it by one and does not modify any other variable. The corresponding symbolic execution relation SE𝑖 is detick fined as follows: Definition D.6 (Symbolic Execution of tick). SE𝑖tick := {⟨Vtick, ⊤⟩} with Vtick defined by (

b+1 𝑥 =b Vtick (𝑥) := 𝑥 otherwise

𝑒 ∈ {𝑒 | ⟨𝜃,𝜑 ⟩ ∈SE𝑖 ∧ 𝜃 (𝑥 )=𝑒 }

f

Note that path conditions may have many irrelevant variables since they are simply the disjunctions of the conditions for different execution paths. For defining the control dependencies, we are only interested in those variables that are pivotal for deciding which expression the variable 𝑥 gets assigned. We can show that the dependency analysis defined above is sound with respect to concrete executions, meaning that whenever a transaction tx is executed in two configurations Γ1 and Γ1 that agree on the dependencies of variables 𝑍 , then this will result in the same assignments to 𝑍 . In particular, if 𝑍 contains the event variable 𝑥, then the two executions will also produce the same observables.

Note that b denotes the variable for the block number and is contained in X𝑖 for any contract C. It is straightforward to show C,f that the symbolic execution for tick is sound and complete for the semantics of the transaction 𝜏 that increases the block number. Lemma D.7 (Completeness of SE𝑖 ). Let C be an arbitrary tick contract. 𝜏

∀Γ Γ ′ . Γ −−→ Γ ′ ⇒ ∃𝜃 𝜑. ⟨𝜃, 𝜑⟩ ∈ SE𝑖tick ∧ VC𝑖 (Γ, 𝜏 ) |= 𝜑 𝑥𝑠

∧ 𝛿 (Γ ′ ) = (VC𝑖 (Γ, 𝜏 ) ◦ 𝜃 )(b)

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

Lemma D.8 (Soundness of SE𝑖 ). Let C be an arbitrary contick tract. ∀Γ 𝜃 𝜑. ⟨𝜃, 𝜑⟩ ∈ SE𝑖tick ∧ VC𝑖 (Γ, 𝜏 ) |= 𝜑 𝜏

⇒ ∃Γ ′ . Γ → − Γ ′ ∧ 𝛿 (Γ ′ ) = (VC𝑖 (Γ, 𝜏 ) ◦ 𝜃 )(b) D.1.4 Round-based user strategies. In the following, we will consider user strategies that proceed in rounds of 𝑘 blocks. More precisely, these user strategies decide upon a single contract transaction txC to schedule at the beginning of each round and then keep scheduling it for the following 𝑘 blocks. From now on, we will treat the parameter 𝑘, which denotes the length of a round, as a global parameter. We will further use notation 𝛿 (𝑅) to denote the block number Γ𝑅 .𝑏 of the last configuration Γ𝑅 of a run 𝑅. We define 𝜌 (Γ) := Γ.𝑏 − (Γ.𝑏 mod 𝑘) to denote the round of a configuration Γ and correspondingly 𝜌 (𝑅) := 𝜌 (Γ𝑅 ). The idea behind enforcing strategies to proceed in rounds is that they enable users to ensure that their transactions get processed before they decide upon the next transaction to schedule. This, in particular, ensures that an attacker cannot frontrun users with their own transactions. Definition D.9 (Round-based user strategies). Let Σ𝑟 ∈ W × C × N → L (X) (see Sec. 3.1) be an honest user strategy operating on configurations Γ = (𝑊, C, 𝑏) and returning a list of transactions ® = Σ𝑟 (Γ) such that | tx| ® ≤ 1 for all configurations Γ. Then we tx define the round-based strategy derived from Σ𝑟 (written Σ𝑟→ ) as follows: Σ𝑟→ (𝑅) := {tx ∈ Σ𝑟 (Γ𝑅1 )\TXs(𝑅2 ) | 𝑅 = 𝑅1 · 𝑅2 ∧ |blocks(𝑅1 ) | = 𝜌 (𝑅) }

f

Intuitively, NoWrite𝑖 (𝑥 ← − ·) is the condition under which variable 𝑥 is not modified in function f of contract C. Round Invariants. We define the notion of a round invariant. Intuitively, a pair (𝜙 𝑝 , 𝜙𝑖 ) denotes a round invariant if the fact that 𝜙 𝑝 holds at the beginning of a round implies that 𝜙𝑖 holds throughout the whole round. More formally, we define this property as follows: Definition D.11 (Round Invariant). Let 𝑘 be the length of a round. We say that a condition 𝜙𝑖 is a round invariant under precondition 𝜙 𝑝 (written RoundInv(𝜙 𝑝 , 𝜙𝑖 )) if the following holds ∀𝑟 ∈ N. ∀V. V |= 𝜙 𝑝 ∧ V (b) = 𝑟𝑘 ⇒ ∀𝑖 ∈ [0, . . . , 𝑘 − 1]. [V (b) → b + 𝑖] ◦ V |= 𝜙𝑖 Here b ∈ GC denotes the variable of the block number. We will additionally make use of the notion of a block-oblivious invariant. Intuitively, a logical condition 𝜙𝑖 is a block-oblivious invariant w.r.t. a function f if 𝜙𝑖 still holds after applying the possible effects that could have resulted from executing f in an arbitrary block of the current round. More formally Definition D.12 (Block-oblivious Invariant). We say that a condition 𝜙𝑖 is a block-oblivious invariant of a function f under a condition 𝜑 pre (written Inv𝑖 (f, 𝜑 pre, 𝜙𝑖 )) if the following holds ∀V, 𝜃, 𝜑, 𝑏.𝜌 (𝑏) = 𝜌 (V (b)) ∧ ⟨𝜃, 𝜑⟩ ∈ SE𝑖f ∧ V |= 𝜙𝑖 ∧ [b → 𝑏] ◦ V |= 𝜑 ∧ [b → 𝑏] ◦ V |= 𝜑 pre ⇒ [b → V (b)] ◦ (𝜃 ◦ ([b → 𝑏] ◦ V)) |= 𝜙𝑖

where blocks(𝑅) returns the blocks of run 𝑅 and TXs(𝑅) the transactions of 𝑅.

We use 𝜌 (𝑏) = 𝑏 − (𝑏 mod 𝑘) to denote the round of a block number.

Intuitively, a round-based user strategy Σ𝑟→ simply applies its round strategy Σ𝑟 at the beginning of each round and keeps on scheduling the transactions as mandated by Σ𝑟 (with exception of those that have already been successfully included in the blockchain) until the end of the round. Given a set of configuration-based strategies {Σ𝑖𝑟 }, we can canon→ ically lift it to arrive at a set {Σ𝑖𝑟 } of round-based honest user strategies.

Intuitively, this definition states that if an assignment V satisfies the invariant 𝜙𝑖 and this assignment would satisfy the prerequisites for execution f in some block 𝑏 of the same round (denoted by satisfaction of the path condition 𝜑 and the precondition 𝜑 pre ), then performing the same updates to V would leave the invariant intact. In particular, we will use the previously stated properties to make use of the following lemma:

D.2

Soundness of interaction condition synthesis

We now define the soundness of the interaction condition synthesis algorithm. Note that in the following, we may omit proofs of simple lemmas that are direct implications of existing definitions or previously established results. For stating the algorithm, we will make use of the following helper definitions: Definition D.10 (No Write Condition). Let C be a smart contract and f be a function of C and SE𝑖 be a symbolic execution relation f f of f. We define the no write condition NoWrite𝑖 (𝑥 ← − ·) for variable 𝑖 𝑥 ∈ X in function f of contract C as C,f f

NoWrite𝑖 (𝑥 ← − ·) := PathCond𝑖f,𝑥 (𝑥)

Lemma D.13 (Preservation of invariants through rounds). Let 𝜙𝑖 and 𝜙 𝑝 be conditions such that RoundInv(𝜙 𝑝 , 𝜙𝑖 ). Let Γ1 , Γ2 , . . . , Γ𝑛 be configurations such that 𝜌 (Γ𝑗 ) = 𝜌 (Γ𝑙 ) for 𝑗, 𝑙 ∈ {1, . . . , 𝑛} tx1

tx2

tx𝑛−1

and 𝛿 (Γ1 ) mod 𝑘 = 0. Further, let Γ1 −−→ Γ2 −−→ . . . −−−−→ Γ𝑛 for transaction tx1, . . . tx𝑛−1 such that for all 𝑗 ∈ {1, . . . 𝑛 − 1}, it −𝑣 ) for some f ∈ F s.t. holds that either tx 𝑗 = 𝜏 or tx 𝑗 = C.f(→ C Inv𝑖 (f, 𝜑 pre, 𝜙𝑝 ) holds for some index 𝑖 and 𝜑 pre with VC𝑖 (Γ𝑗 , tx 𝑗 ) |= 𝜑 pre . Then if VC𝑖 (Γ1, tx) |= 𝜙 𝑝 for some tx and index 𝑖 it also holds that VC𝑖 (Γ𝑛 , tx) |= 𝜙𝑖 . Proof. To prove this lemma, we first show by induction over the ® that if VC𝑖 (Γ1, tx) |= 𝜙 𝑝 then also [b → VC𝑖 (Γ1, tx) (b)] ◦ length of tx 𝑖 VC (Γ𝑛 , tx) |= 𝜙 𝑝 . The cases follow immediately by the Definition D.12 (and the soundness and completeness of the symbolic execution). Finally, we can use Definition D.11 to conclude from [b → VC𝑖 (Γ1, tx)(b)] ◦ VC𝑖 (Γ𝑛 , tx) |= 𝜙 𝑝 that also VC𝑖 (Γ𝑛 , tx) |= 𝜙𝑖 (since

On Identifying Sound Conditions for Frontrunning Resistance

f VC𝑖 (Γ𝑛 , tx) = [b → VC𝑖 (Γ𝑛 , tx)(b)]◦([b → VC𝑖 (Γ1, tx)(b)] ◦ VC𝑖 (Γ𝑛 , tx))). Algorithm 2 Synthesis of condition FRu (𝑥 ← − 𝑒) □ Require: Smart contract C, user u, function f ∈ FC , symbolic exeIntuitively, this lemma states that if (𝜙 𝑝 , 𝜙𝑖 ) is a round invariant cution relations {SE𝑖g }g ∈ FC ∪{ tick },𝑖 ∈ {u,¬u} over the respective and if 𝜙 𝑝 holds at the beginning of a round, then 𝜙𝑖 holds throughout XC,𝑖 g , variable 𝑥 ∈ GC , expression 𝑒 ∈ E u f the whole round as long as only transactions get executed for which f f 1: FRu (𝑥 ← − 𝑒) ← getRI (PathCondu (𝑥 ← − 𝑒)) 𝜙 𝑝 is a block-oblivious invariant. 2: 𝑊 ← ∅, 𝐷 ← ∅ Constructing Interaction Conditions. Our algorithms will itera3: if 𝑒 ≠ 𝑥 then f tively build pairs of conditions (𝜙 𝑝 , 𝜙𝑖 ) that together constitute 4: 𝐷 ← DDepsu (𝑥 ← − ·) ∪ {𝑥 } round invariants. To this end, we will define two functions getRI 5: for all 𝑦 ∈ 𝐷, g ∈ FC ∪ {tick} do and mergeRI such that for a condition 𝜙, getRI (𝜙) returns a round g 6: 𝜑 ← ∀ℓ ∈ L ¬u sender¬u ≠ u → NoWrite¬u (𝑦 ← − ·) invariant (𝜙 𝑝 , 𝜙𝑖 ) such that 𝜙𝑖 is equivalent to 𝜙 (𝜙𝑖 ≡ 𝜙) and g f f mergeRI ((𝜙 𝑝′ , 𝜙𝑖′ ), (𝜙 𝑝 , 𝜙𝑖 )) returns a round invariant (𝜙 𝑝 , 𝜙𝑖 ) such 7: FRu (𝑥 ← − 𝑒) ← mergeRI (FRu (𝑥 ← − 𝑒), getRI (𝜑)) 8: 𝑊 ← 𝑊 ∪ {(𝑦, g)} that 𝜙𝑖 ≡ 𝜙𝑖′ ∧ 𝜙𝑖 . 9: done ← false For the theoretical treatment, we will axiomatize the properties f of getRI and mergeRI as follows: − 𝑒)) × FC ⊈ 𝑊 ∧ done = false do 10: while Vars(FRu (𝑥 ← 11: done ← true Assumption 6 (Round Invariant Generation). Let 𝜙 be a logi12: for all g ∈ FC do 𝑖 cal condition (over X for some f ∈ FC and index 𝑖). Further, let f C,f 13: (𝜙 𝑝 , 𝜙𝑖 ) ← FRu (𝑥 ← − 𝑒) (𝜙 𝑝 , 𝜙𝑖 ) = getRI (𝜙) for logical conditions 𝜙 𝑝 , 𝜙𝑖 (over X𝑖 ). Then, the ¬u C,f 14: if Inv (g, sender¬u ≠ u, 𝜙 𝑝 ) then following hold: 15: continue • RoundInv(𝜙𝑝 , 𝜙𝑖 ) 16: done ← false f • ∀V. V |= 𝜙𝑖 ⇔ V |= 𝜙 − 𝑒)) \ {𝑧 | (𝑧, g) ∈ 𝑊 } 17: 𝑦 ← Vars(FRu (𝑥 ← g Note that getRI is guaranteed to exist, since getRI (𝜙) := (⊥, 𝜙) 18: 𝜑 ← ∀ℓ ∈ L ¬u sender¬u ≠ u → NoWrite¬u (𝑦 ← − ·) g is a trivial implementation that satisfies the above properties. In f f − 𝑒) ← mergeRI (FRu (𝑥 ← − 𝑒), getRI (𝜑)) 19: FRu (𝑥 ← practice, we can implement getRI by using heuristics to compute 20: 𝑊 ← 𝑊 ∪ {(𝑦, g)} more interesting round preconditions 𝜙𝑝 , which we then check to f indeed satisfy the desired properties. E.g., in cases where 𝜙 does not 21: return FRu (𝑥 ← − 𝑒) contain the block number b, getRI (𝜙) := (𝜙, 𝜙) provides relevant round invariants. Simple strengthenings that we attempt in case f that 𝜙 contains the block number b is to substitute b in 𝜙 with • Backrunning conditions BRu (𝑍 ⊥[𝑥 ← −]) that ensure that b + 𝑘 − 1. when an honest user u writes a variable 𝑥 using function f, then this will not interfere with how the attacker can 1 2 1 2 Assumption 7 (Round Invariant Composition). Let 𝜙 𝑝 , 𝜙 𝑝 , 𝜙𝑖 , 𝜙𝑖 concurrently assign variables in the set 𝑍 . In particular, this 𝑖 be logical conditions (over X for some f ∈ FC and index 𝑖) such C,f means that the attacker may not perform concurrent acthat RoundInv(𝜙 𝑝1 , 𝜙𝑖1 ) and RoundInv(𝜙 𝑝2 , 𝜙𝑖2 ). Further, let (𝜙 𝑝 , 𝜙𝑖 ) = tions in which the assignment of variables in 𝑍 may depend mergeRI ((𝜙 𝑝1 , 𝜙𝑖1 ), (𝜙 𝑝2 , 𝜙𝑖2 )) for logical conditions 𝜙 𝑝 , 𝜙𝑖 (over X𝑖 ). on the variable 𝑥, either directly (via data dependencies) or C,f indirectly (via control dependencies). Then, the following hold: f

• RoundInv(𝜙𝑝 , 𝜙𝑖 ) • ∀V. V |= 𝜙𝑖 ⇔ V |= 𝜙𝑖1 ∧ 𝜙𝑖2 Note that a trivial implementation of mergeRI would be mergeRI ((𝜙 𝑝1 , 𝜙𝑖1 ), (𝜙 𝑝2 , 𝜙𝑖2 )) := (𝜙𝑝1 ∧ 𝜙 𝑝2 , 𝜙𝑖1 ∧ 𝜙𝑖2 ) In practice, we perform simplifications to reduce the number of variables occurring in the final round invariant (𝜙 𝑝 , 𝜙𝑖 ). We now devise algorithms for computing interaction conditions that cover two different scenarios f

• Frontrunning conditions FRu (𝑥 ← − 𝑒) that ensure that a call of honest user u to function f will deterministically assign the value of variable 𝑥 according to expression 𝑒. In particular, this means that concurrent attacker actions may neither deviate the control flow of the execution so that the execution will assign another expression 𝑒 ′ ≠ 𝑒 to 𝑥, nor may attacker actions change the variables in 𝑒 so that the execution of f would lead to a different assignment for 𝑥.

Algorithm 2 for generating FRu (𝑥 ← − 𝑒) proceeds as follows: Starting from the path condition for assigning 𝑥 to expression 𝑒, it refines the condition by (1) excluding writes (by the attacker) to all variables on which 𝑥 has a data dependency (provided that 𝑒 indicates a proper assignment to 𝑥); (2) excluding writes (by the attacker) to all variables on which 𝑥 has control dependencies until an invariant is found that holds for all possible attacker interactions. Note that the algorithm is guaranteed to terminate, since if not terminating before (due to successfully finding an invariant), eventually 𝑊 will contain all combinations of contract variables and contract functions, causing a termination of the outer while loop. f

Algorithm 3 for computing BRu (𝑍 ⊥[𝑥 ← −]) proceeds similarly to the previous one. It starts with the condition ⊤ and first excludes writes to all variables 𝑦 that have a data dependency on 𝑥. For variables 𝑦 that have a control dependency on 𝑥, it is ensured that the condition implies a path condition of a specific expression 𝑒,

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

f

Algorithm 3 Synthesis of condition BRu (𝑍 ⊥[𝑥 ← −]) Require: Smart contract C, user u, function f ∈ FC ∪ {tick}, symbolic execution relations {SE𝑖g }g ∈ FC ∪{ tick },𝑖 ∈ {u,¬u} over the respective XC,𝑖 g , variable 𝑥 ∈ GC , set 𝑍 ⊆ GC

the respective XC,𝑖 g , 𝑥 ∈ GC , 𝑒 ∈ E u . Let FRu (𝑥 ← − 𝑒) = (Φpre, Φinv ) f be the result of Algorithm 1. The following properties hold f

Φinv ⊨ PathCondu (𝑥 ← − 𝑒) fr

f

1: BRu (𝑍 ⊥[𝑥 ← −]) ← (⊤, ⊤)

𝑥 ≠ 𝑒 ⇒ ∀𝑦 ∈ DDepsu (𝑥 ← − ·) ∪ {𝑥 }, g ∈ FC ∪ {tick}. !

3: for all (𝑦, g) ∈ 𝐷 do g

𝜑 ← ∀ℓ ∈ L ¬u sender¬u ≠ u → NoWrite¬u (𝑦 ← − ·) g f f −]) ← mergeRI (BRu (𝑍 ⊥[𝑥 ← −]), getRI (𝜑)) 5: BRu (𝑍 ⊥[𝑥 ← 6: 𝑊 ← 𝑊 ∪ {(𝑦, g)} 7: 𝐶 ← {(𝑦, g) ∈ 𝑍 × FC | 𝑥 ∈ CDeps𝑖g (𝑦)} 8: for all (𝑦, g) ∈ 𝐶 do 9: 𝑒 ← select({𝑒 | ⟨𝜃, 𝜑⟩ ∈ SE¬u g ∧ 𝜃 (𝑦) = 𝑒})

∀ sender ≠ u → NoWrite (𝑦 ←− ·) (2)

fr Φinv ⊨

¬u

g

g f f BRu (𝑍 ⊥[𝑥 ← −]) ← mergeRI (BRu (𝑍 ⊥[𝑥 ← −]), getRI (𝜑)) 12: done ← false f

13: while Vars(BRu (𝑍 ⊥[𝑥 ← −])) × FC ⊈ 𝑊 ∧ done = false do 15: 16: 17:

done ← true f (𝜙 𝑝 , 𝜙𝑖 ) ← BRu (𝑍 ⊥[𝑥 ← −]) u u if ¬Inv (f, sender = u, 𝜙 𝑝 ) then done ← false f

𝑦 ← Vars(BRu (𝑍 ⊥[𝑥 ← −])) \ {𝑧 | (𝑧, f) ∈ 𝑊 }

19:

−]) ← mergeRI (BRu (𝑍 ⊥[𝑥 ← −]), BRu (𝑍 ⊥[𝑥 ←

f

f

f

20:

getRI (NoWriteu (𝑦 ← − ·))) 𝑊 ← 𝑊 ∪ {(𝑦, f)} for all g ∈ FC do f

22: 23: 24: 25:

(3)

RoundInv¬u (Φpre, Φinv )

(4)

fr

fr

fr

fr

Vars(Φpre ) ⊆ XC,u f

(5)

fr

Vars(Φinv ) ⊆ XC,u f

(6)

Correspondingly, we can define the characteristic properties of the backrunning conditions:

18:

21:

∀g ∈ FC .Inv¬u (g, sender¬u ≠ u, Φpre )

g ¬u ¬u sender¬u ≠ u → PathCond (𝑦 ← − 𝑒)

11:

14:

g

¬u

ℓ ∈ L ¬u

4:

𝜑 ← ∀ℓ ∈ L

(1) f

g

2: 𝐷 ← {(𝑦, g) ∈ 𝑍 × FC | 𝑥 ∈ DDeps¬u (𝑦 ← − ·) ∨ 𝑥 = 𝑦}

10:

fr

fr

−]) (𝜙 𝑝 , 𝜙𝑖 ) ← BRu (𝑍 ⊥[𝑥 ← if Inv¬u (g, sender¬u ≠ u, 𝜙 𝑝 ) then continue done ← false

Lemma D.15 (Characteristic properties of the backrunning condition). Let C be a smart contract, u ∈ Hon, f ∈ FC , 𝑍 ⊆ X u , {SE𝑖g }g ∈ FC ∪{ tick },𝑖 ∈ {u,¬u} symbolic execution reC,f f lations over the respective XC,𝑖 g , 𝑥 ∈ GC , 𝑒 ∈ E u . Let BRu (𝑍 ⊥[𝑥 ← −]) = f br (Φbr pre , Φinv ) be the result of Algorithm 3. The following properties hold g

∀𝑦 ∈ 𝑍, g ∈ FC . (𝑥 ∈ DDeps¬u (𝑦 ← − ·) ∨ 𝑦 = 𝑥) ⇒ Φbr inv ⊨

∀ sender ≠ u → NoWrite (𝑦 ←− ·) ¬u

!

g

¬u

(7)

ℓ ∈ L ¬u

g

f

26: 27: 28: 29:

𝑦 ← Vars(BRu (𝑍 ⊥[𝑥 ← −])) \ {𝑧 | (𝑧, g) ∈ 𝑊 } g 𝜑 ← ∀ℓ ∈ L ¬u sender¬u ≠ u → NoWrite¬u (𝑦 ← − ·) g f f BRu (𝑍 ⊥[𝑥 ← −]) ← mergeRI (BRu (𝑍 ⊥[𝑥 ← −]), getRI (𝜑)) 𝑊 ← 𝑊 ∪ {(𝑦, g)}

¬u ∀𝑦 ∈ 𝑍, g ∈ FC . 𝑥 ∈ CDeps¬u g (𝑦) ⇒ ∃𝑒 ∈ Eg .

Φbr inv ⊨

∀ sender ≠ u → PathCond (𝑦 ←− 𝑒) ¬u

¬u

!

g

(8)

ℓ ∈ L ¬u

g

f

30: return BRu (𝑍 ⊥[𝑥 ← −])

ensuring that writing 𝑥 (using f) can not change the way how a(nother) function g writes 𝑦. Finally, writes to all variables of the conditions are prohibited until establishing an invariant both for adversarial function executions as well as the execution of f by the honest user. D.2.1 Characteristic Properties. We state the characteristic properties of the frontrunning and backrunning conditions. We first provide the characteristic properties of the frontrunning conditions: Lemma D.14 (Characteristic properties of the frontrunning condition). Let C be a smart contract, u ∈ Hon, f ∈ FC , {SE𝑖g }g ∈ FC ∪{ tick },𝑖 ∈ {u,¬u} symbolic execution relations over

Invu (f, senderu = u, Φbr pre )

(9)

∀g ∈ FC .Inv¬u (g, sender¬u ≠ u, Φbr pre )

(10)

br RoundInv¬u (Φbr pre , Φinv )

(11)

u Vars(Φbr pre ) ⊆ XC,f

(12)

u Vars(Φbr inv ) ⊆ XC,f

(13)

Note that both lemmas follow immediately from the construction of the algorithm provided that getRI provides round invariant and mergeRI preserves round invariants.

On Identifying Sound Conditions for Frontrunning Resistance

D.2.2 Semantic notions of frontrunning and backrunning conditions. The frontrunning and backrunning conditions produced by the algorithms are specific to individual variables 𝑥, which may be changed by an honest user transaction. For formulating requirements for the kind of transactions tx that an honest user may submit at the beginning of a round, we want to ensure that those transactions keep a specific relevant set of variables (denoted as 𝑍 in the following) to be unaffected by the possible deckstacking attacks. To this end, on the one side, it needs to be ensured that the effects that tx has on 𝑍 are deterministicht within the round (so scheduling attacker transactions before tx) may not change how tx assigns variables in 𝑍 . This can be realized by assuring that frontrunning conditions hold for all variables 𝑥 in 𝑍 . On the other side, it also needs to be ensured that if tx changes variables (that could also lie outside of 𝑍 ), this cannot affect how attacker transactions again write variables in 𝑍 . To ensure this, it needs to be established that the backrunning conditions (for 𝑍 ) hold for all variables 𝑥 that are written by tx. Following these intuitions, we establish predicates FRu (Γ, tx, 𝑍 ) and BRu (Γ, tx, 𝑍 ), which capture this intuition. Namely FRu (Γ, tx, 𝑍 ) will express that submitting transaction tx in configuration Γ will ensure that writes to variables in 𝑍 cannot be affected by frontrunning, and BRu (Γ, tx, 𝑍 ) will express that by backrunning the transaction tx an attacker cannot change the variables in 𝑍 . f

In the following, we consider frontrunning conditions FRu (𝑥 ← − fr fr fr fr fr 𝑒) to be of the form (Φpre, Φinv ) where Φpre ⊨ Φinv and Φpre denotes the precondition that needs to hold at the beginning of the round fr in order to ensure that Φinv holds within the whole round. We define the following helper predicates operating on assignments that we will then use to define the predicates FRu (·, ·, ·) and BRu (·, ·, ·). Definition D.16. Let C be a smart contract, u ∈ Hon, f ∈ FC , 𝑍 ⊆ GC , V with an assignment over X u , and SEu a symbolic f C,f execution relation over X u . We define C,f Û fr FRuf (V, 𝑍 ) := Φinv fr

sender(tx) = u and Γ be a configuration. We define FRu (Γ, tx, 𝑍 ) := VCu (Γ, tx) |= FRuf (VCu (Γ, tx), 𝑍 ) So intuitively, FRu (Γ, tx, 𝑍 ) denotes the condition on a configuration Γ and transaction tx, which ensures that concurrent attacker transactions cannot interfere with how tx writes the variables in 𝑍 . We can provide similar definitions for the backrunning condition: Definition D.18. Let C be a smart contract, u ∈ Hon, f ∈ FC , 𝑍 ⊆ GC , V with an assignment over X u , and SEu a symbolic f C,f execution relation over X u . We define C,f Û u BRf,𝑍 (V) := Φbr inv br (Φbr pre ,Φinv ) ∈𝑆

where f

−]) | 𝑥 ∈ GC ∧ ⟨𝜃, 𝜑⟩ ∈ SEuf 𝑆 = {BRu (𝑍 ⊥[𝑥 ← ∧ 𝜃 (𝑥) = 𝑒 ∧ V |= 𝜑 ∧ 𝑒 ≠ 𝑥 } Intuitively, BRu (V) denotes the conjunction for all backrunf,𝑍 ning conditions that enforce that variables in 𝑍 may not be influenced by variables that are written when executing f following the assignment V (which in particular contains the assignment of the argument variables for the function call to f). Note that this definition considers that V may induce changes in any variable 𝑥 of the contract (when executing f), but it ensures that for all such f

variables 𝑥, BRu (𝑍 ⊥[𝑥 ← −]) holds, ensuring that changes to such variables leave the variables in 𝑍 unaffected. Again, we provide a definition that caters to the transaction setting (instead of operating on assignments): Definition D.19 (Backrunning condition). Let C be a smart contract, u ∈ Hon, f ∈ FC and SEu a symbolic execution relation f −𝑣 ) for some arguments → −𝑣 and over X u . Further let tx = C.f(→ C,f sender(tx) = u and Γ be a configuration. We define BRu (Γ, tx, 𝑍 ) := VCu (Γ, tx) |= BRuf,V u (Γ,tx) (𝑍 )

fr

(Φpre ,Φinv ) ∈𝑆

where f

𝑆 = {FRu (𝑥 ← − 𝑒) | 𝑥 ∈ 𝑍 ∧ ⟨𝜃, 𝜑⟩ ∈ SEuf ∧ 𝜃 (𝑥) = 𝑒 ∧ V |= 𝜑 } Intuitively, FRu (V, 𝑍 ) denotes the conjunction for all frontf running conditions that enforce that variables in 𝑍 are assigned as mandated by V (which in particular contains the assignment of the argument variables for the function call to f). Remark. Note that we implicitly assume the existence of a smart contract C and corresponding symbolic execution relations for all of its functions and do not always make this assumption explicit in the lemmas of this section.

C

So intuitively, BRu (Γ, tx, 𝑍 ) denotes the condition on a configuration Γ and transaction tx, which ensures that the way that concurrent attacker transactions write variables in 𝑍 does not depend on how the transaction tx changes any (!) variables. We provide analogous definitions to the previous ones for the round preconditions for frontrunning and backrunning. Definition D.20. Let C be a smart contract, u ∈ Hon, f ∈ FC , 𝑍 ⊆ GC , V with an assignment over X u , and SEu a symbolic f C,f execution relation over X u . We define C,f Û fr u pFRf (V, 𝑍 ) := Φpre fr

fr

(Φpre ,Φinv ) ∈𝑆

We provide a definition that caters to the transaction setting (instead of operating on assignments):

where f

Definition D.17 (Frontrunning condition). Let C be a smart contract, u ∈ Hon, f ∈ FC and SEu a symbolic execution relation f −𝑣 ) for some arguments → −𝑣 and over X u . Further let tx = C.f(→ C,f

𝑆 = {FRu (𝑥 ← − 𝑒) | 𝑥 ∈ 𝑍 ∧ ⟨𝜃, 𝜑⟩ ∈ SEuf ∧ 𝜃 (𝑥) = 𝑒 ∧ V |= 𝜑 } Definition D.21 (Frontrunning round condition). Let C be a smart contract, u ∈ Hon, f ∈ FC and SEu a symbolic execution relation f

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

−𝑣 and −𝑣 ) for some arguments → over X u . Further let tx = C.f(→ C,f sender(tx) = u and Γ be a configuration. We define FRu𝜌 (Γ, tx, 𝑍 ) := VCu (Γ, tx) |= pFRuf (VCu (Γ, tx), 𝑍 ) Definition D.22. Let C be a smart contract, u ∈ Hon, f ∈ FC , 𝑍 ⊆ GC , V an assignment over X u , and SEu a symbolic execution f C,f relation over X u . We define C,f Û pBRuf,𝑍 (V) := Φbr pre br (Φbr pre ,Φinv ) ∈𝑆

where f

−]) | ⟨𝜃, 𝜑⟩ ∈ SEuf ∧ 𝜃 (𝑥) = 𝑒 ∧ V |= 𝜑 ∧ 𝑒 ≠ 𝑥 } 𝑆 = {BRu (𝑍 ⊥[𝑥 ← Definition D.23 (Backrunning condition). Let C be a smart contract, u ∈ Hon, f ∈ FC and SEu a symbolic execution relation f −𝑣 and −𝑣 ) for some arguments → over X u . Further let tx = C.f(→ C,f sender(tx) = u and Γ be a configuration. We define BRu𝜌 (Γ, tx, 𝑍 ) := VCu (Γ, tx) |= pBRuf,V u (Γ,tx) (𝑍 )

Definition D.26 (Write sets). Let C be a contract with variables XC . −𝑣 ), 𝑖 Let Γ be a configuration, tx a transaction such that tx = C.f(→ be an index variable and SE𝑖 be a symbolic execution relation over f X𝑖 and 𝑍 ⊆ XC . C,f Writes (Γ, tx, 𝑍 ) := {𝑥 ∈ 𝑍 | ⟨𝜃, 𝜑⟩ ∈ SEuf ∧ 𝜃 (𝑥) = 𝑒 ∧ VC𝑖 (Γ, tx) |= 𝜑 ∧ 𝑒 ≠ 𝑥 } Intuitively, Writes (Γ, tx, 𝑍 ) denotes the set of variables from 𝑍 , which are written by the transaction tx when executed in configuration Γ. We establish some useful properties of write sets. First, we can show that all variables from 𝑍 , which are not contained in the write set Writes (Γ, tx, 𝑍 ) stay unchanged when executing tx in Γ: Lemma D.27 (Preservation of variables outside write set). Let C be a contract and 𝑍 ⊆ GC a set of variables. Let Γ1 and Γ2 be tx

configurations and tx a transaction such that Γ1 − → Γ2 . Then it holds that Γ1 ≈𝑍 \Writes (Γ1 ,tx,𝑍 ) Γ2

C

We can establish the following properties for the combined frontrunning and backrunning conditions, which are immediately inherited from the definitions of the individual frontrunning and backrunning conditions.

Next, we can show that two configurations that agree on the control dependencies of some set of variables 𝑍 also write the same variables from 𝑍 :

Lemma D.24. Let C be a smart contract, u ∈ Hon, f ∈ FC , 𝑍 ⊆ GC , V an assignment over X u , and {SE𝑖g }g ∈ FC ∪{ tick },𝑖 ∈ {u,¬u} symbolic C,f execution relations over the respective XC,𝑖 g . Then it holds that

Lemma D.28 (Agreement of write sets). Let C be a contract and 𝑍 ⊆ GC a set of variables. Let Γ and Γ be configurations and −𝑣 ) be a transaction invoking function f of contract C. If for tx = C.f(→ Ð 𝐶 = GC ∩ 𝑥 ∈𝑍 CDeps𝑖 (𝑥) (for some index 𝑖) it holds that f

RoundInv (pFRuf (V, 𝑍 ), FRuf (V, 𝑍 ))

Γ ≈𝐶 Γ then also

and ¬u

Inv (g, sender

¬u

≠ u, pFRf (V, 𝑍 ))

Proof. Follows immediately from the definitions of pFRu (V, 𝑍 ), f FRu (V, 𝑍 ), pBRu (V), BRu (V), and the characteristic propf f,𝑍 f,𝑍 erties of the frontrunning and backrunning conditions. □ Lemma D.25. Let C be a smart contract, u ∈ Hon, f ∈ FC ∪ {tick}, 𝑍 ⊆ GC , V an assignment over X u , and {SE𝑖g }g ∈ FC ∪{ tick },𝑖 ∈ {u,¬u} C,f symbolic execution relations over the respective XC,𝑖 g . Then it holds that RoundInv (pBRuf,𝑍 (V), BRuf,𝑍 (V)) and ¬u

Inv (f, sender

¬u

Writes (Γ, tx, 𝑍 ) = Writes (Γ, tx, 𝑍 )

u

u

≠ u, pBRf,V (𝑍 ))

and for all g ∈ FC that Inv¬u (g, sender¬u ≠ u, pBRuf,V (𝑍 ))

We further provide the following helper notion of a write set that will come in handy.

D.2.3 Correctness of Frontrunning and Backrunning Conditions. We next establish the semantic correctness properties for the semantic frontrunning and backrunning predicates that we established before. First, we make the assumption concerning the connection between written variables and produced observables explicit: Assumption 8 (Unique observables). Let Γ1 and Γ2 be configurations −𝑣 ) be a transaction calling function f ∈ F . Let 𝑥 ∈ and tx = C.f(→ C f 𝑋 Ev be the event variable of f and 𝑍 ⊆ GC such that 𝑥 f ∈ 𝑣𝑆𝑒𝑡. If tx

Γ1 −−→ Γ2 for some observable 𝑥𝑠 then the following holds 𝑥𝑠

• |𝑥𝑠 | ≤ 1 • 𝑥 f ∈ Writes (Γ1, tx, 𝑍 ) ⇒ 𝑥𝑠 = [⟨𝑥 f : Γ2 .S C (𝑥 f )⟩] • ∀𝑥 𝑣. 𝑥𝑠 = [⟨𝑥 : 𝑣⟩] ⇒ 𝑥 = 𝑥 f ∧ 𝑥 f ∈ Writes (Γ1, tx, 𝑍 ) Note that this assumption requires that every transaction produces at most one observable (first condition) and that it produces an observable exactly when its corresponding event variable 𝑥 f is written, which then contains the value assigned to this variable (the last two conditions). We formulate this condition in terms of write sets since this provides us with a convenient way to characterize

On Identifying Sound Conditions for Frontrunning Resistance

when a transaction execution writes a variable. A purely semantic notions (which would consider changes to the values assigned to the event variable in Γ1 and Γ2 would fall short of adequately characterizing when the same event is recorded two times in a row.) We first state the core correctness lemma for the semantic frontrunning conditions, which intuitively says that if FRu (Γ, txu, 𝑍 ) holds for a transaction txu then placing an adversarial transaction tx𝐴 before txu will not affect the behavior of txu (on the variables 𝑍 ). More specifically, this means that if txu writes variables then those transactions will be written to the same values as they would be when executing txu without tx𝐴 . Similarly, if executing txu leaves variables unchanged then this should be also the case when executing tx𝐴 before. Note that if the event variables 𝑋 Ev are contained in 𝑍 then this additionally implies that executing txu will produce the same observables (independently of whether tx𝐴 was executed before) because observables are produced exactly if the corresponding event variables are written. Formally, we capture this property with the following lemma. u

Lemma D.29 (Correctness of FR (·, ·, ·) for attacker transactions). Let Γ1 , Γ2 and Γ3 be configurations and txu be a transaction such that sender(txu ) = u for u ∈ Hon, and 𝑍 be a set of variables such that 𝑋 Ev ⊆ 𝑍 . Further, let tx𝐴 be a transaction such that sender(tx𝐴 ) ≠ u. Assume that FRu (Γ1, txu, 𝑍 ) hold and that tx𝐴

txu

𝑥𝑠𝐴

𝑥𝑠 m

Γ1 −−−→ Γ2 −−−→ Γ3

Proof. This property follows directly from the soundness and correctness of symbolic execution, as well as from the characteristic properties of backrunning conditions. □ Similar correctness lemmas hold for the semantic backrunning conditions. This lemma states in a similar fashion that if BRu (Γ, txu, 𝑍 ) holds in a configuration then placing the transaction txu before an (adversarial) transaction tx𝐴 does not change the effect of tx𝐴 (on 𝑍 ). Lemma D.31 (Correctness of BRu (·, ·, ·) for honest user transactions). Let Γ1 , Γ2 and Γ3 be configurations and txu be a transaction such that sender(txu ) = u for u ∈ Hon, and 𝑍 be a set of variables such that 𝑋 Ev ⊆ 𝑍 . Further, let tx𝐴 be a transaction such that sender(tx𝐴 ) ≠ u. Assume that BRu (Γ1, txu, 𝑍 ) hold and that txu

tx𝐴

𝑥𝑠 m

𝑥𝑠𝐴

Γ1 −−−→ Γ2 −−−→ Γ3 Then it holds that tx𝐴

• For all configurations Γ2 such that Γ1 −−−→ Γ2 , it holds that 𝑥𝑠𝐴

Γ3 ≈Writes (Γ1 ,tx𝐴 ,𝑍 ) Γ2 ∧ 𝑥𝑠𝐴 = 𝑥𝑠𝐴 • It holds that Γ2 ≈𝑍 \Writes (Γ1 ,tx𝐴 ,𝑍 ) Γ3 A similar correctness lemma holds for backrunning conditions with respect to 𝜏 transactions (which similarly to honest user transactions, may not impact the behavior of attacker transactions).

Then it holds that txu

• For all configurations Γ2 such that Γ1 −−−→ Γ2 , it holds that 𝑥𝑠 m

Γ3 ≈Writes (Γ1 ,txu ,𝑍 ) Γ2 ∧ 𝑥𝑠 m = 𝑥𝑠 m • It holds that Γ2 ≈𝑍 \Writes (Γ1 ,txu ,𝑍 ) Γ3

Lemma D.32 (Correctness of BRu (·, ·, ·) for 𝜏 transactions). Let Γ1 , Γ2 and Γ3 be configurations and 𝑍 be a set of variables such that 𝑋 Ev ⊆ 𝑍 and u ∈ Hon be a user. Further, let tx𝐴 be a transaction such that sender(tx𝐴 ) ≠ u. Assume that BRu (Γ1, 𝜏 , 𝑍 ) and 𝜌 (Γ1 ) = 𝜌 (Γ2 ) hold and that tx𝐴 𝜏 Γ1 → − Γ2 −−−→ Γ3 𝑥𝑠𝐴

Proof. This property follows directly from the soundness and correctness of symbolic execution, as well as from the characteristic properties of frontrunning conditions. □ We can show a similar correctness lemma for 𝜏 transactions, which shows that the frontrunning condition rules out interference with 𝜏 .

Then it holds that tx𝐴

• For all configurations Γ2 such that Γ1 −−−→ Γ2 , it holds that 𝑥𝑠𝐴

Γ3 ≈Writes (Γ1 ,tx𝐴 ,𝑍 ) Γ2 ∧ 𝑥𝑠𝐴 = 𝑥𝑠𝐴 • It holds that Γ2 ≈𝑍 \Writes (Γ1 ,tx𝐴 ,𝑍 ) Γ3

u

Lemma D.30 (Correctness of FR (·, ·, ·) for 𝜏 transactions). Let Γ1 , Γ2 and Γ3 be configurations and txu be a transaction such that sender(txu ) = u for u ∈ Hon, and 𝑍 be a set of variables such that 𝑋 Ev ⊆ 𝑍 . Assume that FRu (Γ1, txu, 𝑍 ) and 𝜌 (Γ1 ) = 𝜌 (Γ2 ) hold and that txu 𝜏 Γ1 → − Γ2 −−−→ Γ3 𝑥𝑠 m

Then it holds that txu

• For all configurations Γ2 such that Γ1 −−−→ Γ2 , it holds that 𝑥𝑠 m

Γ3 ≈Writes (Γ1 ,txu ,𝑍 ) Γ2 ∧ 𝑥𝑠 m = 𝑥𝑠 m • It holds that Γ2 ≈𝑍 \Writes (Γ1 ,txu ,𝑍 ) Γ3

Proof. This property follows directly from the soundness and correctness of symbolic execution, as well as from the characteristic properties of backrunning conditions. □ Additionally, we can show the following lemma, which states that provided that FRu (Γ, txu, 𝑍 ) holds, it is ensured that the variables from 𝑍 written by txu in Γ can never overlap with variables that would be written by attacker transactions tx𝐴 when executed in Γ. Lemma D.33 (Disjointness of write sets). Let Γ be a configuration and txu be a transaction such that sender(txu ) = u for u ∈ Hon, and 𝑍 ⊆ GC be a set of variables. Assume that FRu (Γ, txu, 𝑍 ) holds. Then it holds for all transactions tx𝐴 with sender(tx𝐴 ) ≠ u that Writes (Γ, txu, 𝑍 ) ⊆ 𝑍 \ Writes (Γ, tx𝐴 , 𝑍 )

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

Additionally, we can provide semantic versions of the notions of invariants and round invariants, which hold for the frontrunning and backrunning conditions. We first can show that if FRu𝜌 (·, ·, ·) holds at the beginning of the round, then FRu (·, ·, ·) holds throughout the round as long as only 𝜏 or attacker transactions get executed. Lemma D.34 (Frontrunning Conditions throughout rounds). Let txu be a transaction with sender(txu ) = u for some u ∈ Hon and 𝑍 ⊆ GC . Let Γ1 , Γ2 , . . . , Γ𝑛 be configurations such that 𝜌 (Γ𝑗 ) = tx1

𝜌 (Γ𝑙 ) for 𝑗, 𝑙 ∈ {1, . . . , 𝑛} and 𝛿 (Γ1 ) mod 𝑘 = 0. Further, let Γ1 −−→ tx2

tx𝑛−1

sent along with the transaction). Those variables, however, should not be considered in the set 𝑋 ∗ , which ranges over the global variables GC (since it will denote the set of variables, which will stay uninfluenced by reordering of transactions). Lemma D.37 (Commutativity (Between user and attacker transactions)). Let Γ1 , Γ1 , Γ2 , Γ2 , Γ3 and Γ3 be configurations and txu be a transaction such that sender(txu ) = u for u ∈ Hon. Let 𝑋 ∗ ⊆ GC be a set of variables such that 𝑋 Ev ⊆ 𝑋 ∗ and closeddeps (𝑋 ∗ ). Further, let tx𝐴 be a transaction such that sender(tx𝐴 ) ≠ u. Assume that Γ1 ≈𝑋 ∗ Γ1 and FRu (Γ1, txu, 𝑋 ∗ ), BRu (Γ1, txu, 𝑋 ∗ ), FRu (Γ1, txu, 𝑋 ∗ ), and BRu (Γ1, txu, 𝑋 ∗ ), hold. Then

Γ2 −−→ . . . −−−−→ Γ𝑛 for transaction tx1, . . . tx𝑛−1 such that for all −𝑣 ) for 𝑗 ∈ {1, . . . 𝑛 − 1}, it holds that either tx 𝑗 = 𝜏 or tx 𝑗 = C.g(→ u some g ∈ FC and sender(tx 𝑗 ) ≠ u. Then if FR𝜌 (Γ1, txu, 𝑍 ) then also FRu (Γ𝑛 , txu, 𝑍 ). Proof. Follows immediately from Lemma D.13 and Lemma D.24. □ We can establish a similar lemma for backrunning conditions. Note that backrunning conditions are also invariant w.r.t. the honest user transaction, resulting in a slightly stronger lemma: Lemma D.35 (Backrunning Conditions throughout rounds). Let txu be a transaction with sender(txu ) = u for some u ∈ Hon and 𝑍 ⊆ GC . Let Γ1 , Γ2 , . . . , Γ𝑛 be configurations such that 𝜌 (Γ𝑗 ) = tx1

𝜌 (Γ𝑙 ) for 𝑗, 𝑙 ∈ {1, . . . , 𝑛} and 𝛿 (Γ1 ) mod 𝑘 = 0. Further, let Γ1 −−→ tx2

tx𝑛−1

Γ2 −−→ . . . −−−−→ Γ𝑛 for transaction tx1, . . . tx𝑛−1 such that for all 𝑗 ∈ −𝑣 ) {1, . . . 𝑛 − 1}, it holds that either tx 𝑗 = 𝜏 or tx 𝑗 = txu or tx 𝑗 = C.g(→ u for some g ∈ FC and sender(tx 𝑗 ) ≠ u. Then if BR𝜌 (Γ1, txu, 𝑍 ) then also BRu (Γ𝑛 , txu, 𝑍 ). Proof. Follows immediately from Lemma D.13 and Lemma D.25. □ Remark. Throughout this paper, we assume that the attacker also only schedules transactions of contract C. This assumption could easily be lifted since transactions of other contracts C ′ ≠ C let the contract variables of C unchanged.

txu

tx𝐴

tx𝐴

txu

𝑥𝑠 m

𝑥𝑠𝐴

𝑥𝑠𝐴

𝑥𝑠 m

Γ1 −−−→ Γ2 −−−→ Γ3 ∧ Γ1 −−−→ Γ2 −−−→ Γ3 ⇒ 𝑥𝑠𝐴 = 𝑥𝑠𝐴 ∧ 𝑥𝑠 m = 𝑥𝑠 m ∧ Γ3 ≈𝑋 ∗ Γ3 for observables 𝑥𝑠 m , 𝑥𝑠 m , 𝑥𝑠𝐴 , 𝑥𝑠𝐴 . Proof. In the following, we will use the shorthands 𝑊u := Writes (Γ1, txu, 𝑋 ∗ ) and 𝑊𝐴 := Writes (Γ1, tx𝐴 , 𝑋 ∗ ). Note that this tx𝐴

gives us immediately (using Lemma D.27) for Γ2′ with Γ1 −−→ Γ2′ that Γ1 ≈𝑋 ∗ \𝑊𝐴 Γ2′ . Consequently, using Lemma D.5, from Γ1 ≈𝑋 ∗ Γ1 and closeddeps (𝑋 ∗ ), we can conclude that Γ2′ ≈𝑋 ∗ \𝑊𝐴 Γ2 , and so also Γ1 ≈𝑋 ∗ \𝑊𝐴 Γ2 and since Γ1 ≈𝑋 ∗ Γ1 also Γ1 ≈𝑋 ∗ \𝑊𝐴 Γ2 (NWu1). ′

txu

′

Similarly, we know by Lemma D.27 that for Γ2 with Γ1 −−→ Γ2 ′ we get Γ1 ≈𝑋 ∗ \𝑊u Γ2 . So, using Lemma D.5, from Γ1 ≈𝑋 ∗ Γ1 and closeddeps (𝑋 ∗ ), we can conclude that Γ2′ ≈𝑋 ∗ \𝑊u Γ2 , and so also Γ1 ≈𝑋 ∗ \𝑊u Γ2 and since Γ1 ≈𝑋 ∗ Γ1 also Γ1 ≈𝑋 ∗ \𝑊u Γ2 (NWa1). Further, by Lemma D.29, we know that Γ2 ≈𝑋 ∗ \𝑊u Γ3 (NWa2) and ′

txu

′

′

that for Γ2 and 𝑥𝑠 m ′ with Γ1 −−−→ Γ2 it holds that Γ2 ≈𝑊u Γ3 and ′ 𝑥𝑠 m

𝑥𝑠 m = 𝑥𝑠 m ′ . Using Lemma D.5, from Γ1 ≈𝑋 ∗ Γ1 and closeddeps (𝑋 ∗ ) ′ we can also conclude that Γ2 ≈𝑊u Γ2 and 𝑥𝑠 m ′ = 𝑥𝑠 m and consequently 𝑥𝑠 m = 𝑥𝑠 m and Γ3 ≈𝑊u Γ2 (Wa). Similarly, from Lemma D.31, we know that Γ2 ≈𝑋 ∗ \𝑊𝐴 Γ3 (NWu2) and that for Γ2′ and 𝑥𝑠𝐴′ with tx𝐴

Γ1 −−−→ Γ2′ it holds that Γ2′ ≈𝑊𝐴 Γ3 and 𝑥𝑠𝐴 = 𝑥𝑠𝐴′ . Using Lemma D.5, ′ 𝑥𝑠𝐴

D.2.4 Commutativity. Using the semantic correctness conditions, we can next establish a commutativity lemma, which shows that front- and backrunning conditions together ensure that honest user transactions and attacker transactions commute. We will consider commutativity with respect to a set 𝑋 ∗ ⊆ GC of variables, which contains the event variables 𝑋 Ev and which is closed under data and control dependencies of the contract C. Formally, we define closedness as follows: Definition D.36 (Closedness under dependencies). Let 𝑋 ∗ ⊆ GC be a set of variables and 𝑖 be some index. We say that 𝑋 ∗ is closed under dependencies (written closeddeps (𝑋 ∗ )) if it holds that Ø GC ∩ DDeps𝑖g (𝑦) ∪ CDeps𝑖g (𝑦) ⊆ 𝑋 ∗ ∗ 𝑦 ∈𝑋 ,g ∈ FC Note that the data or control dependencies of the different contract functions may contain local variables (e.g., referring to the transaction parameters, such as the transaction sender or the value

from Γ1 ≈𝑋 ∗ Γ1 and closeddeps (𝑋 ∗ ), we can also conclude that Γ2′ ≈𝑊𝐴 Γ2 and 𝑥𝑠𝐴′ = 𝑥𝑠𝐴 and consequently 𝑥𝑠𝐴 = 𝑥𝑠𝐴 and Γ3 ≈𝑊𝐴 Γ2 (Wu). Further, from Lemma D.33 (combined with Lemma D.28), we also know that 𝑊𝐴 ⊆ 𝑋 ∗ \ 𝑊u (I1) and consequently also 𝑊u ⊆ 𝑋 ∗ \ 𝑊𝐴 (I2). We now show Γ3 ≈𝑋 ∗ Γ3 by showing Γ3 ≈𝑊𝐴 Γ3 , Γ3 ≈𝑊u Γ3 , and Γ3 ≈ (𝑋 ∗ \𝑊𝐴 )∩(𝑋 ∗ \𝑊u ) Γ3 separately. • By (NWa2), we have Γ2 ≈𝑋 ∗ \𝑊u Γ3 and consequently by (I1) also Γ2 ≈𝑊𝐴 Γ3 . Together with (Wu) (Γ3 ≈𝑊𝐴 Γ2 ), this gives us Γ3 ≈𝑊𝐴 Γ3 . • By (NWu2), we have Γ2 ≈𝑋 ∗ \𝑊𝐴 Γ3 and consequently, by (I2) also Γ2 ≈𝑊u Γ3 . Together with (Wa) (Γ3 ≈𝑊u Γ2 ), this gives us Γ3 ≈𝑊u Γ3 . • Let in the following be NW := (𝑋 ∗ \𝑊𝐴 )∩(𝑋 ∗ \𝑊u ). We have that Γ2 ≈NW Γ3 (by (NWu2) and NW ⊆ 𝑋 ∗ \𝑊𝐴 ), Γ2 ≈NW Γ1 (by (NWa2) and NW ⊆ 𝑋 ∗ \𝑊u ), Γ1 ≈NW Γ1 (by assumption and NW ⊆ 𝑋 ∗ ), Γ1 ≈NW Γ2 (by (NWu1) and NW ⊆ 𝑋 ∗ \𝑊𝐴 ),

On Identifying Sound Conditions for Frontrunning Resistance

and Γ2 ≈NW Γ3 (by (NWa2) and NW ⊆ 𝑋 ∗ \ 𝑊u ). Together, this gives us Γ3 ≈NW Γ3 (by transitivity of ≈). Note that Γ3 ≈𝑊𝐴 Γ3 , Γ3 ≈𝑊u Γ3 , and Γ3 ≈ (𝑋 ∗ \𝑊𝐴 )∩(𝑋 ∗ \𝑊u ) Γ3 give us Γ3 ≈𝑋 ∗ Γ3 because 𝑊u ∪ 𝑊𝐴 ∪ ((𝑋 ∗ \ 𝑊𝐴 ) ∩ (𝑋 ∗ \ 𝑊u )) = (𝑊u ∪ 𝑊𝐴 ) ∪ (𝑋 ∗ \ (𝑊u ∪ 𝑊𝐴 )) = 𝑋 ∗ □ In addition to the commutativity between the user and the attacker transaction, we also need to establish that also (i) user transactions commute with 𝜏 within one round and (ii) attacker transactions commute with 𝜏 within one round. This is crucial since the attacker may freely move transactions between blocks. We state the corresponding lemmas analogously to the previous commutativity lemma. For the commutativity between user transactions and 𝜏 transactions, it is sufficient of the initial configuration satisfies the frontrunning condition, since this condition already ensures that the behavior of the transaction txu (i) does not depend directly on the block number and that (ii) indirect dependencies to the block number cannot impact the behavior of txu within one round (due to the round invariant property of the frontrunning condition). Lemma D.38 (Commutativity (Between user and 𝜏 transactions)). Let Γ1 , Γ1 , Γ2 , Γ2 , Γ3 and Γ3 be configurations and txu be a transaction such that sender(txu ) = u for u ∈ Hon. Let 𝑋 ∗ ⊆ GC be a set of variables such that 𝑋 Ev ⊆ 𝑋 ∗ and closeddeps (𝑋 ∗ ). Assume that Γ1 ≈𝑋 ∗ Γ1 and FRu (Γ1, txu, 𝑋 ∗ ), 𝜌 (Γ1 ) = 𝜌 (Γ3 ) and 𝜌 (Γ1 ) = 𝜌 (Γ3 ) and FRu (Γ1, txu, 𝑋 ∗ ), hold. Then txu

𝜏

𝜏

txu

− Γ2 −−−→ Γ3 Γ1 −−−→ Γ2 → − Γ3 ∧ Γ1 → 𝑥𝑠 m

𝑥𝑠 m

⇒ 𝑥𝑠 m = 𝑥𝑠 m ∧ Γ3 ≈𝑋 ∗ Γ3

Based on the commutativity lemmas, we can now establish results for permutations between transaction sequences where (i) a (single) user transaction may be arbitrarily placed and (ii) where an attacker may shift the block boundaries. In the following, we will consider permutations 𝜋 on lists to be functions that apply finite sequences of pairwise swap operations among neighboring elements to a list. ® =\{𝑥 1 ,...,𝑥𝑛 } tx ® ′ to denote that two We will use the notation tx ′ ® tx ® are equal up to the set 𝑆 = {𝑥 1, . . . , 𝑥𝑛 }, meaning that lists tx, ® ↓𝜆𝑥 . 𝑥∉𝑆 = tx ® ′ ↓𝜆𝑥 . 𝑥∉𝑆 where tx ® ↓𝑃 denotes the list tx ® with all tx elements not satisfying a predicate 𝑃 removed. Note that we generally assume that all (faithfully signed) transactions can execute, but may indicate a potential failure with a dedicated observable. So, in particular, the prior execution of another transaction may not impact the executability of a transaction but may only alter its effect. This implies in particular that if a ® is executable, then also every permutation transaction sequence tx ® of the same transaction sequence is executable. 𝜋 ( tx) The following lemma states that permuting a transaction se® of at most 𝑘 blocks and containing a single transaction quence tx txu of the honest user, in a way such that the order of attacker ® stays unaffected, will not change the effects transactions in 𝜋 ( tx) of executing this sequence in configurations that satisfy the frontrunning and backrunning conditions (provided that they agree on a set 𝑋 ∗ of variables that contain the event variables and that is closed under dependencies). Lemma D.40 (Permutation within rounds (with attacker transactions)). Let C be a contract with variables XC and u ∈ Hon be a user. Let 𝑋 ∗ ⊆ GC be a set of variables such that 𝑋 Ev ⊆ 𝑋 ∗ and closeddeps (𝑋 ∗ ). Let Γ, Γ be configurations with Γ ≈𝑋 ∗ Γ and 𝛿 (Γ) = 𝛿 (Γ) = 𝑟 ∗ 𝜌 (Γ) for some 𝑟 ∈ N. Let txu be a transaction such that sender(txu ) = u and FRu𝜌 (Γ, txu, 𝑋 ∗ ), FRu𝜌 (Γ, txu, 𝑋 ∗ ), BRu𝜌 (Γ, txu, 𝑋 ∗ ), BRu𝜌 (Γ, txu, 𝑋 ∗ ), ® tx

∗

BRu𝜌 (Γ, 𝜏 , 𝑋 ∗ ), and BRu𝜌 (Γ, 𝜏 , 𝑋 ∗ ). Then it holds that if Γ −−→ Γ ′ 𝑥𝑠 ®

for observables 𝑥𝑠 m , 𝑥𝑠 m . Proof. Proof is analogous to that of Lemma D.37, using Lemma D.30. □ Lemma D.39 (Commutativity (Between 𝜏 and attacker transactions)). Let Γ1 , Γ1 , Γ2 , Γ2 , Γ3 and Γ3 be configurations and u ∈ Hon a user. Let 𝑋 ∗ ⊆ GC be a set of variables such that 𝑋 Ev ⊆ 𝑋 ∗ and closeddeps (𝑋 ∗ ). Further, let tx𝐴 be a transaction such that sender(tx𝐴 ) ≠ u. Assume that Γ1 ≈𝑋 ∗ Γ1 and 𝜌 (Γ1 ) = 𝜌 (Γ3 ) and 𝜌 (Γ1 ) = 𝜌 (Γ3 ) and BRu (Γ1, 𝜏 , 𝑋 ∗ ), BRu (Γ1, 𝜏 , 𝑋 ∗ ) hold. Then 𝜏

tx𝐴

tx𝐴

𝑥𝑠𝐴

𝑥𝑠𝐴

𝜏

Γ1 → − Γ2 −−−→ Γ3 ∧ Γ1 −−−→ Γ2 → − Γ3 ⇒ 𝑥𝑠𝐴 = 𝑥𝑠𝐴 ∧ Γ3 ≈𝑋 ∗ Γ3 for observables 𝑥𝑠𝐴 , 𝑥𝑠𝐴 . Proof. Proof is analogous to that of Lemma D.37, using Lemma D.32. □

for some lists of observables 𝑥𝑠, ® configurations Γ ′ and transaction list ® ® ® ↓𝜆𝑥 . sender(𝑥 )=u = [txu ], then also for tx with | tx ↓𝜆𝑥 . 𝑥=𝜏 | < 𝑘 and tx ′ ® =\{txu ,𝜏 } tx ® there exist 𝑥𝑠 all permutations 𝜋 such that 𝜋 ( tx) ® ′ , Γ such ® 𝜋 ( tx)

∗

′

′

that Γ −−−−→ Γ and Γ ′ ≈𝑋 ∗ Γ and 𝑥𝑠 ® ′ = 𝜋 (𝑥𝑠). ® ′ 𝑥𝑠 ®

® =\{txu ,𝜏 } tx ® ensures that Proof. We note that requiring 𝜋 ( tx) such permutation 𝜋 only needs to perform pairwise swaps involving txu or 𝜏 . Consequently, we prove the lemma by induction on the list of such swap operations performed by 𝜋. For each of the pairwise swaps involving txC or 𝜏 , we can easily conclude the existence of the permuted transaction sequence with the desired properties from Lemmas D.37, D.38, D.39, and relying on the fact that backrunning and frontrunning conditions persist through rounds as given by Lemmas D.34 and D.35. □ Lemma D.41 (Permutation within rounds (with 𝜏 )). Let C be a contract with variables XC and u ∈ Hon be a user. Let 𝑋 ∗ ⊆ GC be a set of variables such that 𝑋 Ev ⊆ 𝑋 ∗ and closeddeps (𝑋 ∗ ). Let Γ, Γ be configurations with Γ ≈𝑋 ∗ Γ and 𝛿 (Γ) = 𝛿 (Γ) = 𝑟 ∗ 𝜌 (Γ) for some 𝑟 ∈ N. Assume that BRu𝜌 (Γ, 𝜏 , 𝑋 ∗ ), and BRu𝜌 (Γ, 𝜏 , 𝑋 ∗ ) hold. Then it

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

∗

holds that if Γ −−→ Γ ′ for some lists of observables 𝑥𝑠, ® configurations

simulator published the mempool as the first block in each round.

𝑥𝑠 ®

® with | tx| ® = 𝑘, then also for all permutations Γ ′ and transaction list tx ® 𝜋 ( tx)

′

∗

® =\{𝜏 } tx ® there exist 𝑥𝑠 𝜋 such that 𝜋 ( tx) ® ′ , Γ such that Γ −−−−→ Γ ′

′

𝑥𝑠 ®

′

and Γ ′ ≈𝑋 ∗ Γ and 𝑥𝑠 ® ′ = 𝜋 (𝑥𝑠). ®

aRun𝜙 (𝐴, 𝑅𝐴 , 𝑅𝑆 , 𝑖) :=

® =\{𝜏 } tx ® ensures that such Proof. We note that requiring 𝜋 ( tx) permutation 𝜋 only needs to perform pairwise swaps involving 𝜏 . Consequently, we prove the lemma by induction on the list of such swap operations performed by 𝜋. For each of the pairwise swaps involving 𝜏 , we can easily conclude the existence of the permuted transaction sequence with the desired properties from Lemma D.39, and relying on the fact that backrunning aconditions persist through rounds as given by Lemma D.35. □

D.2.5 Simulator. We formally define a generic simulator used for our soundness proof. The general idea behind the simulator is that at the beginning of every round, it publishes the mempool as the first block and then uses this knowledge to reconstruct the attacker’s behavior for the respective round. To define our simulator, we first define the following function: step(𝐴, 𝑅, P, 𝑛) :=

  𝑅    B ∗    step(𝐴, 𝑅 −→ Γ, P ′, 𝑛 − 1)             

,𝑛 = 0 ,𝑛 > 0 ∧ B = 𝐴(𝑅, P)

 𝑅𝐴      step(𝐴, 𝑅𝐴 , B® [0], 𝑖)           aRun𝜙 (𝐴, step(𝐴, 𝑅𝐴 , B®1 [0], 𝑘), 𝑅2, 𝑖)                      aRun𝜙 (𝐴, step(𝐴, 𝑅𝐴 , 𝜖, 𝑘), 𝑅2, 𝑖)                    

, |blocks(𝑅𝑆 )| = 0 , B® = blocks(𝑅𝑆 ) ® > 0 ∧ | B| ® <𝑘 ∧| B| 𝑆 , 𝑅 = 𝑅1 · 𝑅2 ∧B®1 = blocks(𝑅1 ) ∧B®2 = blocks(𝑅2 ) ∧| B®1 | = 𝑘 𝜙 (Γ𝑅1 ) , 𝑅𝑆 = 𝑅1 · 𝑅2 ∧B®1 = blocks(𝑅1 ) ∧B®2 = blocks(𝑅2 ) ∧| B®1 | = 𝑘 ¬𝜙 (Γ𝑅1 )

Intuitively, this function processes the simulator run 𝑅𝑆 from the left, taking chunks of blocks of size 𝑘 and produces the corresponding attacker run by using step(·, ·, ·, 𝑘) to invoke the attacker 𝑘-times on the mempool extracted from the first block of the simulator run (if the condition 𝜙 holds) or the empty mempool (if 𝜙 does not hold) in each chunk.

B ∗

∧ Γ𝑅 −→ Γ ∧ P ′ = P\B®

Intuitively, step(𝐴, 𝑅, P, 𝑛) invokes the attacker strategy 𝐴 𝑛times with mempool P on run 𝑅.

Lemma D.43 (aRun Correctness). Let 𝐴, 𝑆 be attacker strategies and Σ = Σ𝑟→ be the user strategy for a round strategy Σ𝑟 and 𝑅𝑆 be a run such that (𝑆, Σ) ⊢ 𝑅𝑆 and 𝑛 ∈ N such that 𝑛 ≤ 𝑘. Let 𝜙 be a condition on configurations. Further, let |blocks(𝑅𝑆 )| = 𝑟 ∗ 𝑘 + 𝑖 for some 𝑟, 𝑖 ∈ N and 𝑖 < 𝑘. Then there exists 𝑅𝐴 = aRun𝜙 (𝐴, 𝑅𝐴 , 𝑅𝑆 , 𝑛) such that (𝐴, Σ) ⊢ 𝑅𝐴 and |blocks(𝑅𝑆 )| = 𝑟 ∗ 𝑘 + 𝑛.

Lemma D.42 (step Correctness). Let 𝐴 be an attacker strategy, Σ = Σ𝑟→ the user strategy for a round strategy Σ𝑟 and 𝑅𝐴 a run such that |blocks(𝑅𝐴 )| = 𝑟 ∗ 𝑘 for some 𝑟 ∈ N and (𝐴, Σ) ⊢ 𝑅𝐴 and 𝑛 ∈ N such that 𝑛 ≤ 𝑘. Then there exists a run 𝑅𝐴 = step(𝐴, 𝑅, Σ(𝑅𝐴 ), 𝑛) such that |blocks(𝑅𝐴 )| = 𝑛 and (𝐴, Σ) ⊢ 𝑅𝐴 · 𝑅𝐴 .

Proof. Follows by induction on 𝑛, exploiting the property of round-based user strategy Σ to keep on scheduling the same transactions within the same round. □

Next, we define a function that will allow us to reconstruct an attacker run, from a simulator run, when assuming that the

Proof. Follows by size induction on the length of |blocks(𝑅𝑆 )|, distinguishing the cases |blocks(𝑅𝑆 )| < 𝑘 and |blocks(𝑅𝑆 )| = 𝑘∗𝑟 +𝑗 for 𝑟, 𝑗 ∈ N for 𝑗 < 𝑘. For the individual cases, we use Lemma D.42 in addition to the inductive hypothesis to conclude the proof. □

With these functions in place, we can now define the simulator:

On Identifying Sound Conditions for Frontrunning Resistance ′

 P      B                               B         𝜙 𝑆 𝐴 (𝑅𝑆 , P) :=                        B                    

, |blocks(𝑅𝑆 )| mod 𝑘 = 0 ∧ 𝜙 (𝑅𝑆 ) 𝑆 · 𝑅 𝑆 ∧ 𝜙 (𝑅 𝑆 ) , 𝑅𝑆 = 𝑅pre pre post 𝑆 )| = 𝑘 ∗ 𝑟 ∧∃𝑟 ∈ N.|blocks(𝑅pre 𝑆 ) = [P 𝐴 ] ∧blocks(𝑅post 0 𝐴 ∧𝑅 = aRun𝜙 (𝐴, Γinit, 𝑅𝑆 , 2) 𝐴 ] · [B 𝐴 ] = blocks(𝑅 𝐴 ) ∧L0𝐴 · [B0,0 0,1 𝐴 𝐴 \P 𝐴 ∧B = B0,0 \P0𝐴 · B0,1 0 𝑆 𝑆 𝑆 𝑆 ) , 𝑅 = 𝑅pre · 𝑅post ∧ ∧ 𝜙 (𝑅pre 𝑆 )| = 𝑘 ∗ 𝑟 ∧∃𝑟 ∈ N.|blocks(𝑅pre 𝑆 ∧|blocks(𝑅post )| = 𝑖 ∧ 𝑖 < 𝑘 ∧ 𝑖 > 1 𝑆 ) ∧[P0𝐴 ] · L = blocks(𝑅post ∧𝑅𝐴 = aRun𝜙 (𝐴, Γinit, 𝑅𝑆 , 𝑖 + 1) 𝐴 ] = blocks(𝑅 𝐴 ) ∧L0𝐴 · [B0,0 𝐴 ∧B = B0,0 \P0𝐴 𝑆 · 𝑅 𝑆 ∧ ∧ ¬𝜙 (𝑅 𝑆 ) , 𝑅𝑆 = 𝑅pre pre post 𝑆 )| = 𝑘 ∗ 𝑟 ∧∃𝑟 ∈ N.|blocks(𝑅pre 𝑆 )| = 𝑖 ∧ 𝑖 < 𝑘 ∧|blocks(𝑅post 𝐴 ∧𝑅 = aRun𝜙 (𝐴, Γinit, 𝑅𝑆 , 𝑖 + 1) ∧L0𝐴 · [B] = blocks(𝑅𝐴 )

Here Γinit denotes the initial configuration of all runs (representing a fresh state). Note that aRun𝜙 (𝐴, Γinit, 𝑅𝑆 , 𝑗) simulates the attacker behavior for all complete rounds and additional 𝑗 steps. For this reason, the function is invoked with 𝑗 = 2 in the second case (to produce two attacker blocks for the newly started round) and 𝑗 = 𝑖 + 1 in the third case (to simulate the attacker block once ahead of the current simulated run 𝑅𝑆 ). Also, note that it is evident that the simulator satisfies the substitution criterion, since its definition does not make any adaptive use of the mempool. The simulator satisfies the key property that for a round-based user strategy Σ, within one round, it executes the same transactions as the attacker, with the only difference that the (single) user transaction scheduled by Σ may occur in a different position. All other transactions are executed in the same order. We capture this behavior with the following core property: 𝜙

Lemma D.44 (Correctness of 𝑆 𝐴 (in 𝜙 rounds)). Let u be an honest user and Σ = Σ𝑟→ be the user strategy for a round strategy Σ𝑟 (for u) and let 𝐴 be an attacker strategy. Let 𝜙 be a condition on 𝐴 and 𝑅 𝐴 be an configurations. Let 𝑘 > 1, tx be a transaction and 𝑅pre 𝐴 𝐴 𝐴 )| = 𝑟 ∗ 𝑘 attacker run such that (𝐴, Σ) ⊢ 𝑅pre · 𝑅 and |blocks(𝑅pre 𝐴 for some 𝑟 ∈ N and |blocks(𝑅 )| = 𝑖 for 𝑖 ∈ N with 𝑖 ≤ 𝑘. Let 𝑅𝐴 = ® tx

∗

® Further, Γ𝑅𝐴 − → Γ𝐴 for some configuration Γ𝐴 and transaction list tx. pre

𝑆 be a run such that (𝑆 , Σ) ⊢ 𝑅 𝑆 , and |blocks(𝑅 𝑆 )| = 𝑟 ∗ 𝑘 let 𝑅pre pre pre 𝐴 𝐴 = aRun𝜙 (𝐴, Γ , 𝑅 𝑆 , 0) and Σ (Γ and 𝑅pre init pre 𝑟 𝑅𝐴 ) = Σ𝑟 (Γ𝑅𝑆 ) = {tx}

𝑆 · 𝑅𝑆 , ® such that (𝑆 𝐴 , Σ) ⊢ 𝑅pre for some Γ𝑆 and transaction list tx ′ 𝜙 𝑆 𝐴 𝑆 ® =\{tx,𝜏 } tx ® and 𝑅 = aRun (𝐴, Γinit, 𝑅 , 𝑖 mod |blocks(𝑅 )| = 𝑖, tx 𝑘) and if 𝑖 > 0 then blocks(𝑅𝑆 ) [0] = [tx]. 𝜙

Proof. This proof is carried out by induction on 𝑖 ∈ N. The case 𝑖 = 0 follows trivially from the assumption by choosing 𝑅𝑆 = [tx] ∗

Γ𝑅𝑆 . In the case 𝑖 = 1, we can choose 𝑅𝑆 = Γ𝑅𝑆 −−−→ Γ𝑆 for a pre pre corresponding Γ𝑆 (which is guaranteed to exist since tx is the output of Σ) to derive the desired properties immediately. In the case 𝑖 = 2, [tx] ∗

B ∗

we can choose 𝑅𝑆 = Γ𝑅𝑆 −−−→ Γ𝑆 −→ Γ𝑆′ for B as defined in the pre simulator definition. The claim follows then immediately from the definition of the simulator. In the case 𝑖 > 2 the reasoning follows immediately from the inductive hypothesis, and the definitions of 𝜙 𝑆 𝐴 and aRun. □ 𝜙

Lemma D.45 (Correctness of 𝑆 𝐴 (in ¬𝜙 rounds)). Let u be an honest user and Σ = Σ𝑟→ be the user strategy for a round strategy Σ𝑟 (for u) and let 𝐴 be an attacker strategy. Let 𝜙 be a condition on 𝐴 and 𝑅 𝐴 be an configurations. Let 𝑘 > 1, tx be a transaction and 𝑅pre 𝐴 · 𝑅 𝐴 and |blocks(𝑅 𝐴 )| = 𝑟 ∗ 𝑘 attacker run such that (𝐴, Σ) ⊢ 𝑅pre pre for some 𝑟 ∈ N and |blocks(𝑅𝐴 )| = 𝑖 for 𝑖 ∈ N with 𝑖 ≤ 𝑘. Let 𝑅𝐴 = ® tx

∗

® Further, Γ𝑅𝐴 − → Γ𝐴 for some configuration Γ𝐴 and transaction list tx. pre

𝑆 be a run such that (𝑆 , Σ) ⊢ 𝑅 𝑆 , and |blocks(𝑅 𝑆 )| = 𝑟 ∗ 𝑘 let 𝑅pre pre pre 𝐴 𝐴 = aRun𝜙 (𝐴, Γ , 𝑅 𝑆 , 0) and Σ (Γ and 𝑅pre init pre 𝑟 𝑅𝐴 ) = Σ𝑟 (Γ𝑅𝑆 ) = ∅ and 𝜙

pre

pre

𝑆 ). Then there exists a run ¬𝜙 (𝑅pre ® tx

∗

𝑅𝑆 = Γ𝑅𝑆 − → Γ𝑆 pre

𝑆 · 𝑅 𝑆 , |blocks(𝑅 𝑆 )| = 𝑖, and for some Γ𝑆 such that (𝑆 𝐴 , Σ) ⊢ 𝑅pre 𝑅𝐴 = aRun𝜙 (𝐴, Γinit, 𝑅𝑆 , 𝑖 mod 𝑘). 𝜙

Proof. This proof is carried out by induction on 𝑖 ∈ N. The case 𝑖 = 0 follows trivially from the assumption by choosing 𝑅𝑆 = Γ𝑅𝑆 . For 𝑖 > 0, the claim follows immediately from the inductive pre

𝜙

hypothesis, and the definitions of 𝑆 𝐴 and aRun.

□

𝜙

Lemma D.46 (Correctness of 𝑆 𝐴 (in 𝜙 rounds, no transaction)). Let u be an honest user and Σ = Σ𝑟→ be the user strategy for a round strategy Σ𝑟 (for u) and let 𝐴 be an attacker strategy. Let 𝜙 be a condition on configurations. Let 𝑘 > 1, tx be a transaction 𝐴 and 𝑅 𝐴 be an attacker run such that (𝐴, Σ) ⊢ 𝑅 𝐴 · 𝑅 𝐴 and and 𝑅pre pre 𝐴 )| = 𝑟 ∗ 𝑘 for some 𝑟 ∈ N and |blocks(𝑅 𝐴 )| = 𝑖 for 𝑖 ∈ N |blocks(𝑅pre ® tx

∗

with 𝑖 ≤ 𝑘. Let 𝑅𝐴 = Γ𝑅𝐴 − → Γ𝐴 for some configuration Γ𝐴 and pre

𝑆 be a run such that (𝑆 , Σ) ⊢ 𝑅 𝑆 , ® Further, let 𝑅pre transaction list tx. pre 𝐴 𝑆 𝐴 = aRun𝜙 (𝐴, Γ , 𝑅 𝑆 , 0) and and |blocks(𝑅pre )| = 𝑟 ∗ 𝑘 and 𝑅pre init pre 𝑆 ). Then there exists a run Σ𝑟 (Γ𝑅𝐴 ) = Σ𝑟 (Γ𝑅𝑆 ) = ∅ and 𝜙 (𝑅pre 𝜙

pre

pre

𝜙

pre

𝑆 ). Then there exists a run and 𝜙 (𝑅pre ®′ tx

∗

∗

pre

′

𝑅𝑆 = Γ𝑅𝑆 −−→ Γ𝑆 pre

pre

®′ tx

𝑅𝑆 = Γ𝑅𝑆 −−→ Γ𝑆 𝑆 · 𝑅𝑆 , ® such that (𝑆 𝐴 , Σ) ⊢ 𝑅pre for some Γ𝑆 and transaction list tx ′ ® ® |blocks(𝑅𝑆 )| = 𝑖, tx and =\{𝜏 } tx 𝑅𝐴 = aRun𝜙 (𝐴, Γinit, 𝑅𝑆 , 𝑖 mod 𝑘). 𝜙

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

Proof. This proof is carried out by induction on 𝑖 ∈ N. The case 𝑖 = 0 follows trivially from the assumption by choosing 𝑅𝑆 = Γ𝑅𝑆 . For 𝑖 > 0 the claim follows immediately from the inductive pre

𝜙

hypothesis, and the definitions of 𝑆 𝐴 and aRun.

□

D.2.6 Similarity Relation. We define the similarity relation that our simulator 𝑆 𝐴 can uphold. Intuitively, the simulator can be guaranteed to perform all events in the same order, with the only exception of user-triggered events whose position could be shifted within one round. Note that this similarity is very strong in the sense that for the case where relevant events can only be triggered by user transactions (which is a very common case to be considered), the observables of the traces are fully identical. Even when considering attacker transactions to trigger observables, the provided property still yields useful notions when considering observations, whose concrete ordering within one round is irrelevant (e.g., when tracking money transfers). Since we do not distinguish on the observation level how an observation was created, we will show our result for the general simulation relation, which does not fix the order of observables within a round:

Let 𝜙 be defined as follows: 𝜙 (Γ) :⇔ BRu𝜌 (Γ, 𝜏 , 𝑋 ∗ ) ∧ ∃tx. FRu𝜌 (Γ, tx, 𝑋 ∗ ) ∧ BRu𝜌 (Γ, tx, 𝑋 ∗ ) Let 𝑅𝐴 be an attacker run such that (𝐴, Σ) ⊢ 𝑅𝐴 and |blocks(𝑅𝐴 )| = 𝜙 𝑘 ∗ 𝑟 for 𝑟 ∈ N. Then there exists a run 𝑅𝑆 such that (𝑆 𝐴 , Σ) ⊢ 𝑅𝑆 𝑆 𝐴 and |blocks(𝑅 )| = 𝑘 ∗ 𝑟 and Γ𝑅𝐴 ≈𝑋 ∗ Γ𝑅𝑆 and 𝑅 ∼𝑆 𝑅𝑆 and 𝑅𝐴 = aRun𝜙 (𝐴, Γinit, 𝑅𝑆 , 0). Proof. The proof proceeds by induction on 𝑟 ∈ N. For 𝑟 = 0, we know that 𝑅𝐴 = Γinit . By choosing 𝑅𝑆 = Γinit the claims trivially 𝐴 · 𝑅 𝐴 such hold since 𝑅𝐴 = 𝑅𝑆 . For 𝑟 > 0, we know that 𝑅𝐴 = 𝑅pre post 𝐴 𝐴 that |blocks(𝑅pre )| = (𝑟 − 1) ∗ 𝑘 and |blocks(𝑅post )| = 𝑘. From the 𝑆 such inductive hypothesis, we hence get a valid simulator run 𝑅pre 𝑆 𝐴 𝑆 . We ∗ that |blocks(𝑅pre )| = (𝑟 − 1) ∗ 𝑘, Γ𝑅𝐴 ≈𝑋 Γ𝑅𝑆 and 𝑅pre ∼𝑆 𝑅pre pre pre distinguish the cases of whether 𝜙 (Γ𝑅𝑆 ) holds. pre

• If 𝜙 (Γ𝑅𝑆 ) does not hold, we know by assumption that pre Σ(Γ𝑅𝑆 ) = ∅. Since Σ𝑟 agrees on all configurations with the pre same values for variables in 𝑋 ∗ , we have that also Σ(Γ𝑅𝐴 ) = pre ∅. We can now use Lemma D.45 to deduce the existence of a 𝑆 𝑆 )| = 𝑘. Furvalid simulator run 𝑅post such that |blocks(𝑅post ® tx

𝐴

𝑅 ∼𝑆 𝑅 :⇔ ′

∗

𝐴 =Γ 𝑆 ther, this gives us that for 𝑅post −→ Γ𝐴 also 𝑅post = 𝑅𝐴 −

𝑆

pre 𝑥𝑠

′

𝐴

∀𝑚, 𝑚 , 𝑟, 𝑟 . |blocks(𝑅 )| = 𝑟 ∗ 𝑘 + 𝑚 ∧ 𝑚 < 𝑘

® tx

Γ𝑅𝑆 −−→ . We hence, in particular, know that Γ𝐴 ≈𝑋 ∗ Γ𝑆 ′ pre

′

𝑆

′

′

∧ |blocks(𝑅 )| = 𝑟 ∗ 𝑘 + 𝑚 ∧ 𝑚 < 𝑘 ⇒ 𝑟 = 𝑟 ′ ∧ ∀𝑗 . 𝑗 < 𝑟 𝐴 𝐴 𝑆 𝑆 ∧ 𝑅𝐴 = 𝑅pre · 𝑅𝐴𝑗 · 𝑅post ∧ 𝑅𝑆 = 𝑅pre · 𝑅𝑆𝑗 · 𝑅post 𝐴 𝑆 ∧ |blocks(𝑅pre )| = 𝑗 ∗ 𝑘 ∧ |blocks(𝑅pre )| = 𝑗 ∗ 𝑘

∧ |blocks(𝑅𝐴𝑗 )| = 𝑘 ∧ |blocks(𝑅𝑆𝑗 )| = 𝑘 ® tx

∗

®′ tx

∗

∧ 𝑅𝐴𝑗 = Γ𝐴 −−→ Γ𝐴 ∧ 𝑅𝑆𝑗 = Γ𝑆 −−→ Γ𝑆 ′ 𝑥𝑠 ®

𝑥𝑠 ®

⇒ (∀𝑥𝑠. 𝑥𝑠 ∈ 𝑥𝑠 ® ⇔ 𝑥𝑠 ∈ 𝑥𝑠 ® ′)

∗

𝑥𝑠

and 𝑥𝑠 = 𝑥𝑠 ′ (since the initial configuration agreed on 𝑋 ∗ ). 𝐴 ∼ 𝑅 𝑆 by the definition of ∼ , this also Together with 𝑅pre 𝑆 pre 𝑆 𝑆 . Also, 𝑅 𝐴 = aRun𝜙 (𝐴, Γ , 𝑅 𝑆 , 0) gives us that 𝑅𝐴 ∼𝑆 𝑅pre init follows immediately from Lemma D.43 and the definition of aRun (note that the last argument to aRun denotes the additional invocations of the attacker after a complete round). • If 𝜙 (Γ𝑅𝑆 ) holds, we know that either Σ(Γ𝑅𝑆 ) = ∅ or Σ(Γ𝑅𝑆 ) = pre pre pre {tx}. We distinguish these two cases: – If Σ(Γ𝑅𝑆 ) = ∅ by assumption, we know in this case pre that Σ(Γ𝑅𝐴 ) = Σ(Γ𝑅𝑆 ). We can, hence, use Lemma D.46 pre

Note that here all unbound variables can be implicitly assumed to be universally quantified.

pre

𝑆 to deduce the existence of a valid simulator run 𝑅post 𝑆 such that |blocks(𝑅post )| = 𝑘. Further, this gives us that ® tx

D.2.7 Soundness Proof. We are now in the position to show the soundness of the generated interaction conditions. We first show the following slightly strengthened version of the soundness lemma, which will allow us to conclude the final soundness theorem. Lemma D.47 (Soundness). Let C be a contract with contract variables XC and 𝑋 Ev ⊆ XC the set of critical variables in C and u be a user. Let {SE𝑖 }f ∈ FC ,𝑖 ∈ {u,¬u} be sound and complete symbolic execution ref lations over X𝑖 with 𝑖 ∈ {u, ¬u}. Let 𝑋 ∗ ⊆ GC s.t. closeddeps (𝑋 ∗ ) C,f and 𝑋 Ev ⊆ 𝑋 ∗ . Let Σ = Σ𝑟→ be the user strategy for a round strategy Σ𝑟 (for u and C) such that (1) for all configurations Γ, Γ ′ with Γ ≈𝑋 ∗ Γ ′ it holds that Σ𝑟 (Γ) = Σ𝑟 (Γ ′ ) (2) for all configurations Γ, Σ𝑟 (Γ) ≠ ∅ implies that Σ𝑟 (Γ) = {tx} for some tx such that FRu𝜌 (Γ, tx, 𝑋 ∗ ) and BRu𝜌 (Γ, tx, 𝑋 ∗ ), and BRu𝜌 (Γ, 𝜏 , 𝑋 ∗ ) hold.

∗

®′ tx

∗

𝐴 = Γ 𝑆 for 𝑅post −→ Γ𝐴 also 𝑅post = Γ𝑅𝑆 −−→ Γ𝑆 for 𝑅𝐴 − ′ pre

pre

𝑥𝑠

′

𝑥𝑠

′

𝑆 )| = 𝑘 = ® with tx ® =\{𝜏 } tx ® . Since |blocks(𝑅post some tx ′ 𝐴 )|, we know that tx ® and tx ® must contain |blocks(𝑅post the same number of 𝜏 transactions and consequently that there needs to exist a permutation 𝜋 such that ® ′ = 𝜋 ( tx). ® Using Lemma D.41, we can hence show tx that also Γ𝐴 ≈𝑋 ∗ Γ𝑆 and 𝑥𝑠 ′ = 𝜋 (𝑥𝑠). Together with 𝐴 ∼ 𝑅 𝑆 by the definition of ∼ , this also gives us 𝑅pre 𝑆 pre 𝑆 𝑆 . Also, 𝑅 𝐴 = aRun𝜙 (𝐴, Γ , 𝑅 𝑆 , 0) folthat 𝑅𝐴 ∼𝑆 𝑅pre init lows immediately from Lemma D.43 and the definition of aRun. – If Σ(Γ𝑅𝑆 ) = {tx} by assumption, we know in this case pre −𝑣 ) for that Σ(Γ 𝐴 ) = Σ(Γ 𝑆 ) = {tx} and tx = C.f(→ 𝑅pre

𝑅pre

some f ∈ FC and that the interaction conditions hold in Γ𝑅𝑆 and Γ𝑅𝐴 . We can, hence, use Lemma D.44 to pre

pre

𝑆 such deduce the existence of a valid simulator run 𝑅post

On Identifying Sound Conditions for Frontrunning Resistance

D.3

𝑆 )| = 𝑘. Further, this gives us that for that |blocks(𝑅post ® tx

∗

𝐴 𝑆 𝑅post = Γ𝑅𝐴 −−→ Γ𝐴 also 𝑅post = Γ𝑅𝑆 pre

𝑥𝑠

pre

®′ tx

Relation to TOD

∗

Contracts with non-round-based user strategies can be free of TOD and still not satisfy DS Resistance. For example, consider the following two functions which are trivially free of TOD, since none of them change the contract state:

−−→ Γ𝑆 for ′ 𝑥𝑠

® ′ with tx ® =\{tx,𝜏 } tx ® ′ . We know from the transsome tx action inclusion guarantee that since tx ∈ Σ(Γ𝑅𝐴 ) pre

® We also know (from Definition D.44) that also tx ∈ tx. 𝑆 ) [0] = [tx] and so tx ∈ tx ® ′ . Since transacblocks(𝑅post tions only appear once in a given run, we get from ® =\{tx} tx ® ′ that there needs to exist a permutation 𝜋 tx ® ′ = 𝜋 ( tx). ® Using Lemma D.40, we can hence such that tx show that also Γ𝐴 ≈𝑋 ∗ Γ𝑆 and 𝑥𝑠 ′ = 𝜋 (𝑥𝑠). Together 𝐴 ∼ 𝑅 𝑆 by the definition of ∼ , this also gives with 𝑅pre 𝑆 pre 𝑆 𝑆 . Also, 𝑅 𝐴 = aRun𝜙 (𝐴, Γ , 𝑅 𝑆 , 0) folus that 𝑅𝐴 ∼𝑆 𝑅pre init lows immediately from Lemma D.43 and the definition of aRun. □ With this, we show our final soundness theorem, which establishes that a smart contract and together with any round-based user strategy that respects the synthesized interaction conditions for the contract, satisfies DS Resistance. Theorem D.48 (Soundness of Interaction Conditions). Let C be a contract with contract variables XC and 𝑋 Ev ⊆ XC the set of critical variables in C and u be a user. Let {SE𝑖 }f ∈ FC ,𝑖 ∈ {u,¬u} be sound f and complete symbolic execution relations over X𝑖 with 𝑖 ∈ {u, ¬u}. C,f Let 𝑋 ∗ ⊆ GC s.t. closeddeps (𝑋 ∗ ) and 𝑋 Ev ⊆ 𝑋 ∗ . Let Σ = Σ𝑟→ be the user strategy for a round strategy Σ𝑟 (for u and C) such that (1) for all configurations Γ, Γ ′ with Γ ≈𝑋 ∗ Γ ′ it holds that Σ𝑟 (Γ) = Σ𝑟 (Γ ′ ) (2) for all configurations Γ, Σ𝑟 (Γ) ≠ ∅ implies that Σ𝑟 (Γ) = {tx} for some tx such that FRu𝜌 (Γ, tx, 𝑋 ∗ ) and BRu𝜌 (Γ, tx, 𝑋 ∗ ) and BRu𝜌 (Γ, 𝜏 , 𝑋 ∗ ) hold. Let 𝜙 be defined as follows: 𝜙 (Γ) :⇔ BRu𝜌 (Γ, 𝜏 , 𝑋 ∗ ) ∧ ∃tx. FRu𝜌 (Γ, tx, 𝑋 ∗ ) ∧ BRu𝜌 (Γ, tx, 𝑋 ∗ ) Let 𝑅𝐴 be an attacker run such that (𝐴, Σ) ⊢ 𝑅𝐴 . Then there exists a 𝜙 run 𝑅𝑆 such that (𝑆 𝐴 , Σ) ⊢ 𝑅𝑆 and 𝑅𝐴 ∼𝑆 𝑅𝑆 . Proof. The statement follows immediately from Lemma D.47 and the definition of ∼𝑆 since we know that for a run 𝑅𝐴 it needs 𝐴 · 𝑅 𝐴 such that |blocks(𝑅 𝐴 )| = 𝑟 ∗ 𝑘 and to hold that 𝑅𝐴 = 𝑅pre pre post 𝐴 |blocks(𝑅post )| = 𝑖 for some 𝑖, 𝑘 ∈ N with 𝑖 < 𝑘. Consequently, from 𝑆 such that Lemma D.47, we can deduce the existence of a run 𝑅pre 𝐴 𝐴 𝑆 |blocks(𝑅pre )| = 𝑟 ∗ 𝑘 and 𝑅pre ∼𝑆 𝑅pre . By the definition of ∼𝑆 , we 𝑆 , which concludes the know that then it also holds that 𝑅𝐴 ∼𝑆 𝑅pre proof. □ Note that this theorem indeed proves DS Resistance since the 𝜙 simulator 𝑆 𝐴 only depends on the attacker 𝐴 and the contract C (via the condition 𝜙 that is derived from the contract code using the algorithm for synthesizing interaction conditions) but the user strategy Σ remains arbitrary (satisfying the required conditions). So, in particular, the theorem implies DS Resistance for all sets of user strategies ΣC such that all Σ ∈ ΣC satisfy the required conditions.

1 2 3 4

function test ( uint b ) { /* Noop function trigger () { emit Triggered ( msg . sender ) ; }

*/ }

Still, for the following set of user strategies, the contract does not satisfy DS Resistance: ΣnoTOD := {Σ𝑏 | 𝑏 ∈ {0, 1} ∧ Σ𝑏 (Γ) ≠ [] ⇒ Σ𝑏 (𝑅) = [ test (u : 0T, 𝑏)] ∧ test (u : 0T, 𝑏) ∉ 𝑅 ∨ Σ𝑏 (𝑅) = [ trigger (u : 0T)] test (u:0T,𝑏 )

∧ 𝑅 = 𝑅pre −−−−−−−−−−→ Γ ′ · 𝑅post ∧ |𝑅pre | mod 2 = 𝑏} ΣnoTOD contains two user strategies, Σ

0 and Σ1 . Both strategies initially submit a transaction to invoke the test function with argument b. Then, Σ0 only submits a trigger transaction, exactly if their test transaction was included in an even block and Σ0 submits a trigger transaction, exactly if their test transaction was included in an odd block. Now, an adaptive attacker 𝐴 can, when observing the argument of the test transaction, deduce in which block they need to include it to make the user strategy submit the trigger transaction next. Like this, 𝐴 can reliably produce the event Triggered (u) for the honest user u for both Σ0 and Σ1 . Instead, a non-adaptive attacker always needs to place the user transaction in the same block and hence will not be able to produce the event Triggered (u) for both Σ0 and Σ1 . This example, while artificial, underlines how a user strategy’s dependence can easily enable deckstacking attacks.