Formal Methods for Secure Bitcoin Smart Contracts
Authors: Stefano Lande
The notion of smart contracts was introduced in 1997 by Nick Szabo, to describe agreements among mutually distrusting parties that can be automatically enforced without resorting to a trusted intermediary. Then, the idea was mostly forgotten due to the technical impossibility to implement it. The advent of distributed ledger technologies, pioneered by Bitcoin, provided a technical foundation to reshape and develop smart contracts.
Since smart contracts handle the ownership of valuable assets, attackers may be tempted to exploit vulnerabilities in their implementation to steal or tamper with these assets. For instance, a series of vulnerabilities in Ethereum contracts have been exploited, causing money losses in the order of hundreds of millions of dollars.
Over the last years, a variety of smart contracts for Bitcoin have been proposed, both by the academic community and by that of developers. However, the heterogeneity in their treatment, the informal (often incomplete or imprecise) descriptions, and the use of poorly documented Bitcoin features, poses obstacles to the development of secure smart contracts. Using formal models and domain-specific languages to describe the behaviour of the underlying platform, and to model contracts, could help to overcome these security issues, by reducing the distance between the intended behaviour of a contract and the implementation.
In this thesis, we propose a formal model of Bitcoin transactions, which is the foundation for a new process algebra for defining Bitcoin smart contracts. Furthermore, we present a toolchain for developing smart contracts in BitML, a domain-specific language based on the contributions of this thesis. Moreover, we propose a new extension to Bitcoin, called neighbourhood covenants, which extends its expressiveness as a smart contract platform. We then exploit neighbourhood covenants to implement fungible tokens on Bitcoin.
Highlighting poor anonymity and security practice in the blockchain of Bitcoin
Authors: Stefano Bistarelli, Ivan Mercanti, Francesco Faloci, and Francesco Santini
We highlight how Bitcoin addresses are reused in transactions (implicitly or explicitly), despite recommendations and best practice strongly advise to avoid this. We analyse the blockchain with the purpose to find and count highly reused Bitcoin addresses, starting from the birth of the protocol in 2009. In this study we also include hidden addresses: these addresses are not the explicit endpoints of a transaction, but they are somehow contained in it (e.g., in the script of a Pay to Script Hash transaction). Finally, we try to de-anonymise the top-100 reused addresses, grouping and linking them to their wallet owner. This work shows that such a misuse in reusing the address often corresponds to malicious activities in the bitcoin ecosystem. These results push towards a mandatory single usage, which mitigates dangerous consequences.
Ethanos: efficient bootstrapping for full nodes on account-based blockchain
Authors: Jae-Yun Kim, Junmo Lee, Yeonjae Koo, Sanghyeon Park, and Soo-Mook Moon
Ethereum is a popular account-based blockchain whose number of accounts and transactions has skyrocketed, causing its data explosion. As a result, ordinary clients using PCs or smartphones cannot easily bootstrap as a full node, but rely on other full nodes to verify transactions, thus being exposed to security risks. The most serious overhead is caused by synchronizing the state of all accounts in the block’s state trie, which takes several tens of gigabytes. Observing that more than 95% of the accounts are dormant, we propose a novel state optimization technique, named Ethanos. Ethanos downsizes the state trie by periodically emptying it, and then re-build it only with the active accounts used in the period’s transactions. Ethanos runs transactions using the accounts available in the current period’s state trie as well as those available at the end of the previous period’s state trie. For an account in neither of the tries, the account first restores itself by transmitting a restore transaction. One important result of this state management is that a node can now bootstrap only with the latest period’s state trie, yet can fully verify all transactions thereafter. We evaluated Ethanos with real Ethereum transactions for 300,000 blocks from the 7.0 million block, with a one-week period of emptying the state trie. Our result shows that Ethanos can sharply reduce the state trie, with only a tiny fraction of the restore transactions. More importantly, unlike the Ethereum state trie which continues to grow as time goes on, the Ethanos state trie size at the end of each period is bounded by a few hundred MB, when there are more than one million, one-week-active accounts.
Blockchain Technologies Vulnerability to Quantum Attacks
Authors: Joseph J. Kearney and Carlos A. Perez-Delgado
Quantum computation represents a threat to many cryptographic protocols in operation today. It has been estimated that by 2035, there will exist a quantum computer capable of breaking the vital cryptographic scheme RSA2048. Blockchain technologies rely on cryptographic protocols for many of their essential sub-routines. Some of these protocols, but not all, are open to quantum attacks. Here we analyze the major blockchain-based cryptocurrencies deployed today—including Bitcoin, Ethereum, Litecoin and ZCash, and determine their risk exposure to quantum attacks. We finish with a comparative analysis of the studied cryptocurrencies and their underlying blockchain technologies and their relative levels of vulnerability to quantum attacks.
Dynamic Topology Awareness in Active Distribution Networks Using Blockchain-based State Estimations
Author: Xingzhi Li, Bei Han, Guo-Jie Li, Lingen Luo, Keyou Wang, and Xiuchen Jiang
With growing complexity and uncertainty from distributed generations and active customers, distribution networks are facing more unexpected events and topology changes; while very limited measurements may degrade the observability of distribution system states and endanger the security of the system. Meanwhile, massive data from various type of users (if they can be used), can be valuable for power utilities. This makes privacy and data security a more critical issue, while being endowed with operation and market flexibilities. Thus, we propose a blockchain-based privacy-protecting approach for Dynamic Topology Awareness (DTA), including three layers of physical, cyber and business. At the bottom (physical layer), distribution network is partitioned into subareas and tie-line areas, coping with local data from measurement devices or users. Estimated border values from parallel local estimations would be examined through data consistency checking. And DTA consensus algorithm might be triggered, querying historical status stored as blockchain contracts for anomalies detections and new block formations. Voting mechanism is then adopted to verify new blocks from data tampering. Performance of proposed DTA approach is validated through simulations to identify topology changes and cyber anomalies, with additional discussions on the trade-off between DTA sensitivity and estimation accuracy.
Off-chain Execution and Verification of Computationally Intensive Smart Contracts
Authors: Emrah Sariboz, Kartick Kolachala, Gaurav Panwar, Roopa Vishwanathan, and Satyajayant Misra
We propose a novel framework for off-chain execution and verification of computationally-intensive smart contracts. Our framework is the first solution that avoids duplication of computing effort across multiple contractors, does not require trusted execution environments, supports computations that do not have deterministic results, and supports general-purpose computations written in a high-level language. Our experiments reveal that some intensive applications may require as much as 141 million gas, approximately 71x more than the current block gas limit for computation in Ethereum today, and can be avoided by utilizing the proposed framework.
Security Analysis Methods for Detection and Repair of DoS Vulnerabilities in Smart Contracts
Author: Behkish Nassirzadeh
In recent years we have witnessed a dramatic increase in the applications of blockchain and smart contracts in a variety of contexts, including supply-chain, decentralized finance, and international money transfers. However, a critical stumbling block to their further adoption is smart contract security (or more precisely, the lack thereof). Smart contracts, once deployed on a blockchain, are immutable. Hence, unlike traditional software systems, smart contracts are particularly vulnerable to latent security issues. It is therefore imperative that security analysis tools be developed that help improve smart contract security if they are to have continued adoption and impact. A particularly widespread class of security vulnerabilities that afflicts Ethereum smart contracts is the gas-based denial of service (DoS). Briefly, these vulnerabilities generally present in contracts containing unbounded loops.
To address the described problem, we present Gas Gauge, a tool aimed at detecting gasbased DoS vulnerabilities in Ethereum smart contracts. Gas Gauge consists of three major components: the Detection Phase, Identification Phase, and Correction Phase. First, we describe a highly accurate static analysis approach that finds all the loops in a smart contract (the Detection Phase). Then, a set of inputs that causes the contract to run out of gas is generated using a fuzzing approach. The last component uses static analysis and run-time verification to predict the maximum loop bounds consistent with allowable gas usage automatically. This component uses a binary search approach and an independent parallel processing design to speed up the process. Each part of the tool can be used separately for different purposes or all together to detect, identify and help repair the contracts vulnerable to out-of-gas behaviors.
Gas Gauge was tested on 2,000 real-world solidity smart contracts. The results were compared to seven state-of-the-art tools, and it was empirically demonstrated that Gas Gauge is highly effective and useful.
SAILFISH: Vetting Smart Contract State-Inconsistency Bugs in Seconds
Authors: Priyanka Bose, Dipanjan Das, Yanju Chen, Yu Feng, Christopher Kruegel, and Giovanni Vigna
This paper presents SAILFISH, a scalable system for automatically finding state-inconsistency bugs in smart contracts. To make the analysis tractable, we introduce a hybrid approach that includes (i) a light-weight exploration phase that dramatically reduces the number of instructions to analyze, and (ii) a precise refinement phase based on symbolic evaluation guided by our novel value-summary analysis, which generates extra constraints to over-approximate the side effects of whole-program execution, thereby ensuring the precision of the symbolic evaluation. We developed a prototype of SAILFISH and evaluated its ability to detect two state-inconsistency flaws, viz., reentrancy and transaction order dependence (TOD) in Ethereum smart contracts. Further, we present detection rules for other kinds of smart contract flaws that SAILFISH can be extended to detect. Our experiments demonstrate the efficiency of our hybrid approach as well as the benefit of the value summary analysis. In particular, we show that SAILFISH outperforms five state-ofthe-art smart contract analyzers (SECURIFY, MYTHRIL, OYENTE, SEREUM and VANDAL) in terms of performance, and precision. In total, SAILFISH discovered 47 previously unknown vulnerable smart contracts out of 89,853 smart contracts from ETHERSCAN.
n-HTLC: Neo Hashed Time-Lock Commitment to Defend Against Wormhole Attack in Payment Channel Networks
Authors: Susil Kumar Mohanty and Somanath Tripathy
In today’s cryptocurrency, the Payment Channel Network (PCN) is noticed as one of the most gifted off-chain solutions for scalability issues. Besides this, it consumes lesser transaction fees and low transaction confirmation time. However, security and privacy issues need to be addressed appropriately to make the solution even more effective. Most of the existing HTLC (Hashed Time-Lock Contract) protocols revealed the sender’s information to the intermediate users in the payment route. In this work, we propose an effective secure and privacy-preserving Payment Channel Network protocol, named Neo Hashed Time-Lock Commitment (n-HTLC) protocol. (n-HTLC) does not require the sender to send any information to each intermediate user along the payment route, thus preserves the identity of the sender. But, (n-HTLC) is not compatible with Sphinx onion packet format. Therefore, a symmetric key encryption-based protocol called k-TLC has been proposed. k-TLC is compatible with the Sphinx onion packet format, which is used in the current Lightning network atop of the Bitcoin blockchain network. The security of both n-HTLC and kTLC are proved using the Universal Composability (UC) framework. It is observed that both ensure that no attacker can extract information on the payment route if at least one of the users in the path is honest. To analyze the performance of both n-HTLC and kTLC payment protocol, we conduct experiments using the snapshots of Ripple network1, Lightning network2, and synthetic network of Mazumdar and Ruj (2020). Our experimental results show that both n-HTLC and kTLC outperform state-of-the-art off-chain payment protocols in terms of computational and communication overhead.
Towards Understanding Cryptocurrency Derivatives: A Case Study of BitMEX
Authors: Kyle Soska, Jin-Dong Dong, Alex Khodaverdian, Ariel Zetlin-Jones, Bryan Routledge, and Nicolas Christin
Since 2018, the cryptocurrency trading landscape has evolved from a collection of spot markets (fiat for cryptocurrency) to a hybrid ecosystem featuring complex and popular derivatives products. In this paper we explore this new paradigm through a study of BitMEX, one of the first and most successful derivatives platforms for leveraged cryptocurrency trading. BitMEX trades on average over 3 billion dollars worth of volume per day, and allows users to go long or short Bitcoin with up to 100x leverage. We analyze the evolution of BitMEX products—both settled and perpetual offerings that have become the standard across other cryptocurrency derivatives platforms. We additionally utilize on-chain forensics, public liquidation events, and a site-wide chat room to describe the diverse ensemble of amateur and professional traders that forms this community. These traders range from wealthy agents running automated strategies, to individuals trading small, risky positions and focusing on very short time-frames. Finally, we discuss how derivative trading has impacted cryptocurrency asset prices, notably how it has led to dramatic price movements in the underlying spot markets.
Bitcoin Address Clustering Method Based on Multiple Heuristic Conditions
Authors: He Xi, He Ketai, Lin Shenwen, Yang Jinglin, and Mao Hongliang
We analyzed the associations between Bitcoin transactions and addresses to cluster address and further find groups of addresses controlled by the same entity. It revealed the vulnerabilities of Bitcoin anonymity mechanism, which could be used by the law enforcement agencies to track and crack down illegal transactions. However, single heuristic method and incomplete heuristic conditions were difficult to cluster a large number of addresses comprehensively and accurately. Therefore, this paper reviewed a variety of heuristics, and used multiple heuristics comprehensively to cluster addresses to improve the degree of address aggregation and address recall rate, which laid a foundation for further inferring of entity identity.