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.
The paper presents a model for decentralizing building information modelling, through implementing its infrastructure using the decentralized web. We discuss the shortcomings of BIM in terms of its infrastructure, with a focus on tracing identities of design authorship in this collective design tool. In parallel we examine the issues with BIM in the cloud and propose a decentralized infrastructure based on the Ethereum blockchain and the Interplanetary filesystem (IPFS). A series of computing nodes, that act as nodes on the Ethereum Blockchain, host disk storage with which they participate in a larger storage pool on the Interplanetary Filesystem. This storage is made available through an API is used by architects and designers creating and editing a building information model that resides on the IPFS decentralised storage. Through this infrastructure central servers are eliminated, and BIM libraries and models can be shared with others in an immutable and transparent manner. As such Architecture practices are able to exploit their intellectual property in novel ways, by making it public on the internet. The infrastructure also allows the decentralised creation of a resilient global pool of data that allows the participation of computation agents in the creation and simulation of BIM models.
Abstract We develop an economic model to compare equilibrium security of Proof-of-Work (PoW) versus Proof-of-Stake (PoS) blockchains. We derive general conditions to determine when PoW blockchains are more secure than otherwise equivalent PoS blockchains and vice versa. Applying real-world parameter values to these conditions, we demonstrate that PoS blockchains are more secure than otherwise equivalent PoW blockchains. Furthermore, we demonstrate that PoS’s security advantage over PoW is particularly salient for high-scale blockchains.
We assess how the cost structure of cryptocurrency mining affects the response of miners to exchange rate fluctuations and the immutability of cryptocurrency ledgers that rely on proof-of-work. We show that the amount of mining power supplied to currencies that rely on specialized hardware, such as Bitcoin, responds less to adverse exchange rate shocks than other currencies respond to such shocks, a fact that is instrumental to avoiding double-spending attacks. The results may change if mining equipment used for one cryptocurrency can be transferred to another. For smaller currencies with low exchange rate correlation, transferability eliminates the protection that fixed costs provide. Our results weaken doomsday predictions for Bitcoin and other cryptocurrencies with declining block rewards. This paper was accepted by Bruno Biais, Special Section of Management Science: Blockchains and Crypto Economics. Supplemental Material: The data files are available at https://doi.org/10.1287/mnsc.2023.4901 .
Automated market makers, first popularized by Hanson's logarithmic market scoring rule (or LMSR) for prediction markets, have become important building blocks, called 'primitives,' for decentralized finance. A particularly useful primitive is the ability to measure the price of an asset, a problem often known as the pricing oracle problem. In this paper, we focus on the analysis of a very large class of automated market makers, called constant function market makers (or CFMMs) which includes existing popular market makers such as Uniswap, Balancer, and Curve, whose yearly transaction volume totals to billions of dollars. We give sufficient conditions such that, under fairly general assumptions, agents who interact with these constant function market makers are incentivized to correctly report the price of an asset and that they can do so in a computationally efficient way. We also derive several other useful properties that were previously not known. These include lower bounds on the total value of assets held by CFMMs and lower bounds guaranteeing that no agent can, by any set of trades, drain the reserves of assets held by a given CFMM.
Most carbon Emission Trading Systems (ETS) rely on a centralized system to manage the transactional tasks, and are vulnerable to security threats. This article proposes a Blockchain-enabled Distributed ETS (BD-ETS) to improve the security and efficiency of the system. The BD-ETS transforms the centralized Carbon Emissions Permit (CEP) trading mode to a distributed trading system in which the trading mode is based on a smart contract performed in Hyperledger Fabric. In a smart contract, every transaction considers both the offer price and reputation value of the emitting enterprises. The voting power of the emitting enterprise is determined by its reputation value, which stems from their contributions to carbon emission reduction. To achieve consistency of every node in the CEP transactions, we propose a Delegated Proof of Reputation (DPoR) consensus mechanism. Compared to the enhanced Delegated Proof of Stake, the DPoR decreases the attack intention of malicious enterprises and performs better in finding malicious miners faster, thus improving the security of the BD-ETS. A case study and numerical simulations are developed to illustrate how the CEP trading functions, and to validate the DPoR mechanism.
We implement two versions of a simple but illustrative smart contract: one in Solidity on the Ethereum blockchain platform, and one in Plutus on the Cardano platform, with annotated code excerpts and with source code attached. We get a clearer view of the Cardano programming model in particular by introducing a novel mathematical abstraction which we call Idealised EUTxO. For each version of the contract, we trace how the architectures of the underlying platforms and their mathematics affects the natural programming styles and natural classes of errors. We prove some simple but novel results about alpha-conversion and observational equivalence for Cardano, and explain why Ethereum does not have them. We conclude with a wide-ranging and detailed discussion in the light of the examples, mathematical model, and mathematical results so far.
More than eight million smart contracts have been deployed into Ethereum, which is the most popular blockchain that supports smart contract. However, less than 1% of deployed smart contracts are open-source, and it is difficult for users to understand the functionality and internal mechanism of those closed-source contracts. Although a few decompilers for smart contracts have been recently proposed, it is still not easy for users to grasp the semantic information of the contract, not to mention the potential misleading due to decompilation errors. In this paper, we propose the first system named STAN to generate descriptions for the bytecodes of smart contracts to help users comprehend them. In particular, for each interface in a smart contract, STAN can generate four categories of descriptions, including functionality description, usage description, behavior description, and payment description, by leveraging symbolic execution and NLP (Natural Language Processing) techniques. Extensive experiments show that STAN can generate adequate, accurate, and readable descriptions for contract's bytecodes, which have practical value for users.