Blockchain smart contracts formalization: Approaches and challenges to address vulnerabilities

Blockchain as a distributed computing platform enables users to deploy pieces of software (known as smart contracts) for a wealth of next-generation decentralized applications without involving a trusted third-party. The advantages of smart contracts do, however, come at a price. As with most technologies, there are potential security threats, vulnerabilities and various other issues associated with smart contracts. Writing secure and safe smart contracts can be extremely difficult due to various business logics, as well as platform vulnerabilities and limitations. Formal methods have recently been advocated to mitigate these vulnerabilities. This paper aims to provide a first-time study on current formalization research on all smart contract-related platforms on blockchains, which is scarce in the literature. To this end, a timely and rigorous systematic review to examine the state-of-the-art research and achievements published between 2015 and July 2019 is provided. This study is based on a comprehensive review of a set of 35 research papers that have been extracted from eight major online digital databases. The results indicate that the most common formalization technique is theorem proving, which is most often used to verify security properties relating to smart contracts, while other techniques such as symbolic execution and model checking were also frequently used. These techniques were most commonly used to verify the functional correctness of smart contracts. From the language and automation point of views, there were 12 languages (domain specific/specification/general purpose) proposed or used for the formalization of smart contracts on blockchains, while 15 formal method-specific automated tools/frameworks were identified for mitigating various vulnerabilities of smart contracts. From the results of this work, we further highlight three open issues for future research in this emerging domain including: formal testing, automated verification of smart contracts, and domain specific languages (DSLs) for Ethereum. These issues suggest the need for additional, in-depth research. Our study also provides possible future research directions. (C) 2019 Elsevier Ltd. All rights reserved.