Overview

In recent years, blockchains have seen wide adoption. For instance, the market capitalization of Bitcoin, the leading blockchain-based cryptocurrency, has grown from 15 billion to more than 100 billion in 2017. The goal of the first generation of blockchains was only to provide cryptocurrencies and payment systems. In contrast, more recent blockchains, such as Ethereum, strive to provide distributed computing platforms. Blockchain-based distributed computing platforms enable the trusted execution of general purpose computation, implemented in the form of smart contracts, without any trusted parties. Blockchains and smart contracts are envisioned to have a variety of applications, ranging from finance to IoT asset tracking. As a result, they are embraced by an increasing number of organizations and companies, including major IT and financial firms, such as Cisco, IBM, Wells Fargo, and J.P. Morgan.

However, the development of smart contracts has proven to be extremely error prone in practice. Recently, an automated analysis of a large sample of smart contracts from the Ethereum blockchain found that more than 43% of contracts have security issues. These issues often result in security vulnerabilities, which may be exploited by cyber-criminals to steal cryptocurrencies and other digital assets. For instance, in 2016, 50 million worth of cryptocurrencies were stolen in the infamous ``The DAO'' attack, which exploited a combination of smart-contract vulnerabilities. In addition to theft, malicious attackers may also be able to cause damage by leading a smart contract into a deadlock, which prevents account holders from spending or withdrawing their own assets.

The prevalence of smart-contract vulnerabilities poses a severe problem in practice due to multiple reasons. First, smart contracts handle assets of significant financial value: at the time of writing, contracts deployed on the Ethereum blockchain together hold more than 6 billion worth of cryptocurrency. Second, it is by design impossible to fix bugs in a contract (or change its functionality in any way) once the contract has been deployed. Third, due to the "code is law'" principle , it is also by design impossible to remove a faulty or malicious transaction from the blockchain, which means that it is often impossible to recover from a security incident. Previous work focused on alleviating security issues in existing smart contracts by providing tools for verifying correctness and for identifying common vulnerabilities.

In contrast, we take a different approach by developing a framework, called FSolidM, which helps developers to create smart contracts that are secure by design. The main features of our framework are as follows:

Formal Model:
One of the key factors contributing to the prevalence of security issues is the semantic gap between the developers' assumptions about the underlying execution semantics and the actual semantics of smart contracts.
To close this semantic gap, FSolidM is based on a simple, formal, finite-state machine (FSM) based model for smart contracts. The model was designed to support Ethereum smart contracts, but it could easily be extended to other platforms.

Graphical Editor:
To further decrease the semantic gap and facilitate development, FSolidM provides an easy-to-use graphical editor that enables developers to design smart contracts as FSMs.

Code Generator:
FSolidM provides a tool for translating FSMs into Solidity, the most widely used high-level language for developing Ethereum contracts. Solidity code can be translated into Ethereum Virtual Machine bytecode, which can be deployed and executed on the platform.

Plugins:
FSolidM enables extending the functionality of FSM based smart contract using plugins.
As part of our framework, we provide a set of plugins that address common security issues and implement common design patterns.