IDEAS home Printed from https://ideas.repec.org/a/gam/jmathe/v12y2024i15p2431-d1450481.html
   My bibliography  Save this article

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

Author

Listed:
  • 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
    School of Computer Science and Engineering, Beihang University, Beijing 100191, China
    Yunnan Key Laboratory of Blockchain Application Technology, Kunming 650233, China)

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.

Suggested Citation

  • Jun Jin & Wenhao Zhan & Haisheng Li & Yi Ding & Jie Li, 2024. "A Dynamic Behavior Verification Method for Composite Smart Contracts Based on Model Checking," Mathematics, MDPI, vol. 12(15), pages 1-24, August.
    • Handle: RePEc:gam:jmathe:v:12:y:2024:i:15:p:2431-:d:1450481
    as

    Download full text from publisher

    File URL: https://www.mdpi.com/2227-7390/12/15/2431/pdf
    Download Restriction: no
    File URL: https://www.mdpi.com/2227-7390/12/15/2431/
    Download Restriction: no
    ---><---

    Corrections

    All material on this site has been provided by the respective publishers and authors. You can help correct errors and omissions. When requesting a correction, please mention this item's handle: RePEc:gam:jmathe:v:12:y:2024:i:15:p:2431-:d:1450481. See general information about how to correct material in RePEc.

    If you have authored this item and are not yet registered with RePEc, we encourage you to do it here. This allows to link your profile to this item. It also allows you to accept potential citations to this item that we are uncertain about.

    We have no bibliographic references for this item. You can help adding them by using this form .

    If you know of missing items citing this one, you can help us creating those links by adding the relevant references in the same way as above, for each refering item. If you are a registered author of this item, you may also want to check the "citations" tab in your RePEc Author Service profile, as there may be some citations waiting for confirmation.

    For technical questions regarding this item, or to correct its authors, title, abstract, bibliographic or download information, contact: MDPI Indexing Manager (email available below). General contact details of provider: https://www.mdpi.com .

    Please note that corrections may take a couple of weeks to filter through the various RePEc services.

    IDEAS is a RePEc service. RePEc uses bibliographic data supplied by the respective publishers.