面向交互智能合约运行的正确性判定

doi:10.3969/j.issn.0255-8297.2025.02.001

Abstract

Abstract: 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.

Key words: blockchain, interactive smart contract, correctness determination, code generation

CLC Number:

TP309

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.

References

[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.

Correctness Verification for Interactive Smart Contracts at Runtime

PDF

Knowledge

Abstract

Cite this article

share this article

References

Related Articles 15

Recommended Articles

Metrics

Comments

[1]	FEI Jiajia, ZHAO Xiangfu, CHEN Xiaohan, ZHANG Dengji. Smart Contract Vulnerability Analysis and Improvement Based on Smartcheck [J]. Journal of Applied Sciences, 2024, 42(6): 1027-1039.
[2]	SHI Zhigang, HUANG Jianhua, LI Tianqi. A Blockchain Scheme for Vehicular Internet of Things [J]. Journal of Applied Sciences, 2024, 42(4): 549-568.
[3]	LIU Shaojie, ZHAO Hongbo, LIU Han. Trusted Blockchain Automation Protocol Based on Domain Programming Model [J]. Journal of Applied Sciences, 2024, 42(4): 569-584.
[4]	WU Meng, QI Yong. Auditable and Traceable Blockchain Privacy Protection Model under Zero-Knowledge Proof [J]. Journal of Applied Sciences, 2024, 42(4): 598-612.
[5]	XIA Xiaoliang, QIN Zhi, WAN Wunan, ZHANG Shibin, ZHANG Jinquan. Medical Data Classification Encryption Sharing Scheme Based on Blockchain [J]. Journal of Applied Sciences, 2024, 42(4): 613-628.
[6]	LEI Ming, LIN Yijing, GAO Zhipeng. Value-Driven Ethereum Transaction Tracing Rank Method [J]. Journal of Applied Sciences, 2024, 42(4): 629-641.
[7]	LIU Kai, WANG Jiaxin, MAO Qian'ang, CHEN Yufei, YAN Jiaqi. Dynamic Role Identification and Evolutionary Analysis of Blockchain Game Ecosystems: A Case Study of Axie Infinity [J]. Journal of Applied Sciences, 2024, 42(4): 642-658.
[8]	WANG Zexu, WEN Bin. Smart Contract Vulnerability Detection of Symbol Execution with Critical Path Pre-searching [J]. Journal of Applied Sciences, 2024, 42(2): 364-374.
[9]	WU Guangfu, YANG Zi, HUANG Baozhu. Dynamic Byzantine Fault Tolerance Algorithm Based on Reputation and Clustering [J]. Journal of Applied Sciences, 2023, 41(6): 1046-1057.
[10]	MA Xue, PAN Heng, YAO Zhongyuan, SI Xueming. Dual Authorization Sharing Scheme of Searchable Electronic Medical Data Based on Consortium Blockchain [J]. Journal of Applied Sciences, 2023, 41(5): 881-895.
[11]	LIU Hong, ZHANG Jingyu, LEI Mengting, XIAO Yunpeng. Fair and Verifiable Voting Smart Contract Based on Blockchain [J]. Journal of Applied Sciences, 2023, 41(4): 541-562.
[12]	CAO Haohao, LIU Yang, LI Xiangyang, LIU Xinlei, WANG Yaoqi, ZHANG Yuan. Food Supply Chain Traceability System Based on Multi-blockchain [J]. Journal of Applied Sciences, 2023, 41(4): 563-576.
[13]	WANG Weiyuan, BI Yuanwei, CHEN Xiaohan, LI Chuanbiao. A PBFT Consensus Algorithm for Consortium Chain Optimization [J]. Journal of Applied Sciences, 2023, 41(4): 577-589.
[14]	PAN Liang, CHEN Bin, DAI Mingjun, WANG Taotao, ZHANG Shengli. Dynamic Spectrum Sharing Based on Blockchain Smart Contract [J]. Journal of Applied Sciences, 2023, 41(4): 590-600.
[15]	ZHANG Yong, YAO Zhongyuan, WANG Chao, GUO Shangkun, GUO Xiaohan, SI Xueming. Consortium Chain Multi-chain Collaboration Scheme for Complex Application Scenarios [J]. Journal of Applied Sciences, 2023, 41(4): 601-613.