Smart Contract Design Meets State Machine Synthesis: Case Studies

TL;DR

This paper explores the use of finite state machine synthesis from formal specifications to automatically generate correct smart contracts, demonstrated through case studies like crowdfunding and auctions.

Contribution

It introduces a method for synthesizing smart contracts as FSMs from LTL specifications, enabling correct-by-construction code generation for blockchain applications.

Findings

FSM synthesis successfully generated smart contracts from LTL specifications.

Generated contracts were directly translatable into executable Solidity code.

Case studies demonstrated practical applicability of the approach.

Abstract

Modern blockchain systems support creation of smart contracts -- stateful programs hosted and executed on a blockchain. Smart contracts hold and transfer significant amounts of digital currency which makes them an attractive target for security attacks. It has been shown that many contracts deployed to public ledgers contain security vulnerabilities. Moreover, the design of blockchain systems does not allow the code of the smart contract to be changed after it has been deployed to the system. Therefore, it is important to guarantee the correctness of smart contracts prior to their deployment. Formal verification is widely used to check smart contracts for correctness with respect to given specification. In this work we consider program synthesis techniques in which the specification is used to generate correct-by-construction programs. We focus on one of the special cases of program synthesis where programs are modeled with finite state machines (FSMs). We show how FSM synthesis can be applied to the problem of automatic smart contract generation. Several case studies of smart contracts are outlined: crowdfunding platform, blinded auction and a license contract. For each case study we specify the corresponding smart contract with a set of formulas in linear temporal logic (LTL) and use this specification together with test scenarios to synthesize a FSM model for that contract. These models are later used to generate executable Solidity code which can be directly used in a blockchain system.