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

Jun Jin, Wenhao Zhan, Haisheng Li, Yi Ding and Jie Li ()
Additional contact information
Jun Jin: School of Information, Beijing Wuzi University, Beijing 101149, China
Wenhao Zhan: School of Information, Beijing Wuzi University, Beijing 101149, China
Haisheng Li: Beijing Key Laboratory of Big Data Technology for Food Safety, Beijing Technology and Business University, Beijing 100048, China
Yi Ding: School of Information, Beijing Wuzi University, Beijing 101149, China
Jie Li: School of Information, Beijing Wuzi University, Beijing 101149, China

Mathematics, 2024, vol. 12, issue 15, 1-24

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 (search for similar items in EconPapers)
JEL-codes: C (search for similar items in EconPapers)
Date: 2024
References: View complete reference list from CitEc
Citations:

Downloads: (external link)
https://www.mdpi.com/2227-7390/12/15/2431/pdf (application/pdf)
https://www.mdpi.com/2227-7390/12/15/2431/ (text/html)

Related works:
This item may be available elsewhere in EconPapers: Search for items with the same title.

Export reference: BibTeX RIS (EndNote, ProCite, RefMan) HTML/Text

Persistent link: https://EconPapers.repec.org/RePEc:gam:jmathe:v:12:y:2024:i:15:p:2431-:d:1450481

Access Statistics for this article

Mathematics is currently edited by Ms. Emma He

More articles in Mathematics from MDPI
Bibliographic data for series maintained by MDPI Indexing Manager ().