A Dynamic Behavior Verification Method for Composite Smart Contracts Based on Model Checking

【Author】 Jin, Jun; Zhan, Wenhao; Li, Haisheng; Ding, Yi; Li, Jie

【Source】MATHEMATICS

【影响因子】2.592

【Abstract】A composite smart contract can execute smart contracts that may belong to other owners or companies through external calls, bringing more security challenges to blockchain applications. Traditional static verification methods are inadequate for analyzing the dynamic execution of these contracts, resulting in misjudgment and omission issues. Therefore, this paper proposes a model checking approach based on dynamic behavior that verifies the security and business logic of composite smart contracts. Utilizing automata, the method models contracts, users, attackers, and extracts properties, focusing on six types of common security vulnerabilities. A thorough case study and experimental evaluation demonstrate the method's efficiency in identifying vulnerabilities and ensuring alignment with business requirements. The UPPAAL tool is employed for comprehensive verification, proving its effectiveness in enhancing smart contract security.

【Keywords】smart contracts; model checking; solidity; UPPAAL; formal methods; security vulnerabilities

【发表时间】2024 AUG

【收录时间】2024-08-14

【文献类型】实验仿真

【主题类别】

区块链技术-核心技术-智能合约