Visible to the public FSolidM Design Studio for Ethereum Smart Contracts

Visible to the public 

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!

Visible to the public 

Links

Hosted version: FSolidM design studio 
(Important! To view the design studio, you need to be logged in CPS-VO. You can create an account here.)

Disclaimer: This hosted version can be used only for non-commercial or academic purposes.

Source Code: https://github.com/anmavrid/smart-contracts

Slides:

Publications:

Contact: Anastasia Mavridou

Contributors:
 Aron Laszka (University of Houston), Abhishek Dubey (Vanderbilt University), Emmanouela Stachtiari (Aristotle University of Thessaloniki)