Giovanni Ciatto, Stefano Mariani, Alfredo Maffi, Andrea Omicini
A common use case for blockchain smart contracts (SC) is that of governing interaction amongst mutually untrusted parties, by automatically enforcing rules for interaction. However, while many contributions in the literature assess SC computational expressiveness, an evaluation of their power in terms of coordination (i.e., governing interaction) is still missing. This is why in this paper we test mainstream SC implementations by evaluating their expressive power in coordinating both inter-users and inter-SC activities. To do so, we exploit the archetypal Linda coordination model as a benchmark—a common practice in the field of coordination models and languages—by discussing to what extent mainstream blockchain technologies support its implementation. As they reveal some notable limitations (affecting, in particular, coordination between SC) we then show how Tenderfone, a custom blockchain implementation providing for a more expressive notion of SC, addresses the aforementioned limitations.
To make good use of valuable Internet of Things (IoT) data assets, this paper proposes a trust-aware IoT data economic system (TIDES) with complete IoT data pricing, trading and protection functions. To ensure reliable and automatic data trading, the entire trading process is automatically performed by smart contracts on a hierarchical blockchain. Moreover, we develop several sophisticated methods to ensure the efficiency and service quality of TIDES. First, a complete evaluation model that takes the data trading profile and reputation into consideration is proposed for both suppliers and demanders to assess the trustworthiness of their trading partners. Second, a client-centric data value evaluation model and a game-theory-based pricing model are used to promote win-win transactions in which the demanders obtain higher quality data at an acceptable price and the suppliers receive higher profits. Third, a dispute arbitration model is invoked to detect suspicious trading and refund these payments automatically. TIDES further utilizes a multi-access edge computing (MEC) architecture to alleviate the huge burdens of IoT devices from blockchain operations, reduce the trading latency, and help mobile devices to trade IoT data. The simulation results have shown the advantages of TIDES in terms of trading time, storage overhead, data trading profit, quality data trading, pricing efficiency, and reliability on data asset management and trading.
When actions by one agent force another to deviate from their agreements with a third, "victim" turns into "injurer" in the chain's subsequent steps. Should the chain's initiator be responsible only for the direct harm they cause or also bear some of the indirect losses they trigger? Through an axiomatic approach, we<br/>characterize the class of fixed-fraction rules, which strike a balance between incentives for accident prevention on the one hand and fairness in terms of how liabilities are assigned on the other. Their simple design make the rules ideal for practical implementation through smart contracts, enabling automated conflict resolution.
Spatial crowdsourcing is an effective and novel method. In crowdsourcing systems, a centralized platform is traditionally used to allocate tasks and select workers. Centralized platforms always face following challenges: 1) How to ensure the rationality of tasks allocating; 2) How to ensure the payments of workers in the system when dishonest requesters exist; 3) How to ensure the maximum number of tasks are assigned. 4) How to ensure the integrity and reliability of the centralized platform. To solve these problems, this article proposed a distributed blockchain-based crowdsourcing framework - TSWCrowd (Task Select Worker Crowd). In this framework, tasks are sorted according to specific rules, thus tasks with higher priority are assigned to workers earlier. Workers who are available for a task will be selected and return a result. Then the deployed smart contracts will pay the basic payment automatically. At the same time, relevant contracts also calculate and pay the quality payment according to the proposed quality reward formulation. The proposed TSWCrowd framework on-chain involves a public dataset and uses solidity to compile the smart contracts. The framework was deployed on a local private blockchain. The decentralization property of the blockchain ensures the reliable assignment of tasks. Task-select-worker (TSW) algorithm sorts tasks to ensure reliability. In this paper, the proposed framework was compared with the ABCrowd auction mechanism on-chain and the VCG mechanism off-chain. The results show that the average distance is shorter and the payment is higher, thus reaches the reasonability, reliability and availability.
Understanding the complexities of blockchain governance is urgent. The aim of this paper is to draw on other theories of governance to provide insight into the design of blockchain governance mechanisms. We define blockchain governance as the processes by which stakeholders (those who are affected by and can affect the network) exercise bargaining power over the network. Major considerations include the definition of stakeholders, how the consensus mechanism distributes endogenous bargaining power between those stakeholders, the interaction of exogenous governance mechanisms and institutional frameworks, and the needs for bootstrapping networks. We propose that on-chain governance models can only be partial because of the existence of implicit contracts that embed expectations of return among diverse stakeholders.
Pablo Lamela Seijas, Alexander Nemish, David Smith, Simon Thompson
Marlowe is a DSL for financial contracts. We describe the implementation of Marlowe on the Cardano blockchain, and the Marlowe Playground web-based development and simulation environment. Contracts in Marlowe can be exhaustively analysed prior to running them, thus providing strong guarantees to participants in the contract. The Marlowe system itself has been formally verified using the Isabelle theorem prover, establishing such properties as the conservation of money.
Blockchain-based smart contracts have emerged as a popular means of enforcing agreements among a collection of parties without a prior assumption of trust. However, it has proven difficult to write correct contracts that are robust when operating in the adversarial environment of public blockchains. This thesis evaluates the ability of a domain-specific contract programming language to support the expression and systematic testing of practical smart contracts. We present the design, implementation, and evaluation of Quartz, a contract language based on the state machine model of execution.The design and evaluation of Quartz is grounded in a suite of case study smart contracts. These are intended to span a wide range of application scenarios and design patterns encountered in practice by contract developers. The language's implementation is organized around the translation of a contract to two targets: a formal specification expressed in TLA+ and an implementation expressed in Solidity. Through its support for model checking contract specifications, Quartz enables the discovery of implementation flaws identical to those that have compromised real-world smart contracts. Moreover, its generated Solidity code imposes at most minor execution overhead compared to equivalent handwritten code. Finally, we discuss Quartz's future potential to validate contracts against economic notions of correctness, which are often central concerns in contract design yet are not addressed by current verification techniques.
Juan Ignacio Ibañez, Chris N. Bayer, Paolo Tasca, Jiahua Xu
During the last half century, the concept of shared ledger systems that offer a single source of truth has challenged traditional bookkeeping, leading to innovations such as the resource-event-agent (REA) accounting framework, triple-entry accounting (TEA), and blockchain. Despite these advancements, the historical development of shared ledger systems remains under-researched and unclear, with the influence of REA on TEA particularly overlooked. This study aims to fill this gap by conducting a genealogical analysis of shared ledger systems, with a focus on tracing the development of TEA and its historical byproduct of the REA framework designed by McCarthy. Through a comprehensive literature review and interviews with pioneers in REA, TEA, and blockchain, we uncover the missing link between REA and TEA. Our findings suggest that the current explosion of shared ledger systems results from the convergence of three parallel research streams, occasionally interacting with each other. We correct common misconceptions, acknowledge the influence of key individuals, and map out the overlapping paths of REA, TEA, and blockchain. By elucidating the historical evolution of shared ledger systems, this study contributes to the academic debate and fosters further discourse among researchers in REA, TEA, and blockchain, thereby enhancing the potential applications within these fields.
Abstract Solidity is the dominant programming language for Ethereum smart contracts. This paper presents a high-level formalization of the Solidity language with a focus on the memory model. The presented formalization covers all features of the language related to managing state and memory. In addition, the formalization we provide is effective: all but few features can be encoded in the quantifier-free fragment of standard SMT theories. This enables precise and efficient reasoning about the state of smart contracts written in Solidity. The formalization is implemented in the SOLC-VERIFY verifier and we provide an extensive set of tests that covers the breadth of the required semantics. We also provide an evaluation on the test set that validates the semantics and shows the novelty of the approach compared to other Solidity-level contract analysis tools.
João Santos Reis, Paul Crocker, Simão Melo de Sousa
This paper introduces Tezla, an intermediate representation of Michelson smart contracts that eases the design of static smart contract analysers. This intermediate representation uses a store and aims to preserve the semantics, flow and resource usage of the original smart contract. This enables properties like gas consumption to be statically verified. We provide an automated decompiler of Michelson smart contracts to Tezla. In order to support our claim about the adequacy of Tezla, we develop a static analyser that takes advantage of the Tezla representation of Michelson smart contracts to prove simple but non-trivial properties.
Maha Kadadha, Rabeb Mizouni, Shakti Singh, Hadi Otrok · 5 authors
In this paper, a fully distributed auction-blockchain-based crowdsourcing framework is proposed-ABCrowd. In a typical crowdsourcing framework, independent workers compete to be allocated requesters' tasks. These workers advertise their costs to the centralized platform, which then decides the final allocation of tasks. While performing the allocation, centralized platforms face two main challenges: 1) how to ensure trusted execution for the allocation of tasks, and 2) how to motivate workers to declare their truthful costs. To address these challenges, ABCrowd proposes to run the crowdsourcing platform entirely on Ethereum Blockchain while incorporating auctions. Blockchain and smart contracts guarantee trusted execution for the allocation through autonomous and transparent on-Chain execution. ABCrowd uses the Repeated-Single-Minded Bidder (R-SMB) auction mechanism, which motivates workers to bid truthfully before allocating them and calculating their payments. R-SMB is an approximation of the optimized off-Chain Vickrey-Clarke-Groves (VCG) mechanism in terms of maximized profit. It entails repeating the Single-Minded Bidder (SMB) auction mechanism to meet the allocation requirement of crowdsourcing applications. ABCrowd is implemented and evaluated using Solidity on a private Ethereum Blockchain, where a real publicly available dataset is used. The proposed on-Chain R-SMB auction mechanism is compared to the off-Chain VCG mechanism, where the results show that R-SMB provides similar performance to VCG in terms of the average number of allocated tasks. Furthermore, R-SMB outperforms VCG in workers' travelled distance and requesters' costs, at a low execution cost.
Streaming media has been largely used by millions of users every day. The number of customers and programs, e.g., TV series, movies, and various shows, are still growing fast. However, the demand for video transcoding for various personal terminal devices results in the shortage of computing resources and the prolongation of processing delay in centralized video transcoding systems. To solve this issue, we propose a blockchain, especially, smart contract based scheme that can achieve decentralized and on-demand crowdsourcing for video transcoding, which remarkably mitigates the transcoding overhead. Specifically, our scheme consists of four key components such as employers, workers, task allocation, and payment. An employer initializes the smart contract, releases the task, and initiates the smart contract. Workers bid for the task, and the successful bidder will obtain the task and execute the task. The task allocation mechanism and the payment mechanism can guarantee the profits of both and encourage both as well. Moreover, the smart contract consists of the bidding contract and the task execution contract. The extensive analysis of our proposed scheme justified the feasibility, security for defending against typical threats, applicability in realistic situations, and portability for most multimedia such as videos and audios.
Gianmaria Del Monte, Diego Pennino, Maurizio Pizzonia
Public blockchains should be able to scale with respect to the number of nodes and to the transactions workload. The blockchain scalability trilemma has been informally conjectured. This is related to scalability, security and decentralization, stating that any improvement in one of these aspects should negatively impact on at least one of the other two. In fact, despite the large research and experimental effort, all known approaches turn out to be tradeoffs. We theoretically describe a new blockchain architecture that scales to arbitrarily high workload provided that a corresponding proportional increment of nodes is provisioned. We show that, under reasonable assumptions, our approach does not require tradeoffs on security or decentralization. To the best of our knowledge, this is the first result that disprove the trilemma considering the scalability of all architectural elements of a blockchain and not only the consensus protocol. While our result is currently only theoretic, we believe that our approach may stimulate significant practical contributions.
Bitcoin is the first and most successful Blockchain system so far. In the Bitcoin system, miners use transaction attached fees as a driving force to mine a new block and package transactions, while users compete by bidding transaction fees for faster confirmation. Considering the particularity of Bitcoin trading system, we take time series into consideration to analyze the transaction rules of Bitcoin system from the perspective of multiple cycles and establish a dynamic game model related to time under Generalised Second Price(GSP) mechanism, and also confirm the model's superiority on saving users' fees, compared with the static game model. Also, we propose the quantification of the user experience quantified by calculating the price difference between the transactions uploaded by the same user within adjacent times, making the transaction process of the Bitcoin system no longer the final say of the transaction price. The dynamic game model shows that there is a perfect Bayesian game equilibrium solution in the payment decision, so there is no incentive for users to change the attached fee, and the whole system is maintained stably. In addition, we verify the dynamic game model from computational experiment. Firstly, it is proved that with the help of revenue discount, the cost saving of the dynamic model is generally higher than that of the static model. Then the user's revenue under the dynamic model is showing an upward trend, and the transactions order under the dynamic model is more stable than that under static model, which can be illustrated mathematically and computationally that the proposed dynamic game model in this paper will help all transactions be processed more efficiently in a uniform pipeline.
The exploitation of smart-contract vulnerabilities can have catastrophic consequences such as the loss of millions of pounds worth of crypto assets. Formal verification can be a useful tool in identifying vulnerabilities and proving that they have been fixed. In this paper, we present a formalisation of Solidity and the Ethereum blockchain using the Solid language and its blockchain; a Solid program is obtained by explicating/desugaring a Solidity program. We make some abstractions that over-approximate the way in which Solidity/Ethereum behave. Based on this formalisation, we create Solidifier: a bounded model checker for Solidity. It translates Solid into Boogie, an intermediate verification language, that is later verified using Corral, a bounded model checker for Boogie. Unlike much of the work in this area, we do not try to find specific behavioural/code patterns that might lead to vulnerabilities. Instead, we provide a tool to find errors/bad states, i.e. program states that do not conform with the intent of the developer. Such a bad state, be it a vulnerability or not, might be reached through the execution of specific known code patterns or through behaviours that have not been anticipated.