Itay Tsabary, Matan Yechieli, Alex Manuskin, Ittay Eyal
Smart Contracts and transactions allow users to implement elaborate constructions on cryptocurrency blockchains like Bitcoin and Ethereum. Many of these constructions, including operational payment channels and atomic swaps, use a building block called Hashed Time-Locked Contract (HTLC). In this work, we distill from HTLC a specification (HTLC-Spec), and present an implementation called Mutual-Assured-Destruction Hashed Time-Locked Contract (MAD-HTLC). MAD-HTLC employs a novel approach of utilizing the existing blockchain operators, called miners, as part of the design. If a user misbehaves, MAD-HTLC incentivizes the miners to confiscate all her funds. We prove MAD-HTLC's security using the UC framework and game-theoretic analysis. We demonstrate MAD-HTLC's efficacy and analyze its overhead by instantiating it on Bitcoin's and Ethereum's operational blockchains. Notably, current miner software makes only little effort to optimize revenue, since the advantage is relatively small. However, as the demand grows and other revenue components shrink, miners are more motivated to fully optimize their fund intake. By patching the standard Bitcoin client, we demonstrate such optimization is easy to implement, making the miners natural enforcers of MAD-HTLC. Finally, we extend previous results regarding HTLC vulnerability to bribery attacks. An attacker can incentivize miners to prefer her transactions by offering high transaction fees. We demonstrate this attack can be easily implemented by patching the Bitcoin client, and use game-theoretic tools to qualitatively tighten the known cost bound of such bribery attacks in presence of rational miners. We identify bribe opportunities occurring on the Bitcoin and Ethereum main networks where a few dollars bribe could yield tens of thousands of dollars in reward (e.g., \$2 for over \$25K).
Blockchain forks can have severe economic implications, sow uncertainty and undermine trust. In this paper, we introduce a formal framework to study the emergence, persistency and economic consequences of blockchain forks. We argue that blockchain forks can be process- or protocol-based and emerge unintentionally or deliberately. We then proceed with a sub-classification of protocol-based forks and study the circumstances under which a chain split may become permanent. It can be shown that the persistency of a fork depends on the nature of the change to the consensus rules and on the relative allocation of the consensus-relevant resources. Lastly, we discuss business implications as well as potential consequences for policy makers and practitioners.
This paper explores the connection between software contracts and smart contracts. Despite the assonance, these two terms denote quite different concepts: software contracts are logical properties of software components, while smart contracts are programs executed on blockchains. What is the relation between them? We answer this question by discussing how to integrate software contracts in the design of programming languages for smart contracts.
With the evolving complexity of software systems, interest in software performance analysis has increasingly grown in recent years. Its main objective is to optimize software applications by analyzing its structure, behavior and dependencies, from design to code. Blockchain technologies, also known as distributed ledger technologies, have gained a lot of popularity in the recent years. Particularly the Ethereum blockchain, which apart from having its own cryptocurrency, is programmable. Meaning that developers can use it to create new decentralized applications which rely on smart contracts. Smart contracts are immutable computer programs that run deterministically in the context of the Ethereum Virtual Machine. The main purpose of this report is to explain the process of development of a tool to assist Ethereum developers to visually analyze static and dynamic behaviour of their smart contracts to improve their performance through optimizing gas usage.
David Minarsch, Seyed Ali Hosseini, Marco Favorito, Jonathan S. Ward
The user experience of interacting with distributed ledger technologies (DLT) is fraught with excessive complexity, high risk and unintuitive processes. Moreover, smart contracts deployed in these systems are restricted to being reactive. These limitations have negative implications on user adoption and prevent DLTs from being general purpose. We introduce a framework for the development of Autonomous Economic Agents (AEAs), software agents that act autonomously and pursue an economic goal, and demonstrate how AEAs complement existing decentralised ledgers as a second layer technology. In particular, the framework enables a simplified user experience through automation, supports modularisation and reuse of complex decision making and machine learning capabilities, and allows for proactive behaviour facilitating autonomy. We demonstrate these gains in the context of a specific use-case, a multi-agent trading system modelling a Walrasian Exchange Economy populated by a number of agents trading a basket of tokens.
In this paper, we present a pricing mechanism that aligns incentives of agents who exchange resources on a decentralized ledger with the goal of maximizing transaction throughput. Subdividing a blockchain ledger into shards promises to greatly increase transaction throughput with minimal loss of security. However, the organization and type of the transactions also affects the ledger's efficiency, which is increased by wallet agents transacting in a single shard whenever possible while collectively distributing their transactions uniformly across the available shards. Since there is no central authority to enforce these properties, the only means of achieving them is to design the system such that it is in agents' interest to act in a way that benefits overall throughput. We show that our proposed pricing policy does exactly this by inducing a potential game for the agents, where the potential function relates directly to ledger throughput. Simulations demonstrate that this policy leads to near-optimal throughput under a variety of conditions.
Luís Pedro Arrojado da Horta, João Santos Reis, Mário Pereira, Simão Melo de Sousa
This paper introduces WhylSon, a deductive verification tool for smart contracts written in Michelson, which is the low-level language of the Tezos blockchain. WhylSon accepts a formally specified Michelson contract and automatically translates it to an equivalent program written in WhyML, the programming and specification language of the Why3 framework. Smart contract instructions are mapped into a corresponding WhyML shallow-embedding of the their axiomatic semantics, which we also developed in the context of this work. One major advantage of this approach is that it allows an out-of-the-box integration with the Why3 framework, namely its VCGen and the backend support for several automated theorem provers. We also discuss the use of WhylSon to automatically prove the correctness of diverse annotated smart contracts.
The tokenization of assets deployed to distributed ledger technology is increasingly cited to revolutionize financial services by allowing traditionally illiquid assets to be bought and sold on primary and secondary markets increasing asset liquidity, transparency and reducing transaction completion time. To realize these benefits it is important the token is transferrable, that is, portable from one distributed ledger to another. In this paper we survey current interoperability architectures and smart contract languages, identifying factors affecting the portability of tokenized assets. We propose a portability maturity model that can be used to help assess the current state of technology and supporting market infrastructure.
Abstract A smart contract (SC) is a programme stored in the Ethereum blockchain by a contract‐creation transaction. SC developers deploy an instance of the SC and attempt to execute it in exchange for a fee, paid in Ethereum coins (Ether). If the computation needed for their execution turns out to be larger than the effort proposed by the developer (i.e., the gasLimit ), their client instantiation will not be completed successfully. In this paper, we examine SCs from 11 Ethereum blockchain‐oriented software projects hosted on GitHub.com , and we evaluate the resources needed for their deployment (i.e., the gasUsed ). For each of these contracts, we also extract a suite of object‐oriented metrics, to evaluate their structural characteristics. Our results show a statistically significant correlation between some of the object‐oriented (OO) metrics and the resources consumed on the Ethereum blockchain network when deploying SCs. This result has a direct impact on how Ethereum developers engage with a SC: evaluating its structural characteristics, they will be able to produce a better estimate of the resources needed to deploy it. Other results show specific source code metrics to be prioritised based on application domains when the projects are clustered based on common themes.
Clara Schneidewind, Ilya Grishchenko, Markus Scherer, Matteo Maffei
Ethereum has emerged as the most popular smart contract development platform, with hundreds of thousands of contracts stored on the blockchain and covering a variety of application scenarios, such as auctions, trading platforms, and so on. Given their financial nature, security vulnerabilities may lead to catastrophic consequences and, even worse, they can be hardly fixed as data stored on the blockchain, including the smart contract code itself, are immutable. An automated security analysis of these contracts is thus of utmost interest, but at the same time technically challenging for a variety of reasons, such as the specific transaction-oriented programming mechanisms, which feature a subtle semantics, and the fact that the blockchain data which the contract under analysis interacts with, including the code of callers and callees, are not statically known. In this work, we present eThor, the first sound and automated static analyzer for EVM bytecode, which is based on an abstraction of the EVM bytecode semantics based on Horn clauses. In particular, our static analysis supports reachability properties, which we show to be sufficient for capturing interesting security properties for smart contracts (e.g., single-entrancy) as well as contract-specific functional properties. Our analysis is proven sound against a complete semantics of EVM bytecode and an experimental large-scale evaluation on real-world contracts demonstrates that eThor is practical and outperforms the state-of-the-art static analyzers: specifically, eThor is the only one to provide soundness guarantees, terminates on 95% of a representative set of real-world contracts, and achieves an F-measure (which combines sensitivity and specificity) of 89%.
Clara Schneidewind, Ilya Grishchenko, M. Schérer, Matteo Maffei
Ethereum has emerged as the most popular smart contract development platform,\nwith hundreds of thousands of contracts stored on the blockchain and covering a\nvariety of application scenarios, such as auctions, trading platforms, and so\non. Given their financial nature, security vulnerabilities may lead to\ncatastrophic consequences and, even worse, they can be hardly fixed as data\nstored on the blockchain, including the smart contract code itself, are\nimmutable. An automated security analysis of these contracts is thus of utmost\ninterest, but at the same time technically challenging for a variety of\nreasons, such as the specific transaction-oriented programming mechanisms,\nwhich feature a subtle semantics, and the fact that the blockchain data which\nthe contract under analysis interacts with, including the code of callers and\ncallees, are not statically known.\n In this work, we present eThor, the first sound and automated static analyzer\nfor EVM bytecode, which is based on an abstraction of the EVM bytecode\nsemantics based on Horn clauses. In particular, our static analysis supports\nreachability properties, which we show to be sufficient for capturing\ninteresting security properties for smart contracts (e.g., single-entrancy) as\nwell as contract-specific functional properties. Our analysis is proven sound\nagainst a complete semantics of EVM bytecode and an experimental large-scale\nevaluation on real-world contracts demonstrates that eThor is practical and\noutperforms the state-of-the-art static analyzers: specifically, eThor is the\nonly one to provide soundness guarantees, terminates on 95% of a representative\nset of real-world contracts, and achieves an F-measure (which combines\nsensitivity and specificity) of 89%.\n
Cong T. Nguyen, Diep N. Nguyen, Hoang Thai Dinh, Hoang-Anh Pham · 7 authors
Mobile service providers (MSPs) are particularly vulnerable to roaming frauds, especially ones that exploit the long delay in the data exchange process of the contemporary roaming management systems, causing multi-billion dollars loss each year. In this paper, we introduce BlockRoam, a novel blockchain-based roaming management system that provides an efficient data exchange platform among MSPs and mobile subscribers. Utilizing the Proof-of-Stake (PoS) consensus mechanism and smart contracts, BlockRoam can significantly shorten the information exchanging delay, thereby addressing the roaming fraud problems. Through intensive analysis, we show that the security and performance of such PoS-based blockchain network can be further enhanced by incentivizing more users (e.g., subscribers) to participate in the network. Moreover, users in such networks often join stake pools (e.g., formed by MSPs) to increase their profits. Therefore, we develop an economic model based on Stackelberg game to jointly maximize the profits of the network users and the stake pool, thereby encouraging user participation. We also propose an effective method to guarantee the uniqueness of this game's equilibrium. The performance evaluations show that the proposed economic model helps the MSPs to earn additional profits, attracts more investment to the blockchain network, and enhances the network's security and performance.
Philip Daian, Steven Goldfeder, Tyler Kell, Yunqi Li · 8 authors
Blockchains, and specifically smart contracts, have promised to create fair and transparent trading ecosystems.Unfortunately, we show that this promise has not been met. We document and quantify the widespread and rising deployment of arbitrage bots in blockchain systems, specifically in decentralized exchanges (or "DEXes"). Like high-frequency traders on Wall Street, these bots exploit inefficiencies in DEXes, paying high transaction fees and optimizing network latency to frontrun, i.e., anticipate and exploit, ordinary users' DEX trades.We study the breadth of DEX arbitrage bots in a subset of transactions that yield quantifiable revenue to these bots. We also study bots' profit-making strategies, with a focus on blockchain-specific elements. We observe bots engage in what we call priority gas auctions (PGAs), competitively bidding up transaction fees in order to obtain priority ordering, i.e., early block position and execution, for their transactions. PGAs present an interesting and complex new continuous-time, partial-information, game-theoretic model that we formalize and study. We release an interactive web portal, frontrun.me, to provide the community with real-time data on PGAs. We additionally show that high fees paid for priority transaction ordering poses a systemic risk to consensus-layer security. We explain that such fees are just one form of a general phenomenon in DEXes and beyond-what we call miner extractable value (MEV)-that poses concrete, measurable, consensus-layer security risks. We show empirically that MEV poses a realistic threat to Ethereum today. Our work highlights the large, complex risks created by transaction-ordering dependencies in smart contracts and the ways in which traditional forms of financial-market exploitation are adapting to and penetrating blockchain economies.
The EVM language is a simple stack-based language with words of 256 bits, with one significant difference between the EVM and other virtual machine languages (like Java Bytecode or CLI for .Net programs): the use of the stack for saving the jump addresses instead of having it explicit in the code of the jumping instructions. Static analyzers need the complete control flow graph (CFG) of the EVM program in order to be able to represent all its execution paths. This report addresses the problem of obtaining a precise and complete stack-sensitive CFG by means of a static analysis, cloning the blocks that might be executed using different states of the execution stack. The soundness of the analysis presented is proved.
Smart contract is a disruptive FinTech that is signed in advance and automatically executed when the goods are received. Therefore, the buyer will settle accounts without delay payment under smart contract, which benefits the supplier in B2B transactions. However, how to motivate the buyer to participate in smart contract? In this paper, we consider a supplier selling goods through retailers such as Wal-Mart in a co-opetitive supply chain, where the retailer buys and resells the supplier's goods and the supplier encroaches on the market by opening a direct channel. Without smart contract, the supplier incurs cash opportunity cost because of the retailer's delay payment (referred to as Traditional Contract scenario). With smart contract, the retailer needs to pay the supplier immediately when the goods arrive (referred to as Smart Contract scenario). We use Generalized Nash Bargaining to formulate the contract negotiation, and show that the adoption of smart contract changes the competition and cooperation between the supplier and the retailer both vertically and horizontally. We find that, when the supplier's unit cash opportunity cost is high (low), the smart contract enhances (weakens) the coordination in the reselling channel, increases (decreases) the reselling channel's market share compared to the direct-selling channel, and increases (lowers) the retailer's proportion in the reselling revenue. Interestingly, we show that, when the supplier's bargaining power is moderate or extremely low, it prefers traditional contract when the unit cash opportunity cost is moderate. We also show that, the retailer and the supplier have incentive alignment to adopt smart contract when the supplier's unit cash opportunity cost is high. We further study the impact of the supplier's merchant discount fee under traditional contract and its commission cost when the direct channel is an online store, finding that our main results are qualitatively unchanged.
The performance of existing permissionless smart contract platforms such as Ethereum is limited by the consensus layer. Prism is a new proof-of-work consensus protocol that provably achieves throughput and latency up to physical limits while retaining the strong guarantees of the longest chain protocol. This paper reports experimental results from implementations of two smart contract virtual machines, EVM and MoveVM, on top of Prism and demonstrates that the consensus bottleneck has been removed. Code can be found at https://github.com/wgr523/prism-smart-contracts.
Guido Felipe Valderrama Herrera, Leonardo Garcia Sanchez
Este trabajo analiza la relación que tienen las ventas en corto, los sesgos de los agentes junto la interacción de los fundamentales de oferta y demanda respecto la formación de precios en el mercado del Bitcoin. Dentro del análisis encontramos que las tendencias aportadas en la literatura se mantienen en cuanto a las ventas en corto y sus restricciones a pesar de no encontrar evidencia estadística.
Cilj ovog rada je otkriti i proširiti moje znanje o distribuiranim mrežama i teoriji aukcija izradom koncept aplikacije za aukcije na Ethereum mreži koristeći pametne ugovore. Nezamjenjivi tokeni koriste se za stvaranje digitalne povjerljivosti, a prvi put bili su implementirani koristeći Ethereum ERC721 token standard. NFT-Auction-dapp je aplikacija bazirana na Ethereumu koja omogućuje korisnicima da kreiraju i sudjeluju u aukcijama NFT tokena u stvarnom vremenu, na globalnoj i distribuiranoj mreži, zadržavajući garancije plaćanja i dostave. U radu ću se služiti znanjima koja sam stekao tijekom studija na Visokom učilištu Algebra i znanjima koja sam stekao samostalno kako bih izgradio aplikaciju, objavio ju na javnu Ethereum mrežu i testirao njezinu funkcionalnost.
Blockchain technology and artificial intelligence (AI) are current hot topics\nin research and practice. However, the potentials of their combination have\nbeen studied just recently to a larger extend. While different use cases for\ncombining AI and blockchain have been discussed, the idea of enabling\nblockchain-based smart contracts to perform "smarter" decisions by using AI or\nmachine learning (ML) models has only been considered on the conceptual level\nso far. It remained open, how such AI-enabled smart contracts could be\nimplemented in a robust way for real-world applications. Therefore, in this\npaper a new, enterprise-class implementation of AI-enabled smart contracts is\npresented and first insights regarding its feasibility are discussed.\n
Background: Executing, verifying and enforcing credible transactions on permissionless blockchains is done using smart contracts. A key challenge with smart contracts is ensuring their correctness and security. Several test input generation techniques for detecting vulnerabilities in smart contracts have been proposed in the last few years. However, a comparison of proposed techniques to gauge their effectiveness is missing. Aim: This paper conducts an empirical evaluation of testing techniques for smart contracts. The testing techniques we evaluated are: (1) Blackbox fuzzing, (2) Adaptive fuzzing, (3) Coverage-guided fuzzing with an SMT solver and (4) Genetic algorithm. We do not consider static analysis tools, as several recent studies have assessed and compared effectiveness of these tools. Method: We evaluate effectiveness of the test generation techniques using (1) Coverage achieved - we use four code coverage metrics targeting smart contracts, (2) Fault finding ability - using artificially seeded and real security vulnerabilities of different types. We used two datasets in our evaluation - one with 1665 real smart contracts from Etherscan, and another with 90 real contracts with known vulnerabilities to assess fault finding ability. Result: We find Adaptive fuzzing performs best in terms of coverage and fault finding over contracts in both datasets. Conclusion: However, we believe considering dependencies between functions and handling Solidity specific features will help improve the performance of all techniques considerably.
The confluence of Internet of Things(IoT) , Blockchain(BC) and Artificial Intelligence(AI) acts as a key accelerator for enabling Machine Economy. To be ready for future businesses these technologies needs to be adapted by extending the IoT capabilities to Economy of Things (EoT) capabilities. In this paper we focus on one such implementation experience for Smart Toll Transaction application in the domain of mobility. Our paper showcases a possible solution by leveraging negotiations, decision making, distributed learning capabilities at the devices level using AI-enabled Multi-Agent Systems and the real-time smart contracts between the Cars and Tolls using Blockchain. This solution also showcases the monetization of real time data coming from various IoT devices which are part of vehicles and infrastructure. While blockchain secures the privacy of the participants it also acts as an economic transactional layer and governance layer between the devices in the networ
Blockchain technology is the distributed, decentralised ledger technology underlying Bitcoin and other cryptocurrencies. We apply Oliver Williamson’s transactions cost analysis to the blockchain consensus mechanism. Blockchains reduce the costs of opportunism but are not ‘trustless’. We show that blockchains are trust machines. Blockchains are platforms for three-sided bargaining that convert energy-intensive computation into economically-valuable trust.
In the area of blockchains, a wallet is anything that manages the access to cryptocurrencies and tokens. Off-chain wallets appear in different forms, from paper wallets to hardware wallets to dedicated wallet apps, while on-chain wallets are realized as smart contracts. Wallet contracts are supposed to increase trust and security by being transparent and by offering features like daily limits, approvals, multiple signatures, and recovery mechanisms. The most prominent platform for smart contracts in general and the token ecosystem im particular, and thus also for wallet contracts is Ethereum. Our work aims at a better understanding of wallet contracts on Ethereum, since they are one of the most frequently deployed smart contracts. By analyzing source code, bytecode, and execution traces, we derive usage scenarios and patterns. We discuss methods for identifying wallet contracts in a semi-automatic manner by looking at the deployed bytecodes and the on-chain interaction patterns. We extract blueprints for wallets and compile a ground truth. Furthermore, we differentiate characteristics of wallets in use, and group them into six types. We provide numbers and temporal perspectives regarding the creation and use of wallets. For the 40 identified blueprints, we compile detailed profiles. We analyze the data of the Ethereum main chain up to block 11,500,000, mined on December 22, 2020.