Blockchain has received attention for its potential use in business. Bitcoin is powered by blockchain, and interest in it has surged in the past few years. It has many uses that need to be modeled. Modeling is used in many walks of life to share ideas, reduce complexity, achieve close alignment of one person viewpoint with another and provide abstractions of a system at some level of precision and detail. Software modeling is used in Model Driven Engineering (MDE), and Domain Specific Languages (DSLs) ease model development and provide intuitive syntax for domain experts. The present study has designed and evaluated a meta-model for the bitcoin application domain to facilitate application development and help in truly understanding bitcoin. The proposed meta-model, including stereotypes, tagged values, enumerations and a set of constraints defined by Object Constraint Language (OCL), was defined as a Unified Modeling Language (UML) profile and was implemented in the Sparx Enterprise Architect (Sparx EA) modeling tool. A case study developed by our meta-model is also presented.
In a distributed peer-to-peer network, blockchain technology enables the secure transmission of digital assets.This is done based on intellectual agreement capabilities.Indeed, blockchain world has developed into a tool for managing transversal processes on an unbiased platform.Process mining has evolved as a well-known toolkit for comprehending different organization processes.Recently, researchers developed strategies for resolving the issue of collecting reliable data gathered from blockchains in order to improve the examination of blockchain applications employing process mining.There is yet to be a clear assessment of the utility of process mining on public blockchain event logs.In this paper, we will validate the applicability of process mining on public blockchain event logs by treating ChickenHunt data set.ChickenHunt is a competitive game that is operated as a Decentralized application on Ethereum blockchain network.
We introduce the notion of \emph{traceable mixnets}. In a traditional mixnet, multiple mix-servers jointly permute and decrypt a list of ciphertexts to produce a list of plaintexts, along with a proof of correctness, such that the association between individual ciphertexts and plaintexts remains completely hidden. However, in many applications, the privacy-utility tradeoff requires answering some specific queries about this association, without revealing any information beyond the query result. We consider queries of the following types: a) given a ciphertext in the mixnet input list, whether it encrypts one of a given subset of plaintexts in the output list, and b) given a plaintext in the mixnet output list, whether it is a decryption of one of a given subset of ciphertexts in the input list. Traceable mixnets allow the mix-servers to jointly prove answers to the above queries to a querier such that neither the querier nor a threshold number of mix-servers learn any information beyond the query result. Further, if the querier is not corrupted, the corrupted mix-servers do not even learn the query result. We first comprehensively formalise these security properties of traceable mixnets and then propose a construction of traceable mixnets using novel distributed zero-knowledge proofs (ZKPs) of set membership and of a statement we call reverse set membership. Although set membership has been studied in the single-prover setting, the main challenge in our distributed setting lies in making sure that none of the mix-servers learn the association between ciphertexts and plaintexts during the proof. We implement our distributed ZKPs and show that they are faster than state-of-the-art by at least one order of magnitude.
Mojtaba Eshghie, Cyrille Artho, Hans Stammler, Wolfgang Ahrendt · 6 authors
Logical flaws in smart contracts are often exploited, leading to significant financial losses. Our tool, HighGuard, detects transactions that violate business logic specifications of smart contracts. HighGuard employs dynamic condition response (DCR) graph models as formal specifications to verify contract execution against these models. It is capable of operating in a cross-chain environment for detecting business logic flaws across different blockchain platforms. We demonstrate HighGuard's effectiveness in identifying deviations from specified behaviors in smart contracts without requiring code instrumentation or incurring additional gas costs. By using precise specifications in the monitor, HighGuard achieves detection without false positives. Our evaluation, involving 54 exploits, confirms HighGuard's effectiveness in detecting business logic vulnerabilities. Our open-source implementation of HighGuard and a screencast of its usage are available at: https://github.com/mojtaba-eshghie/HighGuard https://www.youtube.com/watch?v=sZYVV-slDaY
Tianhong Xiong, Shangqing Feng, Maolin Pan, Yang Yu
Summary Currently, inter‐organizational process collaboration (IOPC) has been widely used in the design and development of distributed systems that support business process execution. Blockchain‐based IOPC can establish trusted data sharing among participants, attracting more and more attention. The core of such study is to translate the graphical model (e.g., BPMN) into program code called smart contract that can be executed in the blockchain environment. In this context, a proper smart contract plays a vital role in the correct implementation of block‐chain‐based IOPC. In fact, the quality of graphical model affects the smart contract generation. Problematic models (e.g., deadlock) will result in incorrect contracts (causing unexpected behaviors). To avoid this undesired implementation, this article explores to generate smart contracts by using the verified formal model as input instead of graphical model. Specifically, we introduce a prototype framework that supports the automatic generation of smart contracts, providing an end‐to‐end solution from modeling, verification, translation to implementation. One of the cores of this framework is to provide a CSP#‐based formalization for the BPMN collaboration model from the perspective of message interaction. This formalization provides precise execution semantics and model verification for graphical models, and a verified formal model for smart contract generation. Another novelty is that it introduces a syntax tree‐based translation algorithm to directly map the formal model into a smart contract. The required formalism, verification, and translation techniques are transparent to users without imposing additional burdens. Finally, a set of experiments shows the effectiveness of the framework.
We are currently witnessing the proliferation of blockchain environments to support a wide spectrum of corporate applications through the use of smart contracts. It is of no surprise that smart contract programming language technology constantly evolves to include not only specialized languages such as Solidity, but also general purpose languages such as GoLang and JavaScript. Furthermore, blockchain technology imposes unique challenges related to the monetary cost of deploying smart contracts, and handling roll-back issues when a smart contract fails. It is therefore evident that the complexity of systems involving smart contracts will only increase over time thus making the maintenance and evolution of such systems a very challenging task. One solution to these problems is to approach the implementation and deployment of such systems in a disciplined and automated way. In this paper, we propose a model-driven approach where the structure and inter-dependencies of smart contract, as well as stakeholder objectives, are denoted by extended goal models which can then be transformed to yield Solidity code that conforms with those models. More specifically, we present first a Domain Specific Language (DSL) to denote extended goal models and second, a transformation process which allows for the Abstract Syntax Trees of such a DSL program to be transformed into Solidity smart contact source code. The transformation process ensures that the generated smart contract skeleton code yields a system that is conformant with the model, which serves as a specification of said system so that subsequent analysis, understanding, and maintenance will be easier to achieve.
Business process collaboration between independent parties is challenging when participants do not completely trust each other. Tracking actions and enforcing the activity authorizations of participants via blockchain-hosted smart contracts is an emerging solution to this lack of trust, with most state-of-the-art approaches generating the orchestrating smart contract logic from Business Process Model and Notation (BPMN) models. However, compared to centralized business process orchestration services, smart contract state typically leaks potentially sensitive information about the state of the collaboration, limiting the applicability of decentralized process orchestration. This paper presents a novel, collaboration confidentiality-preserving approach where the process orchestrator smart contract only stores encrypted and hashed process states and validates participant actions against a BPMN model using zero-knowledge proofs. We cover a subset of BPMN, which is sufficient from the practical point of view, support messagepassing between participants, and provide an open-source, endto-end prototype implementation that automatically generates the key software artifacts.
Mojtaba Eshghie, Wolfgang Ahrendt, Cyrille Artho, Thomas Hildebrandt · 5 authors
Smart contracts manage blockchain assets and embody business processes. However, mainstream smart contract programming languages such as Solidity lack explicit notions of roles, action dependencies, and time. Instead, these concepts are implemented in program code. This makes it very hard to design and analyze smart contracts. We argue that DCR graphs are a suitable formalization tool for smart contracts because they explicitly and visually capture the mentioned features. We utilize this expressiveness to show that many common high-level design patterns representing the underlying business processes in smart contract applications can be naturally modeled this way. Applying these patterns shows that DCR graphs facilitate the development and analysis of correct and reliable smart contracts by providing a clear and easy-to-understand specification.
NFTs are a groundbreaking application of blockchain technology that allows for the ownership and trading of unique digital assets. From artwork and collectibles to virtual real estate and gaming items, NFTs have taken the world by storm, capturing the attention of enthusiasts and investors alike.
This paper presents a preliminary exploration of the design and deployment of solidarity primitives for web3 social security, based on the insights generated during Other Internet’s Web3 Work Forum held in July 2023. The paper proposes a modular framework to develop solidarity primitives addressing the three dimensions of security for DAO contributors: psychosocial stability, financial stability and regulatory clarity. Additionally, it outlines a range of both on-chain and off-chain mechanisms and improvement proposals specific to each dimension. Lastly, it discusses current challenges to implementation.
The Blockchain 2.0 era integrated with smart contract along with its platforms and applications have experienced explosive growth in recent years. However, many smart contracts deployed in practice are prone to errors and cannot be modified due to the immutability of the blockchain. In light of this, it is vital to ensure the security of correctness of smart contracts before deployment. This paper proposes a formal modeling method based on Timed Colored Petri net (TCPN) to anlyze smart contracts with time constrains. We apply this formalism to a concrete voting contract system. Its functional requirements are formalized by the improved computing timing logic ASK-CTL with ML (Meta Language). Simulation and experiment show that the security and reliability of the voting contract can be effectively guaranteed.
Research on blockchains addresses multiple issues, with one being the automated creation of smart contracts. Developing smart contract methods is more difficult than mainstream software development as the underlying blockchain infrastructure poses additional complexity. We report on a new approach to developing smart contracts with the objective of automating the process to increase developer efficiency and reduce the risk of errors introduced by software developers. To support industry adoption, we use Business Process Model and Notation (BPMN) modeling to describe an application while targeting applications in the trade vertical. We describe a system that transforms a BPMN model into a multi-modal model that combines Discrete Event (DE) modeling for concurrency with Hierarchical State Machines (HSMs) to represent application functionality. Then, further transformations are used to transform the DE-HSM model into methods in smart contracts. The system lets the modeler decide which of the independent patterns should be transformed into methods of a separate smart contract that is deployed on a sidechain for the purpose of (i) reducing processing costs and/or (ii) providing privacy so that other participants in the smart contract do not have visibility into the processing of the pattern. We also briefly describe a proof-of-concept tool we built to demonstrate the feasibility of our approach.
Abstract Business Processes (BPs) are commonly used by organizations to describe their goals. However, the existent decentralization found in many organizations forces them to build such BPs by coordinating distributed and fragmented BPs. Within this context, microservices arise as a very interesting and convenient way to address the implementation of such processes due to their low coupling characteristic. In this case, the coordination of such fragmented BPs is usually achieved by means of event-based choreographies. One of the main challenges to be faced by choreographies is their evolution due to the complexity that introduces the need of integrating changes among autonomous and independent partners. We face the challenge of evolving a microservice composition that is globally defined in a BPMN model but executed through a choreography of BPMN fragments. We introduce a protocol to manage the propagation of a change done by one microservice to be integrated into both the BPMN fragments of the rest of the microservices and the global BPMN model. This protocol also supports the negotiation among participants and the automatic suggestion of model adaptations to maintain the functional integrity of the composition. These suggestions are supported by a catalogue of adaptation rules that precisely characterize every possible change and propose actions to be considered by the affected microservices. All the evolution process is done at the modelling level, without managing hard-coded implementations. We have developed specific tools to facilitate the practical adoption of this protocol, and we have validated our work in an experiment with users. We can conclude that the proposed approach is effective to evolve microservice compositions implemented as event-based choreography of BPMN fragments from the local perspective of one partner.
Luciano Baresi, Giovanni Quattrocchi, Damian A. Tamburri, Luca Terracciano
The deployment and management of Blockchain applications require non-trivial efforts given the unique characteristics of their infrastructure (i.e., immutability) and the complexity of the software systems being executed. The operation of Blockchain applications is still based on ad-hoc solutions that are error-prone, difficult to maintain and evolve, and do not manage their interactions with other infrastructures (e.g., a Cloud backend). This paper proposes KATENA, a framework for the deployment and management of Blockchain applications. In particular, it focuses on applications that are compatible with Ethereum, a popular general-purpose Blockchain technology. KATENA provides i) a metamodel for defining Blockchain applications, ii) a set of processes to automate the deployment and management of defined models, and iii) an implementation of the approach based on TOSCA, a standard language for Infrastructure-as-Code, and xOpera, a TOSCA-compatible orchestrator. To evaluate the approach, we applied KATENA to model and deploy three real-world Blockchain applications, and showed that our solution reduces the amount of code required for their operations up to $82.7\%$.
Norine Coenen, Bernd Finkbeiner, Jana Hofmann, Julia Tillman
Smart contracts are small but highly security-critical programs that implement wallets, token systems, auctions, crowd funding systems, elections, and other multi-party transactions on the blockchain. A broad range of methods has been developed to ensure that a smart contract is functionally correct. However, smart contracts often additionally need to satisfy certain hyperproperties, such as symmetry, determinism, or an information flow policy. In this paper, we show how a synthesis method for smart contracts can ensure that the contract satisfies its desired hyperproperties. We build on top of a recently developed synthesis approach from specifications in the temporal logic TSL. We present HyperTSL, an extension of TSL for the specification of hyperproperties of infinite-state software. As a preprocessing step, we show how to detect if a hyperproperty has an equivalent formulation as a (simpler) trace property. Finally, we describe how to refine a synthesized contract to adhere to its HyperTSL specification.
The formal description and verification of networks of cooperative and interacting agents is made difficult by the interplay of several different behavioral patterns, models of communication, scalability issues. In this paper, we will explore the functionalities and the expressiveness of a general-purpose process algebraic framework for the specification and model checking based analysis of collective and cooperative systems. The proposed syntactic and semantic schemes are general enough to be adapted with small modifications to heterogeneous application domains, like, e.g., crowdsourcing systems, trustworthy networks, and distributed ledger technologies.
Bernd Finkbeiner, Jana Hofmann, Florian Kohn, Noemi Passing
Smart contracts are small but highly error-prone programs that implement agreements between multiple parties. We present a reactive synthesis approach for the automatic construction of smart contract state machines. Towards this end, we extend temporal stream logic (TSL) with universally quantified parameters over infinite domains. Parameterized TSL is a convenient logic to specify the temporal control flow, i.e., the correct order of transactions, as well as the data flow of the contract's fields. We develop a two-step approach that 1) synthesizes a finite representation of the - in general - infinite-state system and 2) splits the system into a compact hierarchical architecture that enables the implementation of the state machine in Solidity. We implement the approach in our prototype tool SCSynt, which - within seconds - automatically constructs Solidity code that realizes the specified control flow.
Sebastian Müller, Andreas Penzkofer, Nikita Polyanskii, Jonas Theis · 6 authors
The Unspent Transaction Output (UTXO) model is commonly used in the field of Distributed Ledger Technology (DLT) to transfer value between participants. One of its advantages is that it allows parallel processing of transactions, as independent transactions can be added in any order. This property of order invariance and parallelisability has potential benefits in terms of scalability. However, since the UTXO Ledger is an append-only data structure, this advantage is compromised through the presence of conflicting transactions. We propose an extended UTXO Ledger model that optimistically updates the ledger and keeps track of the dependencies of the possible conflicts. In the presence of a conflict resolution mechanism, we propose a method to reduce the extended ledger back to a consistent UTXO Ledger.
The Line-less Mobile Assembly System paradigm (short LMAS) provides necessitated flexibility, especially for large-scale products as customer demands for individualized products persist and product life-cycles remain short. To make LMAS advantages operationally usable in an industrial context, it requires a suitable control system to connect multi-purpose assembly resources and to autonomously configure transient assembly stations. Therefore this paper reviews the relevant literature to identify the necessary components of such architectures. Depending on the control system’s intention and use cases, the properties of the organizational paradigm, an adequate ontology and basic design patterns regarding the distribution and order-relationships of the system entities are to be defined conceptually. For the implementation, a role model, an interaction model, and a data model are required. Due to the utilization of mobile multipurpose resources and the possibility of factory shopfloor reconfiguration by transient stations, existing approaches do not meet LMAS inherent properties. Consequently, we present a suitable decentralized multi-agent control system approach.
Business process modeling and verification have become an essential way to control and assure organizational evolution. We overview the opportunities for the application of blockchain in Business Process Management and Modeling in Finance and we focus on in-depth analysis of claim process in insurance as a use case. We investigate the utilization of blockchain technology for model checking of Workflow, Business Processes to ensure consistency, integrity, and security in a dynamically changing business environment. We create a UML profile for the blockchain, then we combine it with a UML activity diagram followed by a verification using Petri nets to guarantee a distributed computing system and scalable with mutable data. Our paper creates a unified picture of the approaches towards business processes modeling used in the financial industry organized around the set of premises intending to develop a future research agenda for blockchain business process modeling, specifically for the financial industry domain.
Jan 1, 2022·Proceedings of the ... Annual Hawaii International Conference on System Sciences/Proceedings of the Annual Hawaii International Conference on System Sciences
Jan 1, 2022·Proceedings of the ... Annual Hawaii International Conference on System Sciences/Proceedings of the Annual Hawaii International Conference on System Sciences
Considerable progress was forcasted for collaborative business processes with the rise of blockchain programmable platforms. One of the saliant promises was auditable traces of business process execution, but practically that has posed challenges specially with regard to blockchain logs’ structure who turned out to be inadequate for process mining techniques. Approaches to answer this issue have started to emerge in the literature, some focusing on the creation process of event logs and others dealing with their retrieval from the blockchain. This work outlines the generic steps required to solve these challenges and analyzes findings in these approaches with a consideration for efficiency and future research directions.
Jan 1, 2022·Business Process Management: Blockchain, Robotic Process Automation, and Central and Eastern Europe Forum. BPM 2022. Lecture Notes in Business Information Processing, vol 459. Springer, Cham
Blockchain has been proposed to facilitate the enactment of interorganisational business processes. For such processes, blockchain can guarantee the enforcement of rules and the integrity of execution traces - without the need for a centralised trusted party. However, the enactment of interorganisational processes pose manifold challenges. In this work, we ask what answers the research field offers in response to those challenges. To do so, we conduct a systematic literature review (SLR). As our guiding question, we investigate the guarantees and capabilities of blockchain-based enactment approaches. Based on resulting empirical evidence, we develop a taxonomy for blockchain-based enactment. We find that a wide range of approaches support traceability and correctness; however, research focusing on flexibility and scalability remains nascent. For all challenges, we point towards future research opportunities.