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

Authors: Monika; Rajesh Bhatia

Addresses: CSE Department, Punjab Engineering College (Deemed to be University), Chandigarh, 160012, India ' CSE Department, Punjab Engineering College (Deemed to be University), Chandigarh, 160012, India

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.

Keywords: blockchain; smart contracts; security vulnerability; security analysis; formal methods; formal verification.

DOI: 10.1504/IJAACS.2025.145978

International Journal of Autonomous and Adaptive Communications Systems, 2025 Vol.18 No.2, pp.159 - 187

Received: 15 Jan 2023
Accepted: 28 Dec 2023
Published online: 01 May 2025 *

Full-text access for editors Full-text access for subscribers Purchase this article Comment on this article