Secure Smart Contract Generation Based on Petri Nets

Existing blockchain and smart contract development ecosystems do not support to design, develop, and verify secure smart contracts before deploying them. Recent attacks (see DAO hack [5]) on insecure smart contracts have caused a lot of financial loss—to avoid such issues in the future, we need better methods for creating secure smart contracts before deploying them in a blockchain. In this chapter, we present a method and a prototype tool to generate secure smart contracts based on Petri Nets. Our method allows to design and generate a secure smart contract template that can be deployed on a supported blockchain platform (e.g. Ethereum) with very little additional effort. One of the main advantages that our method brings into the smart contract development ecosystem is introducing a formal way to visually model, simulate, and verify business logic/workflows prior to the smart contract code generation. Modeling the smart contracts via Petri Nets helps the developers to minimize the logical errors—by verifying certain Petri Net properties such as deadlocks—during the modeling stage itself. Furthermore, our approach presents a technology-independent way to import and export the modeled use-case logic which can be translated into different smart contract language later.