PaperlayerView exact revision on arXiv

Source-linked AI summary

VeriSolid: Correct-by-Design Smart Contracts for Ethereum

Anastasia Mavridou, Aron Laszka, Emmanouela Stachtiari, Abhishek Dubey

arXiv:1901.01292v2cs.CRcs.SE

TL;DR

Smart contracts can contain vulnerabilities, and blockchain platforms typically make deployed code and transactions difficult to change or reverse. VeriSolid applies formal verification to transition-system models and generates Solidity code from verified designs. Its case studies include verified properties, excluded modeled attacks, and detected liveness violations.

  • Problem

    Smart-contract vulnerabilities can expose digital assets, while platform immutability makes correcting deployed code or reversing malicious transactions difficult.

    Source: §1 · p. 3

  • Method

    VeriSolid verifies high-level transition-system models against developer-specified properties and generates Solidity code through an end-to-end design flow.

    Source: §1 · p. 4, §7 · p. 18

  • Results

    Across case studies, VeriSolid verified stated Blind Auction properties, excluded both modeled DAO attacks, and found liveness violations in both King of Ether versions.

    Source: §5.2 · p. 16, The DAO Attack · p. 16, King of the Ether Throne · p. 17

  • Takeaways & Limitations

    VeriSolid’s transformations preserve established properties in the resulting smart contracts, supporting its correct-by-design approach.

    Source: §7 · p. 18

    VeriSolid prevents re-entrancy by design, a deliberate scope choice because supporting re-entrancy substantially increases verification complexity.

    Source: Lack of the Re-entrancy Vulnerability · p. 9

Abstract

from arXiv · show

The adoption of blockchain based distributed ledgers is growing fast due to their ability to provide reliability, integrity, and auditability without trusted entities. One of the key capabilities of these emerging platforms is the ability to create self-enforcing smart contracts. However, the development of smart contracts has proven to be error-prone in practice, and as a result, contracts deployed on public platforms are often riddled with security vulnerabilities. This issue is exacerbated by the design of these platforms, which forbids updating contract code and rolling back malicious transactions. In light of this, it is crucial to ensure that a smart contract is secure before deploying it and trusting it with significant amounts of cryptocurrency. To this end, we introduce the VeriSolid framework for the formal verification of contracts that are specified using a transition-system based model with rigorous operational semantics. Our model-based approach allows developers to reason about and verify contract behavior at a high level of abstraction. VeriSolid allows the generation of Solidity code from the verified models, which enables the correct-by-design development of smart contracts.

1 Introduction

Blockchain platforms enable self-enforcing smart contracts, but deployed contracts can contain vulnerabilities, and immutable code and transactions make later correction difficult. VeriSolid combines high-level formal verification with a design framework and Solidity code generation.

1 Introduction

  • Vulnerabilities can expose digital assets, while blockchain platforms typically prevent contract-code updates and transaction reversals.The introduction cites a study finding 8,333 of 19,336 deployed Ethereum contracts had at least one security issue, alongside the DAO and Parity losses.Source: §1 · p. 3
  • Secure practices and automated scanners have limits, while formal verification can detect atypical vulnerabilities but is harder to automate.Practices depend on error-prone implementation and cannot guarantee safety; generic scanners may miss contract-specific or atypical issues and can produce false positives.Source: §1 · p. 4
  • VeriSolid combines formal verification with an end-to-end design framework, letting developers specify and verify contract properties against high-level models.It reports no false positives for safety properties and deadlock-freedom; violations are accompanied by execution sequences that can help identify design errors.Source: §1 · p. 4
  • VeriSolid extends FSolidM with formal operational semantics, Solidity support, and natural-language-like templates for safety and liveness properties.The framework also transforms Solidity actions into an augmented transition system and proves it observationally equivalent to the initial model.Source: Contributions · p. 5
  • The framework uses overapproximation for verification and integrates nuXmv and BIP, with verification results presented.The stated goal is meaningful and efficient verification of smart-contract models.Source: Contributions · p. 5

2 VeriSolid: Design and Verification WorkFlow

VeriSolid provides a web-based workflow for specifying Ethereum contracts and properties, verifying models, refining designs, and generating Solidity code. Developers can collaborate through version control, and the graphical workflow includes both mandatory and optional steps.

2 VeriSolid: Design and Verification WorkFlow

  • Developers provide a graphical transition-system contract specification, Solidity declarations, actions and guards, plus properties expressed with predefined templates.The framework is web-based and supports collaborative development with branching, merging, and history viewing.Source: §2 · p. 5
  • VeriSolid generates a BIP model and translates specified properties to CTL, then checks deadlock freedom and other properties with BIP tools or nuXmv.If properties fail, developers can refine the specification and analyze it again; Figure 1 marks mandatory steps with solid arrows and optional steps with dashed arrows.Source: §2 · pp. 5–6, Figure 1 · p. 6
  • Once developers are satisfied that the specified properties hold, VeriSolid automatically generates equivalent Solidity code.The workflow is illustrated in Figure 1; Figure 2 shows the web-based graphical editor.Source: §2 · pp. 5, 7, Figure 1 · p. 6, Figure 2 · p. 6

3 Developer Input: Transition Systems and Properties

The section models smart contracts as transition systems and defines their execution and verification properties, using the blind auction to illustrate states, transitions, guards, and actions.

3.1 Smart Contracts as Transition Systems

  • The blind auction is represented by states for bidding, revealing, finishing, or cancellation, connected by guarded user actions such as bid, reveal, finish, and withdraw.The transition-system abstraction provides an intuitive basis for reasoning about contract behavior.Source: §3.1 · pp. 7–8

3.2 Formal Definition of a Smart Contract

  • A contract is defined by its states, variables, and transitions, whose components include a source state, parameters, guard, action, and destination state.The model also accounts for constructor and fallback actions; VeriSolid prevents re-entrancy by moving to a temporary state before executing a transition action.Source: §3.2 · p. 9, Lack of the Re-entrancy Vulnerability · p. 9

3.3 Smart-Contract Operational Semantics

  • Structural Operational Semantics rules specify transition execution: a satisfied guard permits the action, and normal completion commits the updated ledger and contract states.The rules also cover erroneous execution and returned values.Source: §3.3 · pp. 9–10

3.4 Safety, Liveness, and Deadlock Freedom

  • VeriSolid automatically checks deadlock freedom and lets developers specify safety and liveness properties through natural-language-like templates or CTL.For example, safety properties can require the withdrawal balance reset to occur before the transfer, while a liveness property can require the reset eventually after transfer.Source: §3.4 · pp. 10–11

4 Augmented Transition System Transformation

The framework transforms Solidity actions into an augmented transition system for verification and proves that the augmented and initial contracts are observationally equivalent.

4 Augmented Transition System Transformation

  • The transformation replaces constructor and fallback actions with transitions and decomposes complex actions into transitions containing simple statements.The resulting augmented model captures contract behavior using transitions and can be input to verification tools.Source: §4 · p. 12

4.1 Observational Equivalence

  • Theorem 1 establishes observational equivalence between each initial smart contract and its corresponding augmented contract.The equivalence supports carrying verified properties of the augmented model back to the initial model.Source: §4.1 · p. 13

5 Verification Process

VeriSolid abstracts data and time to check contract properties, maps transition systems into BIP, and applies the process to auction, attack, and platform-contract models.

5 Verification Process

  • Data abstraction leaves environmental-input-dependent guards unevaluated, exploring both transition outcomes and a superset of concrete states and traces.Variables independent of environmental input, such as known-range iteration counters, are updated according to contract statements.Source: §5 · p. 14
  • Time abstraction represents threshold crossings rather than elapsed time: upper-bound guards gain invalidating loops, while lower-bound guards advance to tmin+1.The lower-bound treatment supports checking bounded liveness properties.Source: §5 · p. 14
  • The abstraction preserves safety proofs and deadlock-freedom when absent in the abstract model, while abstract-model liveness violations also hold in the concrete model.The paper relates these checks to withdrawal vulnerabilities and denial-of-service vulnerabilities, respectively.Source: §5 · pp. 14–15

5.1 VeriSolid-to-BIP Mapping

  • VeriSolid-to-BIP uses a one-to-one, single-pass syntax-directed mapping of states, transitions, guards, actions, and variables into a BIP code template.The template distinguishes generated fixed-width text from italic input-replaced elements.Source: §5.1 · p. 15, Figure 7

5.2 Verification Results

  • All checked Blind Auction properties held, and the initial and augmented models had 54 and 161 reachable states, respectively.The models were also found deadlock-free.Source: §5.2 · p. 16
  • The verified DAO safety property excludes both described attacks, while King of the Ether models yield counterexamples to crowning-related liveness properties.The counterexamples are fallback →4 →5 and fallback →4.Source: The DAO Attack · p. 16, King of the Ether Throne · p. 17
  • The transactive-energy platform core had 3,487 reachable states, and properties were verified or shown violated within seconds.The verification results are presented in Appendix G.3.Source: Resource Allocation · p. 17

6 Related Work

Related work addresses smart-contract vulnerabilities through verification, vulnerability discovery, and development tools. VeriSolid emphasizes high-level models and checking developer-specified properties.

6 Related Work

  • VeriSolid lets developers specify desired properties on high-level models and inspect developer-friendly results and counterexamples, enabling checks beyond known vulnerability types.The approach is contrasted with analysis of EVM bytecode and detection of only certain vulnerability types.Source: §6 · p. 17
  • Prior work includes EVM and Solidity semantics, design-pattern studies, and tools ranging from theorem-prover verification to symbolic vulnerability analysis.The passage also describes runtime verification.Source: §6 · pp. 17–18
  • Vulnerability-discovery tools target selected issues or analyze bytecode, including Oyente, MAIAN, Vandal [10], Mythril, and Rattle.EthIR builds on Oyente to enable property inference from EVM code.Source: §6 · p. 18

7 Conclusion

VeriSolid links formal verification to Solidity generation through a sequence of equivalent transformations, aiming to preserve verified properties in deployed contracts. Its appendices define the supported Solidity subset and the operational rules used to model transition execution.

7 Conclusion

  • VeriSolid’s design flow transforms transition systems through augmented, BIP, and NuSMV models into functionally equivalent Solidity code, preserving properties established along the flow.The initial and augmented transition systems are observationally equivalent; the BIP-to-NuSMV transformation is also described as observationally equivalent.Source: §7 · p. 18

A.1 Supported Solidity Subset

  • The supported Solidity subset includes declarations, events, returns, conditionals, loops, and compound statements, with expressions separated by whether they have side effects.The appendix defines notation for supported types, identifiers, definitions, expressions, and statements.Source: §A.1 · pp. 23–24

A.2 Operational Semantics of the Transition System

  • Transition execution initializes state from call parameters and the ledger, checks the guard, runs the action, and commits updated states only after normal completion.A false guard, a mismatched source state, or an exception can prevent the transition from taking effect.Source: §A.2 · pp. 24–26

A.3 Operational Semantics of Supported Solidity Statements

  • Small-step rules model supported statements by mapping execution state, status, and remaining statement to their next values, while exceptions and returns stop further execution.The rules cover control flow such as loops and conditionals, as well as declarations, expressions, events, returns, and compound statements.Source: §A.3 · p. 26, Loop Statements · p. 27

B Templates and CTL for Property Specification

This appendix explains how VeriSolid expresses contract properties using CTL and provides templates for specifying them. It also outlines Solidity calls that can affect contract execution and state.

B.1 Background on CTL

  • CTL formulas describe properties of transition-system execution trees using branch quantifiers and temporal operators, and a property holds when it is satisfied in the initial state.For example, A[p W q] requires p until q occurs on every branch, or forever if q never occurs.Source: §B.1 · pp. 28–29

B.2 Templates and Corresponding CTL formulas

  • VeriSolid offers natural-language-like templates that correspond to CTL formulas, while also allowing developers to specify properties directly in CTL.The appendix lists templates and corresponding formulas for safety and liveness properties.Source: §B.2 · p. 29, Table 3 · p. 29, Table 4 · p. 29

C.1 Solidity Function Calls

  • A low-level Solidity call uses ABI-encoded data and returns a Boolean, including true when no contract exists at the address.The passage contrasts this behavior with high-level calls, which may return a value or raise an exception on failure.Source: §C.1 · p. 30
  • A failed high-level call raises an exception in the caller, reverting its changes and propagating the exception up the call hierarchy.If the named function does not exist, the callee’s fallback function is invoked when present.Source: §C.1 · p. 30
  • Sending ether with send invokes the recipient’s fallback function when present and returns false on failure, whereas transfer raises an exception on failure.Both methods send the specified amount of currency to the contract.Source: §C.1 · p. 30
  • delegatecall executes another contract’s function in the caller’s context, allowing contracts to borrow code from other contracts.The executed function sees the caller’s contract variables rather than the callee’s.Source: §C.1 · p. 30
  • The appendix uses “fallback” as a model name for the unnamed function, and identifies ether as Ethereum’s cryptocurrency.A contract can have at most one fallback function.Source: §C.1 · p. 30

C.2 Examples of Common Solidity Vulnerabilities

The appendix illustrates common Solidity vulnerabilities and describes how VeriSolid checks contract behavior using BIP and nuXmv. Its examples connect vulnerability types to properties that can be verified in contract models.

C.2 Examples of Common Solidity Vulnerabilities

  • Re-entrancy lets a potentially malicious callee exploit the caller’s intermediate state by invoking a function in the caller, and was exploited in the DAO attack.The paper says VeriSolid’s model prevents re-entrancy.Source: Re-Entrancy · p. 31
  • A recipient can block a function that sends ether or makes a high-level call by throwing an exception; VeriSolid can detect this denial-of-service pattern with liveness properties.The paper demonstrates this for “King of Ether 2.”Source: Re-Entrancy · p. 31
  • A deadlock can make contract currency practically inaccessible, and VeriSolid checks deadlock-freedom without requiring a developer-specified property.The passage compares this outcome to the Parity multisignature wallet contracts.Source: Deadlocks · p. 31

C.3 Modeling and Verification with BIP and nuXmv

  • Formal verification covers all execution paths for all possible inputs, unlike simulation and testing, which depend on selected test inputs and control-flow coverage.The passage presents model checking as a rigorous way to assess whether a system model meets specified properties.Source: §C.3 · pp. 31–32
  • VeriSolid checks deadlock-freedom through BIP state-space exploration and checks safety and liveness properties by translating BIP models to NuSMV for CTL verification.A violated property yields a counterexample transition sequence to help locate the error in the input model.Source: §C.3 · p. 32

D Augmentation Algorithms and Equivalence Proof

The augmentation algorithms convert contract actions into transition-system structures that can be verified while preserving the behavior represented by the input model. They account for Solidity control flow and possible reverts.

D.1 Conformance Transformation

  • The conformance transformation adds a self-loop for the fallback action at every state and a new initial state that executes the constructor action before entering the original initial state.This represents a fallback function callable in any state and the contract’s initial action.Source: §D.1 · p. 32

D.2 Augmentation Transformation

  • AugmentStatement translates variable, event, and expression statements directly, while returns transition to the designated return state.The algorithm takes a statement, origin, destination, and return state as input.Source: §D.2 · pp. 33–34
  • Compound, selection, and loop statements are expanded into new states and guarded transitions representing their sequential execution and branches.For loops model initialization, condition evaluation, and body execution; while loops need no initialization or afterthought stage.Source: §D.2 · pp. 33–34
  • AugmentModel replaces each transition with an expanded form and adds a revert branch when its action may raise an exception.The algorithm reduces actions to variable declarations, expressions, and returns, while representing transition reversion explicitly.Source: §D.2 · pp. 33, 35

D.3 Observational Equivalence Proof

The proof relates states in the smart-contract model to corresponding states and intermediate paths in its augmented system. The code-generation sections describe how VeriSolid turns transition-system models into Solidity and present a Blind Auction model and generated code.

D.3 Observational Equivalence Proof

  • The proof establishes relation R between a model state and its corresponding augmented-system state, as well as the intermediate states along execution paths.The final states of normally completed transitions are related to their corresponding next states.Source: §D.3 · p. 36
  • The proof checks the relation across normally completed and reverted transitions and the augmented-system states reachable between them.It uses three properties to establish the relation for the corresponding and reachable states.Source: §D.3 · pp. 36–37

E Solidity Code Generation

  • The code generator takes a developer-defined transition system as input and generates Solidity according to the model’s operational semantics.The input includes the contract name and whether each transition should be payable.Source: E Solidity Code Generation · p. 37
  • Generated code uses an InTransition state during non-empty transition actions and derives the constructor and fallback function from the model’s initial and fallback actions.FSolidM code-generator plugins are not supported to maintain functional equivalence between the model and generated code.Source: E Solidity Code Generation · p. 37

F.1 Complete Augmented Model; F.2 Solidity Code

  • The complete augmented model of the Blind Auction contract is presented before its generated Solidity code.The code listing includes the contract’s states and transition functions, including bid, close, reveal, and finish.Source: §F.1 · p. 40, Figure 9 · p. 40, §F.2 · pp. 40–41

G.1 DAO Model

The DAO model represents a crowdfunding contract, and verification of its safety property rules out two attacks described in.

G.1 DAO Model

  • The simplified DAO contract lets participants donate ether to fund contracts, which can then withdraw funds.The contract model is shown in Figure 10.Source: §G.1 · p. 43, Figure 10 · p. 43
  • Verification of the safety property guarantees that neither of the two attacks in succeeds against the modeled contract.The modeled withdrawal changes state before the next transition, preventing an attacker from making another function call between sending ether and decreasing credit.Source: §G.1 · p. 43, Figure 10 · p. 43

G.2 The King Of the Ether Throne Models

The paper models two King of the Ether Throne contracts and reports that both have a denial-of-service vulnerability detectable through liveness-property model checking.

G.2 The King Of the Ether Throne Models

  • Figures 11 and 12 present models of the two contract versions.Figure 11 is captioned “King of Ether 1.”Source: §G.2 · p. 44, Figure 11 · p. 44
  • Both King of the Ether Throne versions have a denial-of-service vulnerability: a new king whose fallback throws can prevent anyone else from claiming the crown.The first version uses call, which returns false, while the second uses transfer, which reverts.Source: §G.2 · p. 44
  • The vulnerability was detected by model checking the liveness properties presented in Table 1.Source: §G.2 · p. 44

G.3 Resource Allocation Contract

The Resource Allocation case study’s safety properties reveal a bug in the finalize action. The related-work discussion covers smart-contract design, verification, vulnerability discovery, and operational semantics.

G.3 Resource Allocation Contract

  • TRANSAX relies on external solvers to submit energy-offer matches, which the contract checks.Source: §G.3 · p. 44
  • The finalize action contains a bug that violates the first safety property reported for the Resource Allocation contract.The misplaced offers.length = 0 operation is identified in the action code.Source: §G.3 · p. 45

H Extended Related Work

  • VeriSolid supports high-level property specification and verification results and counterexamples, and can check desired security properties rather than only known vulnerability types.Source: Verification and Vulnerability Discovery · p. 46
  • VeriSolid builds on Jiao et al.’s small-step Solidity semantics and extends statement semantics to support exceptions and return values [26].Source: Formal Operational Semantics · p. 48
  • Bartoletti and Pompianu identify nine Ethereum contract design patterns, with authorization present in 61% of studied contracts.Wöhrer and Zdun describe a taxonomy of 18 patterns.Source: Design Patterns and Development · p. 48
  • Simplicity is a typed, combinator-based smart-contract language that is not Turing complete; proposed translations from human-readable contracts lack formal guarantees for generated code.Source: Design Patterns and Development · p. 48
Loading 1901.01292v2…