Security vulnerability analysis and formal verification of smart contracts: a review

Abstract

Since the evolution of bitcoin, Blockchain technology has shown promising improvement and application prospects. However, blockchain gained momentum when Vitalik Buterin launched the Ethereum platform in July 2015. It includes smart contracts (SCs), a program to automate, enforce, and verify a set of rules for a transaction to be valid. Since some SCs handle millions of dollars, their security becomes critical. In the past, some hackers have exploited the vulnerabilities in Ethereum SCs and have caused significant losses to the community and users. However, to use blockchain to its full potential, we need SCs; otherwise, it is just a third-party free, decentralised system for transferring money. This paper focuses on the security aspect of SCs in terms of security vulnerabilities and tools developed to discover and locate these vulnerabilities. To prove the correctness of SCs, this study also focuses on formal verification techniques used to model and verify SCs.