PaperlayerView exact revision on arXiv

Source-linked AI summary

A Semantic Framework for the Security Analysis of Ethereum smart contracts

Ilya Grishchenko, Matteo Maffei, Clara Schneidewind

arXiv:1802.08660v2cs.CR

TL;DR

Smart contracts require rigorous security analysis, but vulnerabilities are financially dangerous and analysis is complicated by Solidity and low-level EVM execution. The paper provides complete EVM-bytecode small-step semantics formalized in F*, defines central security properties, validates the semantics against Ethereum’s official test suite, and identifies unsound or incomplete existing verification conditions.

  • Problem

    Smart-contract vulnerabilities can cause catastrophic losses, while rigorous analysis is complicated by Solidity’s specialized behavior and low-level EVM bytecode.

  • Method

    The paper develops complete small-step EVM-bytecode semantics, formalizes a large fragment in F*, and defines security properties using hyper- and safety properties.

  • Results

    The F* formalization was validated against the official Ethereum test suite, while comparisons showed existing Oyente verification conditions are neither sound nor complete.

  • Takeaways & Limitations

    The framework provides semantic and security foundations intended to facilitate rigorous future analysis of Ethereum smart contracts.

  • Takeaways & Limitations

    The examined Oyente versions failed to detect transaction-order dependency and incorrectly flagged at least one correctly guarded contract as reentrant.

Abstract

from arXiv · show

Smart contracts are programs running on cryptocurrency (e.g., Ethereum) blockchains, whose popularity stem from the possibility to perform financial transactions, such as payments and auctions, in a distributed environment without need for any trusted third party. Given their financial nature, bugs or vulnerabilities in these programs may lead to catastrophic consequences, as witnessed by recent attacks. Unfortunately, programming smart contracts is a delicate task that requires strong expertise: Ethereum smart contracts are written in Solidity, a dedicated language resembling JavaScript, and shipped over the blockchain in the EVM bytecode format. In order to rigorously verify the security of smart contracts, it is of paramount importance to formalize their semantics as well as the security properties of interest, in particular at the level of the bytecode being executed. In this paper, we present the first complete small-step semantics of EVM bytecode, which we formalize in the F* proof assistant, obtaining executable code that we successfully validate against the official Ethereum test suite. Furthermore, we formally define for the first time a number of central security properties for smart contracts, such as call integrity, atomicity, and independence from miner controlled parameters. This formalization relies on a combination of hyper- and safety properties. Along this work, we identified various mistakes and imprecisions in existing semantics and verification tools for Ethereum smart contracts, thereby demonstrating once more the importance of rigorous semantic foundations for the design of security verification techniques.

1 Introduction

The paper establishes rigorous semantic foundations for analyzing Ethereum smart-contract security at the EVM-bytecode level. It formalizes execution and key security properties, validates the semantics, and exposes weaknesses in existing analysis techniques.

  • Motivation: Smart-contract vulnerabilities can have catastrophic financial consequences, including the DAO attack’s 60M$ loss.The paper also notes that fraudulent contracts occur in practice.
  • Motivation: The paper addresses the difficulty of rigorous smart-contract analysis caused by Solidity’s specialized behavior and low-level EVM bytecode with dynamic creation and invocation.These challenges make static information scarce and analysis difficult.
  • Contributions: The work introduces the first complete small-step semantics for EVM bytecode and formalizes a large fragment in F*.The formalization supports verification techniques and machine-checked proofs.
  • Contributions: The executable F* formalization was successfully validated against the official Ethereum test suite.The complete semantics and F* formalization are publicly available.
  • Contributions: The paper formally defines call integrity, atomicity, and independence from miner-controlled parameters using hyper- and safety properties.Existing static analyses instead rely on reachability properties and syntactic conditions.
  • Results: Examples show that syntactic conditions in current analysis techniques are imprecise and, in several cases, unsound.The findings motivate solid semantic foundations and rigorous security definitions.

2 Background on Ethereum

Ethereum represents account state on a blockchain and executes contract code through the gas-bounded EVM. Contracts use EVM bytecode and are commonly authored in Solidity, whose call behavior can involve failures and code execution.

  • Ethereum: Ethereum’s global state contains external accounts with balances and contract accounts with persistent storage and code.Accounts and transactions are organized within a blockchain maintained through proof-of-work consensus.
  • Transactions: Transactions create contract accounts or call existing accounts, with contract calls additionally executing code that may alter storage or perform internal transactions.Calls to external accounts only transfer Ether.
  • Execution: Gas bounds EVM execution by limiting the number of instruction steps, despite the underlying language being quasi Turing-complete.The transaction originator specifies the maximum gas and gas price.
  • EVM Bytecode: EVM bytecode is assembler-like code for a stack-based machine, with instructions for computation, control flow, storage, environment access, calls, creation, and self-destruction.The bytecode includes SHA3 and blockchain-specific operations.
  • Gas and Exceptions: Exceeding the gas limit raises an exception that reverts the current transaction’s global-state effects.Nested-transaction exceptions revert only the nested transaction’s effects.
  • Solidity: Most contracts are written in Solidity, whose low-level send and call functions can transfer Ether while also invoking code that may fail.These calls do not automatically propagate exceptions.

3 Small-Step Semantics

The paper defines a revised small-step semantics for EVM bytecode, formalized in F* and designed to support executable execution and verification. It models transaction environments, global and local machine state, call stacks, arithmetic, internal calls, and final execution outcomes.

  • Semantic scope: The semantics substantially revises prior EVM models to cover the full bytecode instruction set, including contract calls and creation.The authors also report finding and fixing a major call-related flaw and several minor errors in existing work.
  • State model: The global state maps account addresses to accounts containing nonce, balance, persistent storage, and contract code.External accounts have empty bytecode, while contract execution can access and modify account storage.
  • Callstacks: Call stacks contain regular execution states and may be topped by HALT or EXC states representing normal or exceptional termination.Exceptions revert the terminated internal transaction’s effects, whereas halting states retain global state, remaining gas, return data, and transaction effects.
  • Execution states: A regular execution state combines the global state, transaction environment, local stack-machine state, and accumulated transaction effects.The transaction environment records immutable execution parameters such as actor, input, sender, value, and code.
  • Execution states: The local machine state tracks gas, program counter, memory, active memory words, and the 256-bit stack, starting from a fresh zeroed configuration for each internal transaction.Only the available gas is instantiated initially; stack, memory, program counter, and active memory words start empty or zero.
  • Small-step rules: The ADD rule updates the stack and program counter while charging three gas units, whereas CALL transfers value and creates a fresh internal execution state.The presented CALL rule assumes an existing recipient, stack depth below 1024, and sufficient balance.
  • Formalization in F*: The F* formalization implements execution through stepwise call-stack evolution and an execution function that runs until a final state is reached.The executable formalization was validated against the official Ethereum test suite and is publicly available to support analysis and soundness proofs.

4 Security Definitions

The paper defines security properties for smart contracts that address attacker-controlled calls, gas-dependent execution, and miner influence, and compares them with existing verification conditions. It also identifies limitations and soundness gaps in current analyses.

  • 4.1 Call Integrity: Call integrity captures whether untrusted code can control a contract’s outgoing calls, even when the contract transfers control to an attacker.The property is formulated as a hyperproperty over alternative attacker schedules, call stacks, and execution traces.
  • 4.2 Proof Technique for Call Integrity: Three local conditions—local independence, effect independence, and single-entry—together entail call integrity for a set of untrusted addresses.The paper establishes this implication as a sound proof technique for the hyperproperty of call integrity.
  • Exception Handling: Atomicity requires contract effects to be independent of available gas, with an exception-triggering execution reverting the overall execution.This addresses inconsistent states caused when nested calls revert their effects while the caller continues and updates its own state.
  • 4.4 Independence of Miner controlled Parameters: Miner independence requires outgoing Ether flows to avoid dependence on miner-controlled transaction-environment values and transaction-influenced contract state.The definitions cover timestamp dependency and related dependence on execution context shaped by prior transactions.
  • 4.5 Classification of Bugs: The security properties do not cover all known bugs, including unexpected runtime exceptions and bugs caused by Solidity semantics that diverge from programmer intuitions.Correct exception handling is contract-specific; atomicity provides a generic condition for out-of-gas cases but may not characterize other runtime exceptions.
  • 4.6 Discussion: The authors find that Oyente’s verification conditions are neither sound nor complete, with examples of false positives, false negatives, and missed dependencies.The discussion includes timestamp dependence missed by local-path characterization, incorrect reentrancy classifications, and syntactic checks that do not ensure atomicity.

5 Conclusions

The paper provides formal semantic and security foundations for Ethereum smart contracts, validates a large F* formalization, and identifies directions for extending verification support.

  • The work defines salient smart-contract security properties using a combination of hyper-properties and safety properties.The framework includes properties such as call integrity, atomicity, and independence from miner-controlled parameters.
  • The framework is made available to the academic community to support future research on rigorous smart-contract security analysis.
  • Future work includes formalizing Solidity semantics and compilation into EVM, with a soundness proof against the EVM semantics.The stated goal is to support verification from Solidity through bytecode that is secure by construction.

A Formalization

The formalization defines the mathematical components of EVM configurations, including bitstrings, bytearrays, accounts, call stacks, and transaction environments. These structures capture execution state, exceptional and regular halting, persistent global state, and immutable transaction context.

  • A.1 Notations: Bitstrings, non-negative integers, arrays, and lists provide the basic notation for representing EVM data structures.The formalization uses B, Bx, Nx, [X], and L(X), with implicit conversion between fixed-size bitstrings and unsigned integers.
  • A.1 Notations: Ethereum account addresses are modeled as 160-bit values.The address set is A = B160.
  • A.2 Configurations: The global state is a partial mapping from account addresses to accounts containing nonce, balance, persistent storage, and bytecode.Each account records balance and nonce in N256, storage as a mapping from 256-bit keys to 256-bit values, and code as a bytearray.
  • A.2 Configurations: A call stack tracks nested calls through regular execution states and top-level exceptional or regular halting states.Regular states contain machine state, execution environment, global state, and transaction effects; halting states record exceptions or successful termination data.
  • A.2 Configurations: Global state belongs in the call stack because exceptions revert a call’s effects and resume execution using the caller’s state.The same rollback principle applies to transaction effects.
  • A.2 Configurations: The formal syntax of call stacks is specified explicitly and summarized by a complete grammar.The grammar organizes execution states and the associated components used by the semantics.
  • A.3 Transaction environment: The transaction environment is a tuple containing the originator address, gas price, and block header.The block header includes parent, beneficiary, difficulty, number, gas limit, and timestamp.

B Small step semantics

The semantics defines execution as a small-step relation that evolves a call stack under a fixed transaction environment.

  • B Small step semantics: The relation Γ ⊨ S → S′ models one execution step from call stack S to S′ under transaction environment Γ.The transaction environment supplies block and transaction information that remains unchanged during code execution.

B.1 Notations

The formalization introduces notation for accessing and updating global state, memory, tuple components, and signed or unsigned machine values.

  • B.1 Notations: Global-state notation accesses accounts by address and provides simplified update operations for account state.This notation reflects that global state is a mapping from addresses to accounts.
  • B.1 Notations: Memory fragments are represented by offset-and-size slices, and updates replace bounded portions with supplied bytearrays.The update range is limited by both the requested size and the length of the replacement value.
  • B.1 Notations: Bitvector slices and concatenation support extraction and recombination of machine-word data.The notation extracts bits between specified positions and joins bitvectors into larger values.
  • B.1 Notations: Named tuple components and update notation improve readability when manipulating execution-state records.For example, program-counter updates can be written directly as µ[pc → µ.pc + 1].
  • B.1 Notations: Bitvectors and unsigned integers are interpreted interchangeably, while signed conversion functions support operations using signed machine words.Conversion functions map between Bx or Nx and Intx, then return unsigned representations.

B.2 Auxiliary definitions

Auxiliary definitions specify instruction access, validity checks, jump destinations, memory expansion costs, and fresh account-address generation for the EVM semantics.

  • B.2 Auxiliary definitions: The currently executed EVM command is obtained from the instruction at the machine state’s program counter.A dedicated function formalizes this lookup from machine state and execution environment.
  • B.2 Auxiliary definitions: The valid function detects insufficient gas and invalid resulting stack sizes, while individual rules handle stack underflows by pattern matching.These conditions produce exceptions during instruction execution.
  • B.2 Auxiliary definitions: Valid jump destinations are exactly code positions occupied by JUMPDEST, with PUSHn data skipped when scanning bytecode.The destination-set function recursively advances to the next valid instruction position.
  • B.2 Auxiliary definitions: Memory expansion is modeled by tracking active words and charging costs for newly activated memory.The memory-cost function maps the number of active words before and after execution to the corresponding additional cost.
  • B.2 Auxiliary definitions: The newAddress function derives a fresh account address from an existing address and nonce.The construction uses RLP encoding and assumes collision resistance.

B.3 Small-step rules

Binary EVM operations are specified uniformly through operation-specific functionality and gas-cost mappings, with small-step rules updating the stack, program counter, and gas. The rules also cover exponentiation and Keccak-256 hashing, whose costs or state effects differ from ordinary binary operations.

  • Binary stack operations: Each binary operation is modeled through a common rule using its functionality and gas-cost mapping.The rule consumes two stack values, pushes the computed result, advances the program counter, and subtracts the operation cost.
  • Binary stack operations: The binary instruction set includes arithmetic, comparisons, bitwise operations, multiplication, division, modulo, sign extension, and byte extraction.The listed operations include ADD, SUB, LT, GT, EQ, AND, OR, XOR, SLT, SGT, MUL, DIV, SDIV, MOD, SMOD, SIGNEXTEND, and BYTE.
  • Binary stack operations: Simple binary operations use constant costs of 3 or 5 gas, depending on the operation class.The 3-gas class includes arithmetic comparisons and BYTE, while the 5-gas class includes multiplication, division, modulo, and related operations.
  • Exceptional operations: Exponentiation computes (a^b) mod 2^256 and charges a cost based on the exponent, with a base cost of 10 gas when b is zero.For nonzero b, the cost is 10 + 10 · (1 + floor(log256 b)).
  • Exceptional operations: SHA3 reads a memory segment, computes its Keccak-256 hash, pushes the hash onto the stack, and updates the active memory-access information.Its cost combines memory expansion with a fixed and size-dependent component.

Unary stack operations

Unary stack operations transform one stack value and charge fixed gas while preserving the small-step state-transition pattern. ISZERO tests equality with zero, whereas NOT applies bitwise negation.

  • Unary stack operations: ISZERO replaces the top stack value with 1 when it is zero and 0 otherwise, costing 3 gas.The rule advances the program counter and preserves the remainder of the stack.
  • Unary stack operations: NOT replaces the top stack value with its bitwise negation and costs 3 gas.The transition advances the program counter and deducts 3 gas when the stack and gas are valid.
  • Unary stack operations: Both unary instructions require sufficient gas and at least one stack element before execution.Invalid gas or stack conditions produce no valid execution rule.

Ternary stack operations

The rules define ternary arithmetic and instructions that access or copy call data and code. These operations validate gas and stack shape, then update the stack or memory while accounting for copied lengths and memory expansion.

  • Ternary stack operations: ADDMOD and MULMOD consume three stack values and return modular addition or multiplication, yielding 0 when the modulus is zero.Both instructions cost 8 gas and update the stack, program counter, and gas.
  • Ternary stack operations: ADDMOD and MULMOD require at least three stack values and valid 8-gas execution capacity.The failure condition combines insufficient gas with an undersized stack.
  • Environment access: Environment-access instructions such as ADDRESS, CALLER, CALLVALUE, CODESIZE, and CALLDATASIZE push corresponding execution-context values onto the stack.Each operation uses a fixed 2-gas rule and requires valid gas and stack capacity.
  • Call-data access: CALLDATALOAD reads up to 32 bytes from call input, right-pads short reads with zeros, and writes the resulting 256-bit value to the stack.Out-of-range positions produce zero-filled results.
  • Call-data access: CALLDATACOPY copies a selected input segment into memory and zero-pads missing bytes.The rule computes the copied length, expands memory, writes the bytes, and charges the resulting gas cost.
  • Code access: CODECOPY copies the currently executed code into memory, padding beyond the available code with STOP bytes.As with CALLDATACOPY, the transition accounts for memory expansion and the copied range.

Accessing the transaction environment

Transaction-environment instructions expose transaction, block, and gas information by pushing context values onto the stack. BLOCKHASH additionally searches recent ancestors for a requested block hash.

  • Transaction and block context: ORIGIN, COINBASE, TIMESTAMP, NUMBER, and DIFFICULTY push transaction-origin or block-header values onto the stack.These instructions use fixed 2-gas transitions that advance the program counter.
  • Block hash access: BLOCKHASH takes a block number from the stack and pushes the corresponding hash when it lies within the 256 most recently completed blocks.The lookup starts from the parent block and costs 20 gas.
  • Block hash access: The BLOCKHASH search stops when it reaches 256 traversed ancestors, the genesis block, or a requested number greater than the current block number.Otherwise, the search recursively follows parent links until it finds the requested block.
  • Gas context: GASLIMIT and GASPRICE expose the block gas limit and transaction gas price through the same stack-transition pattern.Both instructions push their corresponding context values and charge 2 gas.
  • Execution validity: These environment instructions require valid gas and sufficient stack space before pushing their results.The corresponding invalidity condition is specified for the 2-gas environment-access operations.

Accessing the global state

The semantics formalize instructions that access account state and code, updating the stack, program counter, gas, memory, or instruction state as specified.

  • Account and code access: BALANCE pushes an account’s balance when the address is valid, otherwise zero, and charges 400 gas.The address is obtained from the stack; the stack and program counter are updated.
  • Account and code access: EXTCODESIZE pushes the size of the addressed account’s code and charges 700 gas.The address is reduced modulo 2160 before the code size is read.
  • Account and code access: EXTCODECOPY reads code from an addressed account and copies the selected fragment into local memory.The copied length is bounded by the requested size and available code length, with memory and instruction state updated.

Stack operations

The semantics specify stack manipulation, control flow, memory and storage access, halting, account destruction, calls, logging, and execution-state queries through explicit small-step rules.

  • Stack manipulation: PUSHn, DUPn, and SWAPn respectively push bytecodes, duplicate a selected stack element, and exchange the first and nth elements.PUSHn supports n from 1 to 32, while DUPn and SWAPn support n from 1 to 16; each rule charges 3 gas.
  • Control flow: JUMP updates the program counter only for a valid destination, while JUMPI selects the destination when b is nonzero and otherwise advances sequentially.The rules charge 8 gas for JUMP and 10 gas for JUMPI, with invalid conditions handled separately.
  • Local memory: MLOAD reads 32 bytes from local memory onto the stack, whereas MSTORE and MSTORE8 write 32 bytes or one byte, respectively.Memory expansion contributes to the cost through Cmem, and MSTORE8 stores b mod 256.
  • Persistent storage: SLOAD reads persistent storage, while SSTORE writes a value and applies gas costs based on whether a zero slot becomes nonzero.Clearing a previously nonzero slot yields a 15000 balance refund.
  • Halting: RETURN halts execution while recording memory data for possible propagation, whereas STOP halts without propagating data.RETURN produces HALT(σ, g, d, η), while STOP produces an empty return value.
  • Calls and execution state: CALL initiates execution of another account’s code using supplied gas, value, input memory, and a designated return-data region.GAS and MSIZE expose execution-state values on the stack, while LOGn records an address, topics, and memory data for external observers.
Loading 1802.08660v2…