FSolidM Design Studio for Ethereum Smart Contracts

Important!

Before running the studio, please make sure of the following:

• You must first be logged into CPS-VO. If you have no account, you can create one here.
• Make sure you are using one of the supported web browsers listed here

Short Description

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 smart contracts as Finite State Machines (FSM). We present a design studio for creating FSM on an easy-to-use graphical interface and for automatically generating Ethereum contracts. We have integrated in FSolidM a set of design patterns, which we implement as plugins that developers can easily add to their contracts to enhance security and functionality. Additionally, we have integrated model checkers for verifying deadlock-freedom, liveness, and safety properties.

Note: VeriSolid is an extension of FSolidM that allows connection to the NuSMV verification tool. Please check our paper and open source code for more info!