PaperlayerView exact revision on arXiv

Source-linked AI summary

Designing Secure Ethereum Smart Contracts: A Finite State Machine Based Approach

Anastasia Mavridou, Aron Laszka

arXiv:1711.09327v1cs.CRcs.FLcs.SE

TL;DR

Smart contracts can contain exploitable vulnerabilities despite handling valuable assets, and deployed bugs cannot be patched. FSolidM addresses this by modeling contracts as finite-state machines, providing graphical design and automatic Solidity generation, and extending contracts with plugins. The framework includes security features and design patterns, while its locking and transition-counter plugins add measurable, approximately additive computational overhead.

  • Problem

    Many deployed Ethereum smart contracts contain security issues that can enable asset theft or damage, while deployed contract bugs cannot be patched.

  • Method

    FSolidM uses a formal finite-state-machine model, graphical editor, automatic FSM-to-Solidity translation, and plugins for security features and design patterns.

  • Results

    Locking adds around 10,672 gas, transition counter 5,648 gas, and both plugins 16,319 gas; plugin overhead is approximately additive.

  • Takeaways & Limitations

    FSolidM provides a framework for creating secure smart contracts through formally modeled FSM designs, generated Solidity code, and add-on plugins.

Abstract

from arXiv · show

The adoption of blockchain-based distributed computation platforms is growing fast. Some of these platforms, such as Ethereum, provide support for implementing smart contracts, which are envisioned to have novel applications in a broad range of areas, including finance and Internet-of-Things. However, a significant number of smart contracts deployed in practice suffer from security vulnerabilities, which enable malicious users to steal assets from a contract or to cause damage. Vulnerabilities present a serious issue since contracts may handle financial assets of considerable value, and contract bugs are non-fixable by design. To help developers create more secure smart contracts, we introduce FSolidM, a framework rooted in rigorous semantics for designing con- tracts as Finite State Machines (FSM). We present a tool for creating FSM on an easy-to-use graphical interface and for automatically generating Ethereum contracts. Further, we introduce a set of design patterns, which we implement as plugins that developers can easily add to their contracts to enhance security and functionality.

1 Introduction

Ethereum enables smart contracts, but deployed contracts often contain vulnerabilities that can cause major asset losses and cannot be patched after deployment. FSolidM addresses this problem by designing contracts as formally modeled FSMs and generating Solidity code with extensible security plugins.

  • Motivation: 8,333 of 19,336 analyzed Ethereum contracts suffered at least one security issue, while attacks have stolen millions of dollars in digital assets.The DAO attack alone stole 3.6 million Ethers, worth around $50 million at the time.
  • Motivation: Deployed smart-contract bugs are especially serious because contracts may hold significant assets and their functionality cannot be altered after deployment.Faulty or malicious transactions also cannot be removed from the blockchain.
  • FSolidM framework: FSolidM introduces a formal finite-state-machine model for smart contracts, primarily targeting Ethereum while allowing possible application to other platforms.The model represents contracts as states and transitions with rigorous semantics.
  • FSolidM framework: An easy-to-use graphical editor enables developers to design smart contracts as FSMs, and a tool translates the resulting FSMs into Solidity code.The graphical editor specifies states, transitions, and guards, while Solidity functions implement FSM transitions.
  • Extensions and benefits: FSolidM plugins add security features and design patterns, while rigorous semantics support formal-analysis integration and reduce error-prone manual coding.The tool is open-source and available online.

2 Related Work

Prior work catalogs Ethereum vulnerabilities and develops verification or detection tools, while FSolidM focuses on creating contracts securely through a formal FSM-based workflow. Related studies also document the prevalence of common design patterns and trust dependencies.

  • Vulnerabilities and patterns: Prior studies provide taxonomies of Ethereum smart-contract vulnerabilities and design patterns, which FSolidM addresses through framework plugins.The paper focuses on two common vulnerability types and implements selected patterns and security features.
  • Common vulnerabilities: Reentrancy permits a malicious callee to exploit an intermediate caller state by invoking a function in the caller contract.The DAO attack is identified as an example involving this vulnerability.
  • Common vulnerabilities: Transaction-ordering dependence leaves users uncertain about the contract state when their calls execute because multiple invocations may be processed in unpredictable order.The paper notes that preventing this issue is difficult when users invoke functions concurrently.
  • Vulnerabilities and patterns: Authorization and time constraint are the two most common surveyed design patterns, used in 61% and 33% of Ethereum contracts, respectively.The study measured pattern prevalence across contracts in practice.
  • Verification and discovery: Existing approaches verify selected properties, formalize the Ethereum Virtual Machine, translate contracts into F*, or detect vulnerable patterns with tools such as Oyente.Some approaches require substantial manual analysis or changes to Ethereum execution semantics.
  • Trust and immutability: A study of all contracts deployed on Ethereum found that two out of five require trust in at least one third party under a control-flow-immutability heuristic.This indicator quantifies the prevalence of contractual loopholes associated with modifying contract control flow.

3 Defining Smart Contracts as FSMs

FSolidM models Ethereum smart contracts as finite state machines whose guarded transitions execute actions and change contract state. A blind auction illustrates this model through four states for bidding, revealing, completion, and cancellation.

  • Blind-auction example: The blind auction has four states: AcceptingBlindedBids, RevealingBids, Finished, and Canceled.Bidders submit hashed bids and deposits, reveal bids, withdraw eligible funds, or retract bids after cancellation.
  • Blind-auction example: In the auction FSM, ABB is initial; bid, reveal, close, finish, cancel, unbid, and withdraw transitions govern the auction lifecycle.The close transition can move the auction from ABB to RB when now >= creationTime + 5 days.
  • FSM model: The model separates contract, input, and output variables, with guards based on contract and input data and actions using Solidity statements.These variable classes represent stored data, transition inputs, and returned transition outputs.
  • FSM model: A smart contract is modeled as a finite set of states, an initial state, variables, and guarded transitions between states.Transitions execute ordered action sets when their guard conditions are satisfied.

4 FSM-to-Solidity Transformation

FSolidM transforms a graphical FSM specification into Solidity by mapping states, variables, guards, actions, inputs, outputs, and transitions to contract code. The transformation also supports developer-specified transition properties and plugins.

  • Transformation overview: Developers provide an FSM graph, and FSolidM generates a Solidity contract whose transition functions encode guards, actions, inputs, outputs, and state changes.The generated code is based on a formal transformation and can be extended with plugins.
  • Transformation input: The transformation input includes the FSM name, states, initial state, contract variables with visibility, transitions, and custom types.Each transition specifies its name, guards, inputs, statements, outputs, source and destination states, and tags.
  • Generated state representation: States are generated as a Solidity enum, with the contract state initialized to the FSM's initial state.For the blind auction, the generated declaration contains ABB, RB, F, and C, initialized to ABB.
  • Generated transitions: The blind-auction variables are generated as Solidity declarations for bids, pending returns, the highest bidder, and the highest bid.The bid function is payable and stores a blinded bid with its deposit.
  • Generated transitions: Each generated transition function checks its source state and guards, executes its statements, returns declared outputs, and updates state when source and destination differ.The bid example remains in ABB, while close checks now >= creationTime + 5 days and changes state from ABB to RB.
  • Generated transitions: The close function requires the auction to be in ABB, enforces the five-day guard, and changes the state to RB.It has no associated actions.

5 Security Extensions and Patterns

FSolidM extends its FSM-to-Solidity model with plugins for security and functionality. The extensions include locking against reentrancy, transition ordering, timed transitions, and administrator-controlled access.

  • Plugin framework: Plugins extend contracts or selected transitions without requiring developers to write the additional code manually.They are appended to the contract-level Plugins and transition-level TransitionPlugins elements.
  • Locking: The locking plugin prevents reentrancy by ensuring contract functions cannot be nested within one another.Its modifier locks before a transition, executes it, and unlocks afterward; the tool applies it before other plugins.
  • Transition counter: The transition-counter plugin addresses unpredictable state by requiring each function call to provide the next transition number in sequence.A call succeeds only when its supplied number matches the counter, which then increments by one.
  • Automatic timed transitions: Timed transitions automatically execute when their guard is satisfied at a developer-specified time measured in seconds from contract creation.The modifier checks for due timed transitions before executing the invoked transition.
  • Automatic timed transitions: Manual timed-transition modifiers can be omitted accidentally, allowing calls such as bids after an auction's time limit; the plugin automates this enforcement.Timed transitions use guards and actions without input or output data and include a transition time.
  • Access control: The access-control plugin maintains runtime administrators and can forbid non-administrators from accessing selected functions.Its management functions are restricted to one privileged group, with possible extension to finer-grained access control.

6 The FSolidM Tool

FSolidM provides graphical and code editors, model validation, automatic FSM-to-Solidity generation, and extensible plugins. Its security plugins add transition overhead that is nearly constant and additive.

  • Tool: FSolidM is built on WebGME and supports collaborative, versioned smart-contract development.Users can branch, merge, and view contract history.
  • Tool: Developers specify contract states, transitions, guards, and other inputs through graphical and Solidity editors.Generated model code is locked in the code editor, while manually specified code remains editable.
  • Tool: FSolidM checks FSM specifications, reports errors with links to erroneous model nodes, generates Solidity, and integrates plugins.The tool can detect issues such as a missing initial state.
  • Numerical Results: Security plugins increase computational cost, so the evaluation compares blind-auction transitions with locking and transition counter plugins.Design-pattern plugins are excluded because they provide functionality without the security overhead examined here.
  • Numerical Results: 10,668–10,686 gas is the locking overhead across transitions, corresponding to 54% for unbid and 16% for reveal.The experiment measures transition cost as the gas cost of a transaction invoking the transition function.
  • Numerical Results: 10,672 gas, 5,648 gas, and 16,319 gas are the increases for locking, transition counter, and both plugins, respectively.The reported overhead for the two plugins together is approximately additive.

7 Conclusion and Future Work

The paper concludes that FSolidM supports secure smart-contract creation through FSM modeling, graphical design, automatic generation, and extensible plugins. Future work expands plugins, verification, and analysis of interacting contracts.

  • 7 Conclusion and Future Work: FSolidM combines a formal FSM-based contract model, graphical editor, automatic code generator, and add-on plugins.The framework targets creating secure contracts rather than fixing deployed ones.
  • 7 Conclusion and Future Work: Locking and transition counter plugins address reentrancy and unpredictable-state vulnerabilities, while timed-transition and access-control plugins support common design patterns.The design-pattern plugins target contracts with complex functionality.
  • 7 Conclusion and Future Work: Planned extensions include security plugins for Solidity-addressable vulnerability types and plugins implementing popular design patterns.These extensions are intended to broaden the framework’s plugin coverage.
  • 7 Conclusion and Future Work: Future work will integrate verification tools and correctness-by-design techniques to verify contract security and safety properties.The paper gives deadlock reachability as an example verification question.
  • 7 Conclusion and Future Work: The framework will support modeling and verifying multiple interacting contracts as interacting FSMs.Joint verification can expose deadlocks that do not occur in individual contracts considered separately.

A Implementation of the Access Control Plugin

The access-control plugin restricts developer-tagged transitions and administrative operations to authorized administrators.

  • Implementation: The access-control plugin is introduced as an extension to the FSolidM contract model.Its implementation is described in the paper’s access-control section.
  • Implementation: When enabled, the plugin requires the caller to satisfy isAdmin[msg.sender] before executing protected code.The access check is implemented through a Solidity modifier.
  • Implementation: Administrators can add an address only when it is not already an administrator.The addAdmin function itself is restricted by onlyAdmin.
  • Implementation: Administrators can remove administrators through the onlyAdmin-protected removeAdmin function.The passage identifies removeAdmin as an administrative operation.
  • Implementation: Transitions tagged “only admin” by the developer receive the access-control restriction.The plugin applies to transitions whose tags contain admin.

B Event Plugin

The event plugin emits Solidity events after tagged transitions execute, allowing Ethereum clients to receive execution notifications. The section also presents generated blind-auction code using locking and transition-counting protections.

  • Event Plugin: The event plugin uses Solidity events to notify Ethereum clients when tagged transitions execute.Clients can listen to Ethereum logging facilities for these events.
  • Event Plugin: The plugin adds event behavior to transitions carrying the event tag.The implementation refers to the set of transitions tagged event.
  • Generated Blind Auction: The generated blind-auction contract applies locking and transition-counter plugins to its transitions.The listed implementation includes these plugins in the generated code.
  • Generated Blind Auction: The blind auction begins in AcceptingBlindedBids, proceeds through RevealingBids, and can finish or be canceled according to its modeled transitions.The contract defines states ABB, RB, F, and C, with guards controlling state changes.
  • Generated Blind Auction: The reveal transition checks bid hashes and deposits before updating the highest bid and bidder.It iterates over submitted values and secrets and requires equal input lengths.
  • Generated Blind Auction: Finish and cancellation transitions require appropriate states and, for finishing, the auction’s time condition.The finish transition requires at least ten days from creation, while cancellation depends on the current auction state.
  • Generated Blind Auction: Withdraw and unbid return pending deposits under conditions determined by the winner and the auction state.The winner withdraws only the difference between deposit and bid, while canceled bids can be fully withdrawn.

D Numerical Results on Computational Cost – Table

Table 2 reports the computational cost of transitions under four combinations of the locking and transition counter plugins. The results are discussed in Section 6.1.

  • Table 2 lists the gas cost of each transition for all four combinations of the locking and transition counter plugins.
  • The table provides the computational-cost results for evaluating plugin overhead on contract transitions.
  • FSolidM is open-source and available online.

E.1 FSolidM Metamodel

The FSolidM metamodel represents contract behavior with finite state machines and supports versioned model changes, code generation, and security-pattern application through graphical services.

  • FSolidM Metamodel: The FSolidM metamodel is represented as a UML class diagram whose Contract behavior is described by an FSM.
  • FSolidM Metamodel: Each contract has exactly one InitialState, while State Base may be instantiated as either an InitialState or a State.
  • Versioning: FSolidM versions committed changes, enabling branching, merging, and viewing a contract’s history.
  • The SolidityCodeGenerator and AddSecurityPatterns mechanisms: Developers invoke Solidity code generation or security extensions and patterns through services in the graphical tool.
  • The SolidityCodeGenerator and AddSecurityPatterns mechanisms: Successful generation provides downloadable Solidity artifacts, while incorrect input produces detailed explanatory error messages.
Loading 1711.09327v1…