The number of attacks and accidents leading to significant losses of crypto-assets is growing. According to Chainalysis, in 2021, approx. $14 billion has been lost due to various incidents, and this number is dominated by Decentralized Finance (DeFi) applications. In order to address these issues, one can use a collection of tools ranging from auditing to formal methods. We use formal verification and provide the first formalisation of a DeFi contract in a foundational proof assistant capturing contract interactions. We focus on Dexter2, a decentralized, non-custodial exchange for the Tezos network similar to Uniswap on Ethereum. The Dexter implementation consists of several smart contracts. This poses unique challenges for formalisation due to the complex contract interactions. Our formalisation includes proofs of functional correctness with respect to an informal specification for the contracts involved in Dexter's implementation. Moreover, our formalisation is the first to feature proofs of safety properties of the interacting smart contracts of a decentralized exchange. We have extracted our contract from Coq into CameLIGO code, so it can be deployed on the Tezos blockchain. Uniswap and Dexter are paradigmatic for a collection of similar contracts. Our methodology thus allows us to implement and verify DeFi applications featuring similar interaction patterns.
Eduardo Castelló Ferrer, Ivan Berman, Aleksandr Kapitonov, Vadim Manaenko · 6 authors
The physical autonomy of robots is well understood both theoretically and practically. By contrast, there is almost no research exploring their potential economic autonomy. In this paper, we present the first economically autonomous robot -- a robot able to produce marketable goods while having full control over the use of its generated income. Gaka-chu ("painter" in Japanese) is a 6-axis robot arm that creates paintings of Japanese characters from an autoselected keyword. By using a blockchain-based smart contract, Gaka-chu can autonomously list a painting it made for sale in an online auction. In this transaction, the robot interacts with the human bidders as a peer not as a tool. Using the blockchain-based smart contract, Gaka-chu can then use its income from selling paintings to replenish its resources by autonomously ordering materials from an online art shop. We built the Gaka-chu prototype with an Ethereum-based smart contract and ran a 6-month long experiment, during which the robot created and sold four paintings, simultaneously using its income to purchase supplies and repay initial investors. In this work, we present the results of the experiments conducted and discuss the implications of economically autonomous robots.
Developing secure smart contracts remains a challenging task. Existing approaches are either impractical or leave the burden to developers for fixing bugs. In this paper, we propose the first practical smart contract compiler, called HCC, which automatically inserts security hardening checks at the source-code level based on a novel and language-independent code property graph (CPG) notation. The high expressiveness of our developed CPG allows us to mitigate all of the most common smart contract vulnerabilities, namely reentrancy, integer bugs, suicidal smart contracts, improper use of tx.origin, untrusted delegate-calls, and unchecked low-level call bugs. Our large-scale evaluation on 10k real-world contracts and several sets of vulnerable contracts from related work demonstrates that HCC is highly practical, outperforms state-of-the-art contract hardening techniques, and effectively prevents all verified attack transactions without hampering functional correctness.
Smart contracts on Ethereum handle millions of U.S. Dollars and other financial assets. In the past, attackers have exploited smart contracts to steal these assets. The Ethereum community has developed plenty of tools to detect vulnerable smart contracts. However, there is no standardized data set to evaluate these existing tools, or any new tools developed. There is a need for an unbiased standard benchmark of real-world Ethereum smart contracts. We have created ScrawlD: an annotated data set of real-world smart contracts taken from the Ethereum network. The data set is labelled using 5 tools that detect various vulnerabilities in smart contracts, using majority voting.
Hyoung Joong Kim, Soohyuk Choi, Yong Tae Yoon, Shiyong Yoo
Smart contract is an important building block of blockchain. Automated market makers are working without an order book, and they determine the price of assets automatically. It is reported that he automated market makers have the impermanent loss, which causes financial damage to liquidity providers. Impermanent loss makes the liquidity providers hesitant to deposit assets in the liquidity pool. Therefore, their participation incentive from liquidity provision should be anticipated by automatic market makers inherently. However, the existence of impermanent gain has never been reported. Impermanent gain is important to attract liquidity providers without giving compensation incentives. This study shows that for some automated market makers, impermanent gain coexists with impermanent loss. Examples showing the coexistence and conditions are provided.
In this paper, we will consider a governance token pricing algorithm that conducts liquidity operations on AMM (CPMM) DEXs (automated market maker decentralized exchanges) with liquidity that belongs to a decentralized autonomous organization (DAO), also called protocol-owned liquidity (POL). The primary aim of the protocol is maintaining a price peg by determining algorithmically when and how to carry out interventions that consist of two steps: extracting liquidity from an AMM liquidity pool and conducting "token swap" operations. We will cover setting up an optimal peg function as a weighted sum of certain normalized factors, which are to be determined collectively by the DAO. In particular, we will review various arithmetic invariants of liquidity intervention, which brings the price to a peg while leaving total liquidity intact, and show how such interventions can be substituted in practice by so-called PMM (proactive market maker) protocols.
Transactions submitted through the blockchain peer-to-peer (P2P) network may leak out exploitable information. We study the economic incentives behind the adoption of blockchain dark venues, where users' transactions are observable only by miners on these venues. We show that miners may not fully adopt dark venues to preserve rents extracted from arbitrageurs, hence creating execution risk for users. The dark venue neither eliminates frontrunning risk nor reduces transaction costs. It strictly increases the payoff of miners, weakly increases the payoff of users, and weakly reduces arbitrageurs' profits. We provide empirical support for our main implications, and show that they are economically significant. A 1% increase in the probability of being frontrun raises users' adoption rate of the dark venue by 0.6%. Arbitrageurs' cost-to-revenue ratio increases by a third with a dark venue.
Blockchain - the decentralized global ledger technology provides a potentially attractive alternate to organize modern finance. Organizations use ERP software to integrate the management of all major business processes. Instead, blockchain can provide single version of the truth, in real time, regardless of constraints, to all participants across the organizational boundaries.
This research critically analyses blockchain scaling solutions based on their ability to realistically balance the properties of the blockchain trilemma. We have concluded this research by outlining a gap in the current body of literature and implementation of scalability solutions. An extended UTXO transaction model is proposed to overcome challenges associated with implementing both layer one and layer two scaling solutions in a blockchain system. The examination of industry approaches is used to justify this direction and puts forth a basis for future work.
Recently, many Delegated Proof-of-Stake (DPoS)-based blockchains have been widely used in decentralized applications, such as EOSIO, Tron, and Binance Smart Chain. Compared with traditional PoW-based blockchain systems, these systems achieve a higher transaction throughput and are well adapted to large-scale scenes in daily applications. Decentralization is a key element in blockchain networks. However, little is known about the evolution of decentralization in DPoS-based blockchain networks. In this paper, we conduct a systematic analysis on the decentralization of DPoS with data from up to 135,000,000 blocks in EOSIO, the first successful DPoS-based blockchain system. We characterize the decentralization evolution of the two phases in DPoS, namely block producer election and block production. Moreover, we study the voters with similar voting behaviors and propose methods to discover abnormal mutual voting behaviors in EOSIO. The analytical results show that our methods can effectively capture the decentralization evolution and abnormal voting phenomena in the system, which also have reference significance for other DPoS-based blockchains.
We study a scenario where an adjudication task (e.g., the resolution of a binary dispute) is outsourced to a set of agents who are appointed as jurors. This scenario is particularly relevant in a Web3 environment, where no verification of the adjudication outcome is possible, and the appointed agents are, in principle, indifferent to the final verdict. We consider simple adjudication mechanisms that use (1) majority voting to decide the final verdict and (2) a payment function to reward the agents with the majority vote and possibly punish the ones in the minority. Agents interact with such a mechanism strategically: they exert some effort to understand how to properly judge the dispute and cast a yes/no vote that depends on this understanding and on information they have about the rest of the votes. Eventually, they vote so that their utility (i.e., their payment from the mechanism minus the cost due to their effort) is maximized. Under reasonable assumptions about how an agent's effort is related to her understanding of the dispute, we show that appropriate payment functions can be used to recover the correct adjudication outcome with high probability. Our findings follow from a detailed analysis of the induced strategic game and make use of both theoretical arguments and simulation experiments.
A transaction fee mechanism (TFM) is an essential component of a blockchain protocol. However, a systematic evaluation of the real-world impact of TFMs is still absent. Using rich data from the Ethereum blockchain, the mempool, and exchanges, we study the effect of EIP-1559, one of the earliest-deployed TFMs that depart from the traditional first-price auction paradigm. We conduct a rigorous and comprehensive empirical study to examine its causal effect on blockchain transaction fee dynamics, transaction waiting times, and consensus security. Our results show that EIP-1559 improves the user experience by mitigating intrablock differences in the gas price paid and reducing users' waiting times. However, EIP-1559 has only a small effect on gas fee levels and consensus security. In addition, we find that when Ether's price is more volatile, the waiting time is significantly higher. We also verify that a larger block size increases the presence of siblings. These findings suggest new directions for improving TFMs.
Péter Garamvölgyi, Yuxi Liu, Dong Zhou, Fan Long · 5 authors
Traditional public blockchain systems typically had very limited transaction throughput because of the bottleneck of the consensus protocol itself. With recent advances in consensus technology, the performance limit has been greatly lifted, typically to thousands of transactions per second. With this, transaction execution has become a new performance bottleneck. Exploiting parallelism in transaction execution is a clear and direct way to address this and to further increase transaction throughput. Although some recent literature introduced concurrency control mechanisms to execute smart contract transactions in parallel, the reported speedup that they can achieve is far from ideal. The main reason is that the proposed parallel execution mechanisms cannot effectively deal with the conflicts inherent in many blockchain applications. In this work, we thoroughly study the historical transaction execution traces in Ethereum. We observe that application-inherent conflicts are the major factors that limit the exploitable parallelism during execution. We propose to use partitioned counters and special commutative instructions to break up the application conflict chains in order to maximize the potential speedup. When we evaluated the maximum parallel speedup achievable, these techniques doubled this limit to an 18x overall speedup compared to serial execution, thus approaching the optimum. We also propose OCC-DA, an optimistic concurrency control scheduler with deterministic aborts, which makes it possible to use OCC scheduling in public blockchain settings.
Dimitris Karakostas, Aggelos Kiayias, Thomas Zacharias
We study Nash-dynamics in the context of blockchain protocols. We introduce a formal model, within which one can assess whether the Nash dynamics can lead utility-maximizing participants to defect from the "honest" protocol operation, towards variations that exhibit one or more undesirable infractions, such as abstaining from participation and producing conflicting protocol histories. Blockchain protocols that do not lead to such infraction states are said to be compliant. Armed with this model, we evaluate the compliance of various Proof-of-Work (PoW) and Proof-of-Stake (PoS) protocol families, with respect to different utility functions and reward schemes, leading to the following results: i) PoS ledgers under resource-proportional rewards can be compliant if costs are negligible, but non-compliant if costs are significant; ii) PoW and PoS under block-proportional rewards exhibit different compliance behavior, depending on the lossiness of the network; iii) PoS ledgers can be compliant w.r.t. one infraction, i.e., producing conflicting messages, but non-compliant (and non-equilibria) w.r.t. abstaining or an attack we call selfish signing; iv) taking externalities, such as exchange rate fluctuations, into account, we quantify the benefit of economic penalties, in the context of PoS protocols, in disincentivizing particular infractions.
Yangguang Tian, R. Edward Minchin, Christian Vriborg Petersen, E Moayed · 5 authors
Abstract Infrastructure is critical for enabling society to function and the economy to thrive. Unfortunately, there is an increasing mismatch between the need for infrastructure investment and available financing globally due to constraints on public resources and limited capacity to effectively leverage private sector co-financing in the current system. This research explores the integration of blockchain-enabled asset tokenization with public-private partnership (PPP) project finance to engage private sector resources and innovation to supplement limited public sector capacities and to leverage the inherent efficiencies in infrastructure financing. A conceptual framework of tokenization-enabled PPP project finance is proposed. The transactional and contractual structures of the blockchain-driven infrastructure financing system are illustrated and evaluated. It is found that the potential benefits can be summarized into three categories: better project management, improved bankability, and enhanced inclusivity.
Recent literature has addressed initial coin offering (ICO) projects, which are an innovative form of venture financing through cryptocurrencies using blockchain technology. Many features of ICOs remain unexplored, leaving much room for additional research, including the success factors of ICO projects. We investigate the success of ICO projects, with our main purpose being to identify factors that influence a project's outcome. Following a literature review, from which several potential variables were collected, we used a database comprising 428 ICO projects in the banking/financial sector to regress several econometric models. We confirmed the impacts of several variables and obtained particularly valuable results concerning project and campaign variables. We confirmed the importance of a well-structured and informative whitepaper. The proximity to certain markets with high availability of financial and human capital is also an important determinant of the success of an ICO. We also confirm the strong dependency on cryptocurrency and the impact of cryptocurrency valuations on the success of a project. Furthermore, we confirm the importance of social media in ICO projects, as well as the importance of human capital characteristics. Our research contributes to the ICO literature by capturing most of the success factors previously identified and testing their impacts based on a large database. The current research contributes to the building of systems theory and signaling theory by adapting their frameworks to the ICO environment. Our results are also important for regulators, as ICOs are mainly unregulated and have vast future potential, and for investors, who can benefit from our analysis and use it in their due diligence.
Matheus V. X. Ferreira, Daniel J. Moroz, David C. Parkes, Mitchell Stern
In recent years, prominent blockchain systems such as Bitcoin and Ethereum have experienced explosive growth in transaction volume, leading to frequent surges in demand for limited block space and causing transaction fees to fluctuate by orders of magnitude. Existing systems sell space using first-price auctions; however, users find it difficult to estimate how much they need to bid in order to get their transactions accepted onto the chain. If they bid too low, their transactions can have long confirmation times. If they bid too high, they pay larger fees than necessary. In light of these issues, new transaction fee mechanisms have been proposed, most notably EIP-1559, aiming to provide better usability. EIP-1559 is a history-dependent mechanism that relies on block utilization to adjust a base fee. We propose an alternative design - a dynamic posted-price mechanism - which uses not only block utilization but also observable bids from past blocks to compute a posted price for subsequent blocks. We show its potential to reduce price volatility by providing examples for which the prices of EIP-1559 are unstable while the prices of the proposed mechanism are stable. More generally, whenever the demand for the blockchain stabilizes, we ask if our mechanism is able to converge to a stable state. Our main result provides sufficient conditions in a probabilistic setting for which the proposed mechanism is approximately welfare optimal and the prices are stable. Our main technical contribution towards establishing stability is an iterative algorithm that, given oracle access to a Lipschitz continuous and strictly concave function f, converges to a fixed point of f.
We introduce the SPRIG (Smart Proofs via Recursive Information Gathering) protocol. SPRIG allows agents to propose, question, and defend mathematical proofs in a decentralized fashion. A structure of stakes and bounties aims at producing debates in good faith and if those persist, they must go down to machine-level details, where they can be settled automatically. This combination of economic incentives and an oracle is designed to promote succinct and informative proofs. SPRIG can run autonomously as a smart contract on a blockchain platform, and hence it does not rely on a central trusted institution. We translate SPRIG into a general game-theoretic model and prove that the protocol satisfies two desirable properties: no spamming and monotonicity. We then characterize analytically the equilibrium of a simple two-player specification of the model: this provides important insights into the impact of the protocol’s parameters on the probabilities that it induces type I/II errors. We conclude by discussing the main attacks SPRIG’s designers will need to take into account.
Jan 1, 2022·Proceedings of the ... Annual Hawaii International Conference on System Sciences/Proceedings of the Annual Hawaii International Conference on System Sciences
Leonardo Maria De Rossi, Michel Avital, Rob Gleasure
Over the last decade, numerous studies have examined the remarkable appreciation of cryptocurrencies and have typically focused on their price and the factors that predict them. In contrast, this paper argues that the success of a cryptocurrency is determined not only by its monetary value but also by the proliferation of its end users. Specifically, we hypothesize that changes in developers’ and miners’ activities drive the growing proliferation of a cryptocurrency’s end users. Building on the Bitcoin case, we use a time-series model based on 4,285 Bitcoin daily observations to suggest that changes in the number of end users are anticipated by surges or drops in activity by the developers and miners who develop and maintain the network. We further find a limited relationship between these variables and the price of Bitcoin. These results support an alternative view of cryptocurrencies’ success and highlight further research avenues in this nascent domain.
Elvira Albert, Pablo Gordillo, Alejandro Hernández-Cerezo, Clara Rodríguez-Núñez · 5 authors
Abstract The use of the Ethereum blockchain platform [17] has experienced an enormous growth since its very first transaction back in 2015 and, along with it, the verification and optimization of the programs executed in the blockchain (known as Ethereum smart contracts ) have raised considerable interest within the research community.