SmartScan: A Finite State Machine and CTL-Based Formal Verification Framework for Enhanced Security in Smart Contracts
Abstract
Smart contracts are self-executing programs deployed on blockchain platforms that facilitateautomated and decentralized transactions. However, once deployed, they become immutable, makingthem vulnerable to catastrophic exploits, such as reentrancy, access control misconfiguration, integeroverflow, and front-running. The need for proof and verification is urgent, as evidenced by other highprofile,capital-draining incidents, such as the DAO attack and Parity wallet vulnerabilities. Abstract:We present ContractFuzzer, a systematic fuzzer for detecting vulnerabilities in Ethereum smartcontracts. Existing tools are based on static analysis, symbolic execution, or heuristic detection, andthus typically impose high false positives, low completeness, and limited formal verification. In thispaper, we introduce SmartScan, a formal verification framework that systematically checks smartcontract security by integrating FSM modeling and CTL-based model checking in nuXmv. Ourmethodology performs automatic parsing of Solidity code, automated generation of FSM and BIPmodels, conversion to the SMV format, and verification of CTL security properties. It responds todetected violations with automated counterexample generation to assist in debugging and iterative reverification.For validation, SmartScan will be tested on 10 different types of Solidity contracts thataddress 14 critical vulnerabilities. Our experimental results show 95.4% detection accuracy, 3.2% falsepositive rate, and 2.8% false negative rate, with 100% verification coverage, and average verificationtime of 3–7 seconds for each property, outperforming state-of-the-art tools in both coverage andprecision. SmartScan: SmartScan has a wide-ranging practical utility in discovering and diagnosingvulnerabilities such as reentrancy and access control issues, which it has been applied in, such as in acase study of a DeFi Lending contract. SmartScan provides a scalable, precise, and developer-centricapproach to improve the confidence and reliability of blockchain applications by combining exhaustiveformal verification of smart contracts with automated counterexample generation.References
Singh, Amritraj; Parizi, Reza M.; Zhang, Qi; Choo, Kim-Kwang Raymond and Dehghantanha, Ali (2019). Blockchain Smart Contracts Formalization: Approaches and Challenges to Address Vulnerabilities. Computers & Security, 101654–. http://doi:10.1016/j.cose.2019.101654
Permenev, Anton; Dimitrov, Dimitar; Tsankov, Petar; Drachsler-Cohen, Dana and Vechev, Martin (2020). IEEE Symposium on Security and Privacy (SP) - VerX: Safety Verification of Smart Contracts. 1661–1677. http://doi:10.1109/SP40000.2020.00024
Liu, Jing and Liu, Zhentian (2019). A Survey on Security Verification of Blockchain Smart Contracts. IEEE Access, 1–1. http://doi:10.1109/ACCESS.2019.2921624
So, Sunbeom; Lee, Myungho; Park, Jisu; Lee, Heejo and Oh, Hakjoo (2020). IEEE Symposium on Security and Privacy (SP) - VERISMART: A Highly Precise Safety Verifier for Ethereum Smart Contracts. 1678–1694. http://doi:10.1109/SP40000.2020.00032
Gao, Zhipeng; Jiang, Lingxiao; Xia, Xin; Lo, David and Grundy, John (2020). Checking Smart Contracts with Structural Code Embedding. IEEE Transactions on Software Engineering, 1–1. http://doi:10.1109/TSE.2020.2971482
di Angelo, Monika and Salzer, Gernot (2019). IEEE International Conference on Decentralized Applications and Infrastructures (DAPPCON) - A Survey of Tools for Analyzing Ethereum Smart Contracts. 69–78. http://doi:10.1109/dappcon.2019.00018
Feist, Josselin; Grieco, Gustavo and Groce, Alex (2019). IEEE/ACM 2nd International Workshop on Emerging Trends in Software Engineering for Blockchain (WETSEB) - Slither: A Static Analysis Framework for Smart Contracts. 8–15. http://doi:10.1109/wetseb.2019.00008
Grech, Neville; Brent, Lexi; Scholz, Bernhard and Smaragdakis, Yannis (2019). IEEE/ACM 41st International Conference on Software Engineering (ICSE) - Gigahorse: Thorough, Declarative Decompilation of Smart Contracts. 1176–1186. http://doi:10.1109/ICSE.2019.00120
Zheng, Zibin; Xie, Shaoan; Dai, Hong-Ning; Chen, Weili; Chen, Xiangping; Weng, Jian and Imran, Muhammad (2019). An overview on smart contracts: Challenges, advances and platforms. Future Generation Computer Systems, S0167739X19316280–. http://doi:10.1016/j.future.2019.12.019
Zou, Weiqin; Lo, David; Kochhar, Pavneet Singh; Le, Xuan-Bach D.; Xia, Xin; Feng, Yang; Chen, Zhenyu and Xu, Baowen (2019). Smart Contract Development: Challenges and Opportunities. IEEE Transactions on Software Engineering, 1–1. http://doi:10.1109/TSE.2019.2942301
Pinna, Andrea; Ibba, Simona; Baralla, Gavina; Tonelli, Roberto and Marchesi, Michele (2019). A Massive Analysis of Ethereum Smart Contracts Empirical Study and Code Metrics. IEEE Access, 7, 78194–78213. http://doi:10.1109/ACCESS.2019.2921936
Ante, Lennart (2020). Smart Contracts on the Blockchain â A Bibliometric Analysis and Review. Telematics and Informatics, 101519–. http://doi:10.1016/j.tele.2020.101519
Kushal Babel, Philip Daian, Mahimna Kelkar and Ari Juels. (2023). Clockwork Finance: Automated Analysis of Economic Security in Smart Contracts. IEEE., pp.1-46. http://DOI:10.1109/SP46215.2023.10179346
SUMIT KUMAR RANA, ARUN KUMAR RANA, SANJEEV KUMAR RANA, VISHNU SHARMA, UMESH KUMAR LILHORE, OSAMAH IBRAHIM KHALAF AND ANTONINO GALLETTA. (2023). Decentralized Model to Protect Digital Evidence via Smart Contracts Using Layer 2 Polygon Blockchain. IEEE. 11, pp.83289 - 83300. http://DOI:10.1109/ACCESS.2023.3302771
Yamashita, Kazuhiro; Nomura, Yoshihide; Zhou, Ence; Pi, Bingfeng and Jun, Sun (2019). IEEE International Workshop on Blockchain Oriented Software Engineering (IWBOSE) - Potential Risks of Hyperledger Fabric Smart Contracts. 1–10. http://doi:10.1109/IWBOSE.2019.8666486
Kemmoe, Victor Youdom; Stone, William; Kim, Jeehyeong; Kim, Daeyoung and Son, Junggab (2020). Recent Advances in Smart Contracts: A Technical Overview and State of the Art. IEEE Access, 1–1. http://doi:10.1109/ACCESS.2020.3005020
Wang, Wei; Song, Jingjing; Xu, Guangquan; Li, Yidong; Wang, Hao and Su, Chunhua (2020). ContractWard: Automated Vulnerability Detection Models for Ethereum Smart Contracts. IEEE Transactions on Network Science and Engineering, 1–1. http://doi:10.1109/TNSE.2020.2968505
Shafaq Naheed Khan; Faiza Loukil; Chirine Ghedira-Guegan; Elhadj Benkhelifa and Anoud Bani-Hani; (2021). Blockchain smart contracts: Applications, challenges, and future trends . Peer-to-Peer Networking and Applications. http://doi:10.1007/s12083-021-01127-0
Anna Vacca; Andrea Di Sorbo; Corrado A. Visaggio and Gerardo Canfora; (2021). A systematic literature review of blockchain and smart contract development: Techniques, tools, and open challenges . Journal of Systems and Software. http://doi:10.1016/j.jss.2020.110891
Huang, Yongfeng; Bian, Yiyang; Li, Renpu; Zhao, J. Leon and Shi, Peizhong (2019). Smart Contract Security: A Software Lifecycle Perspective. IEEE Access, 7, 150184–150202. http://doi:10.1109/access.2019.2946988
S. ROUHANI and R. DETERS. (2019). Security, Performance, and Applications of Smart Contracts: A Systematic Survey. IEEE. 7, pp.50759 - 50779. http://DOI:10.1109/ACCESS.2019.2911031
Kai Peng; Meijun Li; Haojun Huang; Chen Wang; Shaohua Wan and Kim-Kwang Raymond Choo; (2021). Security Challenges and Opportunities for Smart Contracts in Internet of Things: A Survey . IEEE Internet of Things Journal. http://doi:10.1109/jiot.2021.3074544
Jiao, Jiao; Kan, Shuanglong; Lin, Shang-Wei; Sanan, David; Liu, Yang and Sun, Jun (2020). IEEE Symposium on Security and Privacy (SP) - Semantic Understanding of Smart Contracts: Executable Operational Semantics of Solidity. 1695–1712. http://doi:10.1109/SP40000.2020.00066
Hewa, Tharaka; Ylianttila, Mika and Liyanage, Madhusanka (2020). Survey on blockchain based smart contracts: Applications, opportunities and challenges. Journal of Network and Computer Applications, 102857–. http://doi:10.1016/j.jnca.2020.102857
SATPAL SINGH KUSHWAHA, SANDEEP JOSHI, DILBAG SINGH, MANJIT KAUR AND HEUNG-NO LEE. (2022). Systematic Review of Security Vulnerabilities in Ethereum Blockchain Smart Contract. IEEE. 10, pp.6605 - 6621. http://DOI:10.1109/ACCESS.2021.3140091
Desen Kirli, Benoit Couraud, Valentin Robu, Marcelo Salgado-Bravo, Sonam Norbu, Merlinda Andoni, Ioannis Antonopoulos, Matias Negrete-Pincetic, David Flynn and Aristides Kiprakis. (2022). Smart contracts in energy systems: A systematic review of fundamental approaches and implementations. Elsevier. 158, pp.1-28. https://doi.org/10.1016/j.rser.2021.112013
Hamledari, H., & Fischer, M. (2021). Construction payment automation using blockchain-enabled smart contracts and robotic reality capture technologies. Automation in Construction, 132, 103926. http://doi:10.1016/j.autcon.2021.103926
Anusha Vangala; Anil Kumar Sutrala; Ashok Kumar Das and Minho Jo; (2021). Smart Contract-Based Blockchain-Envisioned Authentication Scheme for Smart Farming . IEEE Internet of Things Journal. http://doi:10.1109/jiot.2021.3050676
Mehdi Sookhak; Mohammad Reza Jabbarpour; Nader Sohrabi Safa and F. Richard Yu; (2021). Blockchain and smart contract for access control in healthcare: A survey, issues and challenges, and open issues . Journal of Network and Computer Applications. http://doi:10.1016/j.jnca.2020.102950
Saini, Akanksha; Zhu, Qingyi; Singh, Navneet; Xiang, Yong; Gao, Longxiang and Zhang, Yushu (2020). A Smart Contract Based Access Control Framework for Cloud Smart Healthcare System. IEEE Internet of Things Journal, 1–1. http://doi:10.1109/JIOT.2020.3032997
Seven, Serkan; Yao, Gang; Soran, Ahmet; Onen, Ahmet and Muyeen, S. M. (2020). Peer-to-Peer Energy Trading in Virtual Power Plant Based on Blockchain Smart Contracts. IEEE Access, 8, 175713–175726. http://doi:10.1109/ACCESS.2020.3026180
Hu, Teng; Liu, Xiaolei; Chen, Ting; Zhang, Xiaosong; Huang, Xiaoming; Niu, Weina; Lu, Jiazhong; Zhou, Kun and Liu, Yuan (2021). Transaction-based classification and detection approach for Ethereum smart contract. Information Processing & Management, 58(2), 102462–. http://doi:10.1016/j.ipm.2020.102462
Sánchez, César; Schneider, Gerardo; Ahrendt, Wolfgang; Bartocci, Ezio; Bianculli, Domenico; Colombo, Christian; Falcone, Yliés; Francalanza, Adrian; Krstić, Srđan; Lourenço, Joa̋o M.; Nickovic, Dejan; Pace, Gordon J.; Rufino, Jose; Signoles, Julien; Traytel, Dmitriy and Weiss, Alexander (2019). A survey of challenges for runtime verification from advanced application domains (beyond software). Formal Methods in System Design. http://doi:10.1007/s10703-019-00337-w
HAIQING LIU, YAN ZHANG, SHIQIANG ZHENG AND YUANCHENG LI. (2019). Electric Vehicle Power Trading Mechanism Based on Blockchain and Smart Contract in V2G Network. IEEE. 7, pp.160546 - 160558. http://DOI:10.1109/ACCESS.2019.2951057
Li, Yinan; Yang, Wentao; He, Ping; Chen, Chang and Wang, Xiaonan (2019). Design and management of a distributed hybrid energy system through smart contract and blockchain. Applied Energy, 248, 390–405. http://doi:10.1016/j.apenergy.2019.04.132
Xiong, Wei and Xiong, Li (2019). Smart Contract Based Data Trading Mode Using Blockchain and Machine Learning. IEEE Access, 1–1. http://doi:10.1109/ACCESS.2019.2928325
Alkadi, O., Moustafa, N., Turnbull, B., & Choo, K.-K. R. (2021). A Deep Blockchain Framework-Enabled Collaborative Intrusion Detection for Protecting IoT and Cloud Networks. IEEE Internet of Things Journal, 8(12), 9463–9472. http://doi:10.1109/jiot.2020.2996590
Wang, Zeli; Jin, Hai; Dai, Weiqi; Choo, Kim-Kwang Raymond and Zou, Deqing (2021). Ethereum smart contract security research: survey and future research opportunities. Frontiers of Computer Science, 15(2), 152802–. http://doi:10.1007/s11704-020-9284-9
Lu Wang; Longqin Xu; Zhiying Zheng; Shuangyin Liu; Xiangtong Li;Liang Cao; Jingbin Li and Chuanheng Sun; (2021). Smart Contract-Based Agricultural Food Supply Chain Traceability . IEEE Access. http://doi:10.1109/access.2021.3050112
Bhaskara S. Egala; Ashok K. Pradhan; Venkataramana Badarla and Saraju P. Mohanty; (2021). Fortified-Chain: A Blockchain-Based Framework for Security and Privacy-Assured Internet of Medical Things With Effective Access Control . IEEE Internet of Things Journal. http://doi:10.1109/jiot.2021.3058946
Sowmya, G. and Sridevi, R. (2025). SmartScan: A Comprehensive Framework for Efficient and Optimized Formal Verification of Complex Blockchain Smart Contracts. Journal of Theoretical and Applied Information Technology, 103(3), pp. 814-834. Available at: https://www.jatit.org/volumes/Vol103No3/4Vol103No3.pdf
Krupp, J. and Rossow, C., 2018. teEther: Gnawing at Ethereum to Automatically Exploit Smart Contracts. Proceedings of the 27th USENIX Security Symposium, pp.1317-1333.
Luu, L., Chu, D.H., Olickel, H., Saxena, P. and Hobor, A., 2016. Making Smart Contracts Smarter. Proceedings of the 2016 ACM SIGSAC Conference on Computer and Communications Security (CCS '16), pp.254-269.
Feist, J., Grieco, G. and Groce, A., 2019. Slither: A Static Analysis Framework for Smart Contracts. Proceedings of the 2019 IEEE/ACM 2nd International Workshop on Emerging Trends in Software Engineering for Blockchain (WETSEB '19), pp.8-15.
Kalra, S., Goel, S., Dhawan, M. and Sharma, S., 2018. Zeus: Analyzing Safety of Smart Contracts. Proceedings of the 2018 Network and Distributed System Security Symposium (NDSS '18), pp.1-15.
DOI:
https://doi.org/10.31449/inf.v50i6.8593Downloads
Published
How to Cite
Issue
Section
License
Authors retain copyright in their work. By submitting to and publishing with Informatica, authors grant the publisher (Slovene Society Informatika) the non-exclusive right to publish, reproduce, and distribute the article and to identify itself as the original publisher.
All articles are published under the Creative Commons Attribution license CC BY 3.0. Under this license, others may share and adapt the work for any purpose, provided appropriate credit is given and changes (if any) are indicated.
Authors may deposit and share the submitted version, accepted manuscript, and published version, provided the original publication in Informatica is properly cited.
