Options
Model Checking of Hyperledger Fabric Smart Contracts
Publikationstyp
Conference Paper
Date Issued
2023-09
Sprache
English
Author(s)
Volume
2023-September
Citation
28th IEEE International Conference on Emerging Technologies and Factory Automation (ETFA 2023)
Contribution to Conference
Publisher DOI
Scopus ID
Publisher
Institute of Electrical and Electronics Engineers Inc.
ISBN
9798350339918
Conducting interactions between shared-purpose organizations that are not entirely trustworthy of each other without centralized oversight is an idea that emerged with the advent of private blockchains such as Hyperledger Fabric and its smart contracts. It is critical to check contracts to ensure their proper functionality, as organizations may collaborate with competitors. Due to the new architecture of Hyperledger Fabric, tools in this area are limited. To formally verify the source code of contracts, we mapped Fabric contract concepts into the Rebeca modeling language. Rebeca is an actor-based language that enables the modeling of concurrent and distributed systems and is supported by a model checking tool, Afra. We have identified vulnerabilities such as deadlock and starvation by examining the desired properties. Using the model checking approach, we could debug the code and hence benefit from speeding up the transactions, creating fewer extra blocks, requiring less storage space to store the ledger, and avoiding wasting computing resources.
Subjects
Hyperledger Fabric
Model Checking
Smart Contracts
DDC Class
004: Computer Sciences