Formal Semantic Approach to Detect Smart Contract Vulnerabilities Using KEVM
Article Sidebar
Main Article Content
Abstract
Smart contracts are self-executing programs that run on blockchain platforms. While smart contracts offer a range of benefits, such as immutability and transparency, they are not immune to vulnerabilities. Malicious actors can exploit smart contract vulnerabilities to execute unintended actions or access sensitive data[1]. One approach to mitigating smart contract vulnerabilities is formal verification. Formal verification is a method of verifying the correctness of software using mathematical techniques. It involves mathematically proving that a program conforms to a set of specifications. Formal verification can help detect and eliminate vulnerabilities in smart contracts before they are deployed on the blockchain. KEVM (K Framework-based EVM) is a framework that allows for formal verification of smart contracts on the Ethereum Virtual Machine (EVM). KEVM uses the K Framework, a formal semantics framework, to specify the behavior of the EVM. With KEVM, smart contract developers can verify the correctness of their contracts before deployment, reducing the risk of vulnerabilities. In this paper, we have studied smart contract vulnerabilities such as Over usage of Gas, Signature Replay attack, and misuse of fallback function. We have also written the formal specification for these vulnerabilities and executed it using KEVM.
Article Details
References
Atzei, Nicola, Bartoletti, Massimo, “A survey of attacks on Ethereum smart contracts”,2018.
Liu J, Liu Z, “A Survey on Security Verification of Blockchain Smart Contracts”, ACCESS.2019.2921624 , IEEE Access 2019
Atzei et al. "Smart Contract Vulnerabilities: Vulnerable Does Not Imply Exploited" , 2018
Ivica Nikolic, Aashish Kolluri et al. "Finding The Greedy, Prodigal, and Suicidal Contracts at Scale, 2018
Sun, Tianyu Yu, Wensheng, “A formal verification framework for security issues of blockchain smart contracts”, Electronics (Switzerland), 10.3390/electronics9020255, 2020
Bhargava et al. "Towards Safer Smart Contracts: A Survey of Languages and Verification Methods" by Bhargava et al.,2018
Bhattacharya P, Singh A , “A Systematic Review on Evolution of Blockchain Generations ITEE Journal A Systematic Review on Evolution of Blockchain Generations”, International Journal of Information Technology and Electrical Engineering, December 2018.
Praitheeshan, Purathani, Pan, Lei, “Security Analysis Methods on Ethereum Smart Contract Vulnerabilities: A Survey”, ArxIvID 1908.08605, 2019
Kshirsagar, P. R., Yadav, R. K., Patil, N. N., & Makarand L, M. (2022). Intrusion Detection System Attack Detection and Classification Model with Feed-Forward LSTM Gate in Conventional Dataset. Machine Learning Applications in Engineering Education and Management, 2(1), 20–29. Retrieved from http://yashikajournals.com/index.php/mlaeem/article/view/21
Everett Hildenbrandt , Manasvi Saxena, Xiaoran Zhu et al. "KEVM: A Complete Semantics of the Ethereum Virtual Machine", 2018
Atzei et al. "A Survey of Attacks on Ethereum Smart Contracts (SoK)" by Atzei et al., 2017
Ilya Grishchenko, “A Semantic Framework for the Security Analysis of Ethereum smart contracts”, 10.1007/978-3-319-89722- 6_10, 2018
Nikoli? et al. "Smart Contract Security: An Imperative for Blockchain Adoption" , 2018
Conti et al, "A Classification of Blockchain-based Attacks and Vulnerabilities" , 2018
Bhargava et al. "Smart Contract Security: Challenges and Future Directions" ,2019
Gabriel Santos, Natural Language Processing for Text Classification in Legal Documents , Machine Learning Applications Conference Proceedings, Vol 2 2022.
Bhargavan et al. ,"A Formal Verification Framework for Ethereum Virtual Machine Bytecode", 2016
Tsankov et al., "Formal Verification of Smart Contracts: Short Paper", 2018
Delmolino et al. ,"Formally Verified Smart Contracts in Ethereum", 2016
Kavaliro et al. , "Automated Verification of Smart Contracts Using K Framework", 2019
Braghin et al. , "Formal Verification of Smart Contracts withthe K Framework" ,2019
Bansal et al., "Smart Contract Verification with KEVM: A Comprehensive Study", 2019
Kalaivani, A. ., Karpagavalli, S. ., & Gulati, K. . (2023). Expert Automated System for Prediction of Multi-Type Dermatology Sicknesses Using Deep Neural Network Feature Extraction Approach. International Journal of Intelligent Systems and Applications in Engineering, 11(3s), 170–178. Retrieved from https://ijisae.org/index.php/IJISAE/article/view/2557
Levy et al., "Formal Verification of Solidity Smart Contracts with K", 2019
Arroyo et al. ,"On the Use of K for the Formal Verification of Smart Contracts" , 2020
Aurrecoechea et al. ,"KEVM-IDE: A Development Environment for Smart Contracts Based on K Semantics" ,2019 [24]. Chen et al. ,"KEVM-IELE: Toward Translation Validation from EVM to IELE", 2020.