Compared with a single smart contract, interactive smart contracts have more complex interactions such as mutual calling. However, existing smart contract detection and verification methods primarily consider the problems existing in a single smart contract, and the correctness of interactive smart contracts cannot be guaranteed. To address this limitation, this paper proposes a method for verifying the correctness of interactive smart contracts, where behavior interaction priority (BIP) modeling is built for interactive smart contract systems and Solidity deployment diagram (SDD) is introduced to describe contract interactions. By employing formal verification techniques, the proposed approach ensures the correctness of the interactive smart contracts and realizes their reconstruction. Experimental results show that the proposed method can effectively verify the correctness of interactive contract systems.
WANG Jiacheng, JIANG Jiajia, LI Dan, ZHANG Yushu
. Correctness Verification for Interactive Smart Contracts at Runtime[J]. Journal of Applied Sciences, 2025
, 43(2)
: 195
-207
.
DOI: 10.3969/j.issn.0255-8297.2025.02.001
[1] 何蒲, 于戈, 张岩峰, 等. 区块链技术与应用前瞻综述[J]. 计算机科学, 2017, 44(4): 1-7, 15. He P, Yu G, Zhang Y F, et al. Survey on blockchain technology and its application prospect [J]. Computer Science, 2017, 44(4): 1-7, 15. (in Chinese)
[2] 贺海武, 延安, 陈泽华. 基于区块链的智能合约技术与应用综述[J]. 计算机研究与发展, 2018, 55(11): 2452-2466. He H W, Yan A, Chen Z H. Survey of smart contract technology and application based on blockchain [J]. Journal of Computer Research and Development, 2018, 55(11): 2452-2466. (in Chinese)
[3] Scharfman J. Decentralized autonomous organization (DAO) fraud, hacks, and controversies [M]//The Cryptocurrency and Digital Asset Fraud Casebook, Volume II: DeFi, NFTs, DAOs, Meme Coins, and other Digital Asset Hacks. Cham: Springer Nature Switzerland AG, 2024: 65-106.
[4] Sayeed S, Marco-Gisbert H, Caira T. Smart contract: attacks and protections [J]. IEEE Access, 2020, 8: 24416-24427.
[5] Mavridou A, Laszka A, Stachtiari E, et al. VeriSolid: correct-by-design smart contracts for Ethereum [C]//23rd International Conference on Financial Cryptography and Data Security, 2019: 446-465.
[6] Tsankov P, Dan A, Drachsler-Cohen D, et al. Securify: practical security analysis of smart contracts [C]//2018 ACM SIGSAC Conference on Computer and Communications Security, 2018: 67-82.
[7] Ghaleb A, Rubin J, Pattabiraman K. AChecker: statically detecting smart contract access control vulnerabilities [C]//2023 IEEE/ACM 45th International Conference on Software Engineering (ICSE), 2023: 945-956.
[8] Zhang J, Li Y, Gao J, et al. Siguard: detecting signature-related vulnerabilities in smart contracts [C]//2023 IEEE/ACM 45th International Conference on Software Engineering: Companion Proceedings (ICSE-Companion), 2023: 31-35.
[9] Maroti M, Kecskes T, Kereskenyi R, et al. Next generation (meta) modeling: web- and cloud-based collaborative tool infrastructure [C]//Proceedings of the 8th Workshop on Multiparadigm Modeling, 2014: 41-60.
[10] Mavridou A, Laszka A. Tool demonstration: FSolidM for designing secure Ethereum smart contracts [C]//7th International Conference on Principles of Security and Trust, 2018: 270-277.
[11] Mavridou A, Laszka A. Designing secure Ethereum smart contracts: a finite state machine based approach [C]//22nd International Conference on Financial Cryptography and Data Security, 2018: 523-540.
[12] Basu A, Bensalem B, Bozga M, et al. Rigorous component-based system design using the BIP framework [J]. IEEE Software, 2011, 28(3): 41-48.
[13] Najah B S, Takoua A, Saddek B, et al. Model-driven information flow security for component-based systems [C]//Workshop on From Programs to Systems-The Systems Perspective in Computing, 2014: 1-20.
[14] Mavridou A, Stachtiari E, Bliudze S, et al. Architecture-based design: a satellite onboard software case study [C]//13th International Conference on Formal Aspects of Component Software (FACS), 2016: 260-279.
[15] Clarke E M, Emerson E A. Design and synthesis of synchronization skeletons using branching time temporal logic [C]//Symposium on 25 Years of Model Checking, 2008: 196-215.
[16] Bliudze S, Cimatti A, Jaber M, et al. Formal verification of infinite-state BIP models [C]//13th International Symposium on Automated Technology for Verification and Analysis, 2015: 326-343.
