交互智能合约相较于单一智能合约，存在相互调用等复杂的交互关系。然而，现有的智能合约检测、验证方法仅考虑单个智能合约存在的问题，无法保证交互智能合约运行的正确性。因此，本文提出一种能够对交互智能合约运行的正确性进行判定的方法，对交互智能合约系统进行行为交互优先级（behavior-interaction-priority,BIP）建模，并引入Solidity部署图（Solidity deployment diagram,SDD）描述合约之间的交互关系。该方法采用形式化的方法对交互智能合约运行的正确性进行验证，并实现了对交互合约代码的重构。实验结果表明，该方法可以实现对交互智能合约系统运行正确性的有效判定。
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.
[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.
