Access Control Verification in Smart Contracts Using Colored Petri Nets
Oct 22, 2024
DOI: 10.3390/computers13110274
Published in: Computers
Publisher: MDPI
This paper presents an approach for the verification of access control in smart contracts written in the Digital Asset Modeling Language (DAML). The approach utilizes Colored Petri Nets (CPNs) and their analysis tool CPN Tools. It is a model-driven-based approach that employs a new meta-model for capturing access control requirements in DAML contracts. The approach is supported by a suite of tools that fully automates all of the steps: parsing DAML code, generating DAML model instances, transforming the DAML models into CPN models, and model checking the generated CPN models. The approach is tested using several DAML scripts involving access control extracted from different domains of blockchain applications.
Other Researches
Model-Driven Approach for Generating Smart Contracts for Access Control
Access controls are principles and policies that are deployed on a system to ensure privileged access to system resources. Role-based access controls are a type of access controls which ensure access to resources based on users' roles. There has bee...
Artificial intelligence has been identified as one of the main driving forces of innovation in state-of-the-art mobile and wireless networks. It has enabled many novel usage scenarios, relying on predictive models for increasing network management e...
Test case prioritization for model transformations
The application of model transformations is a critical component in Model-Driven Engineering (MDE). To ensure the correctness of the generated models, these model transformations need to be extensively tested. However, during the regression testing ...
A Model-Driven Approach for Solving the Software Component Allocation Problem
The underlying infrastructure paradigms behind the novel usage scenarios and services are becoming increasingly complex—from everyday life in smart cities to industrial environments. Both the number of devices involved and their heterogeneity make t...
A Framework for the Regression Testing of Model-to-Model Transformations
Background: Model transformations play a key role in Model-Driven Engineering (MDE). Testing model transformation is an important activity to ensure the quality and correctness of the generated models. However, during the evolution and maintenance o...