- Merkle Trees Optimized for Stateless Clients in Bitcoin
Authors: Bolton Bailey and Suryanarayana Sankagiri
The ever-growing size of the Bitcoin UTXO state is a factor preventing nodes with limited storage capacity from validating transactions. Cryptographic accumulators, such as Merkle trees, offer a viable solution to the problem. Full nodes create a Merkle tree from the UTXO set, while stateless nodes merely store the root of the Merkle tree. When provided with a proof, stateless nodes can verify that a transaction’s inputs belong to the UTXO set. In this work, we present a systematic study of Merkle tree based accumulators, with a focus on factors that reduce the proof size. Based on the observation that UTXOs typically have a short lifetime, we propose that recent UTXOs be co-located in the tree. When proofs for different transactions are batched, such a design reduces the per-transaction proof size. We provide details of our implementation of this idea, describing certain optimizations that further reduce the proof size in practice. On Bitcoin data before August 2019, we show that our design achieves a 4.6x reduction in proof size vis-a-vis UTREEXO [10], which is a different Merkle-tree based system designed to support stateless nodes.
Link: https://www.ifca.ai/fc21/wtsc/WTSC21paper8.pdf
- On-Chain Smart Contract Verification over Tendermint
Authors: Luca Olivieri, Fausto Spoto, and Fabio Tagliaferro
Smart contracts are computer code that runs in blockchain and expresses the rules of an agreement among parties. A bug in their code has major consequences, such as rule violations and security attacks. Smart contracts are immutable and cannot be easily replaced to patch a bug. To overcome these problems, there exist automatic static analyzers that find bugs before smart contracts are installed in blockchain. However, this off-chain verification is optional: programmers are not forced to use it. This paper defines on-chain verification instead, that occurs inside the same blockchain nodes, when the code of smart contracts is installed. It acts as a mandatory entry filter that bans code that does not abide to the verification rules, that are consequently part of the consensus rules of the blockchain. Thus, an improvement in on-chain verification entails a consensus update of the network. This paper provides an implementation of on-chain verification for smart contracts written in the Takamaka subset of Java, running as a Tendermint application. It shows that on-chain verification works, reporting actual experiments.
Link: https://www.ifca.ai/fc21/wtsc/WTSC21paper1.pdf
- Post-Quantum Verifiable Random Function from Symmetric Primitives in PoS Blockchain
Authors: Maxime Buser, Rafael Dowsley, Muhammed F. Esgin, Shabnam Kasra Kermanshahi, Veronika Kuchta, Joseph K. Liu, Raphael Phan, and Zhenfei Zhang
In this work, we study verifiable random functions (VRF) that may resist quantum threats. VRFs have a wide range of applications and play a key role in Proof-of-Stake blockchains, such as Algorand. Our main proposal is a VRF construction X-VRF based on XMSS signature scheme. Our construction is the first quantum-safe VRF proposal based on symmetric primitives. Being based on symmetric-key primitives that have long been studied, X-VRF provides strong confidence that it can withstand quantum attacks in the long run. Despite its stateful nature, we empower XMSS with blockchain so that the users do not need to maintain individual states. While increasing the usability of XMSS, our technique also enforces honest behaviour when creating an X-VRF output so as to satisfy the fundamental uniqueness property of VRFs. We show how X-VRF can be used in the Algorand setting to extend it to a quantum-safe blockchain, and provide various instances of X-VRF, each may suit a different setting. Our X-VRF instances are the most efficient quantum-safe VRF proposals in the literature. Our extensive performance evaluation, analysis, and implementation indicates the effectiveness of our proposed constructions in practice. In particular, we show that X-VRF can maintain a very competitive throughput close to the existing Algorand protocol and can produce substantially more transactions per second than Bitcoin.
Link: https://eprint.iacr.org/2021/302.pdf
- EthVer: Formal verification of randomized Ethereum smart contracts
Authors: Łukasz Mazurek
Despite the great potential capabilities and the mature technological solutions, the smart contracts have never been used at a large scale, one of the reasons being the lack of good methods for verification of correctness and security of the contracts — although the technology itself (e.g. the Ethereum platform) is well studied and secure, the actual smart contracts are human-made and thus inherently error-prone. As a consequence, critical vulnerabilities in the contracts are discovered and exploited every few months. The most prominent example of a buggy contract was the infamous DAO attack — a successful attack on the largest Ethereum contract in June 2016 resulting in $70 mlnworth Ether stolen and the hard fork of the Ethereum network (80% of Ethereum users decided to revert the transaction and hence two parallel transaction histories exist from that event). The main contribution of this work is the automatic method of formal verification of randomized Ethereum smart contracts. We formally define and implement the translation of the contracts into MDP (Markov decision process) formal models which can be verified using the PRISM model checker — a state of the art tool for formal verification of models. As a proof of concept, we use our tool, EthVer, to verify two smart contracts from the literature: the Rock-Paper-Scissors protocol from K. Delmolino et al., Step by step towards creating a safe smart contract: Lessons and insights from a cryptocurrency lab. and the Micropay 1 protocol from R. Pass, a. shelat, Micropayments for decentralized currencies.
Link: https://www.ifca.ai/fc21/wtsc/WTSC21paper3.pdf
- Survey on Blockchain Networking: Context, State-of-the-Art, Challenges
Authors: Maya Dotan, Yvonne-Ann Pignolet, Stefan Schmid, Saar Tochner, and Aviv Zohar
Blockchains in general and cryptocurrencies such as Bitcoin in particular are realized using distributed systems and hence critically rely on the performance and security of the interconnecting network. The requirements on these networks and their usage, however can differ significantly from traditional communication networks, with implications on all layers of the protocol stack. This paper is motivated by these differences, and in particular by the observation that many fundamental design aspects of these networks are not well-understood today. In order to support the networking community to contribute to this emerging application domain, we present a structured overview of the field, from topology and neighbor discovery, over block and transaction propagation, to sharding and off-chain networks, also reviewing existing empirical results from different measurement studies. In particular, for each of these domains, we provide the context, highlighting differences and commonalities with traditional networks, review the state-of-the-art, and identify open research challenges. Our paper can hence also be seen as a call-to-arms to improve the foundation on top of which blockchains are built.
Link: https://www.univie.ac.at/ct/stefan/csur21crypto.pdf
- HashSplit: Exploiting Bitcoin Asynchrony to Violate Common Prefix and Chain Quality
Authors: Muhammad Saad, Afsah Anwar, Srivatsan Ravi, and David Mohaisen
The safety of the Bitcoin blockchain relies on strong network synchrony. Therefore, violating the blockchain safety requires strong adversaries who control a mining pool with ≈ 51% hash rate. In this paper, we show that the network synchrony does not hold in the real world Bitcoin network, which can be exploited to amortize the cost of various attacks. Towards that, first we construct the Bitcoin ideal world functionality to formally specify its ideal execution model in a synchronous network. We then develop a large-scale data collection system through which we connect with more than 36K IP addresses of the Bitcoin nodes and identify 359 mining nodes. We contrast the Bitcoin ideal functionality against real world measurements to expose network anomalies that can be exploited to optimize the existing attacks. Particularly, we observe high block propagation delay in the Bitcoin network causing weak network synchronization: on average, in 9.97 minutes, only 39% nodes have the up-to-date blockchain. Through a fine-grained analysis, we discover non-uniform block propagation delay among the mining nodes showing that the Bitcoin network is asynchronous. To realize the threat of asynchronous network, we present the HashSplit attack that allows an adversary to orchestrate concurrent mining on multiple branches of the blockchain to violate common prefix and chain quality properties. We also propose the attack countermeasures by releasing a Bitcoin Core version that closely models the Bitcoin ideal functionality. Our measurements, theoretical modeling, proposed attack, and countermeasures open new directions in the security evaluation of Bitcoin and similar blockchain systems.
Link: https://eprint.iacr.org/2021/299.pdf
- Absentia: secure function evaluation on Ethereum
Authors: Didem Demirag and Jeremy Clark
This paper describes a blockchain-based approach for secure function evaluation (SFE) in the setting where multiple participants have private inputs (multiparty computation) that no other individual should learn. The emphasis of Absentia is reducing the participants’ work to a bare minimum, where they can effectively have the computation performed in their absence and they can trust the result. While we use an SFE protocol (Mix and Match) that can operate perfectly well without a blockchain, the blockchain does add value in at least three important ways: (1) the SFE protocol requires a secure bulletin board and blockchains are the most widely deployed data structure with bulletin board properties (immutability and non-equivocation under reasonable assumptions); (2) blockchains provide a built-in mechanism to financially compensate participants for the work they perform; and (3) a publicly verifiable SFE protocol can be checked by the blockchain network itself, absolving the users of having to verify that the function was executed correctly. We benchmark Absentia on Ethereum. While it is too costly to be practical (a single gate costs thousands of dollars), it sets a research agenda for future improvements. We also alleviate the cost by composing it with Arbitrum, a layer 2 ‘roll-up’ for Ethereum which reduces the costs by 94%.
Link: https://www.ifca.ai/fc21/wtsc/WTSC21paper4.pdf
- Empirical Analysis of On-chain Voting with Smart Contracts
Authors: Robert Muth and Florian Tschorsch
Blockchains and smart contracts promise transparency, verifiability, and self-enforcing agreements. Against this background, novel use cases such as decentralized governance platforms that implement voting to collectively manage funds have emerged. While a number of arguments against blockchain-based voting exist, we still see a relevance. In this paper, we therefore present a quantitative analysis of the Ethereum blockchain with respect to voting. To this end, we develop a blockchain analysis toolchain that we use to analyze 3 173 smart contracts on the Ethereum Mainnet with voting functionality. We extract insights on the complexity of deployed voting methods and reveal a trend towards a centralization of funds, i.e., five smart contracts manage 98 % of funds comprising more than four million USD. We additionally analyze the feasibility of on-chain voting for Ethereum as well as other well-established blockchains that are used for voting, i.e., Bitcoin and Dash.
Link: https://www.ifca.ai/fc21/wtsc/WTSC21paper5.pdf
- SciviK: A Versatile Framework for Specifying and Verifying Smart Contracts
Authors: Shaokai Lin, Xinyuan Sun, Jianan Yao, and Ronghui Gu
The growing adoption of smart contracts on blockchains poses new security risks that can lead to significant monetary loss, while existing approaches either provide no (or partial) security guarantees for smart contracts or require huge proof effort. To address this challenge, we present SciviK, a versatile framework for specifying and verifying industrial-grade smart contracts. SciviK’s versatile approach extends previous efforts with three key contributions: (i) an expressive annotation system enabling built-in directives for vulnerability pattern checking, neural-based loop invariant inference, and the verification of rich properties of real-world smart contracts (ii) a fine-grained model for the Ethereum Virtual Machine (EVM) that provides low-level execution semantics, (iii) an IR-level verification framework integrating both SMT solvers and the Coq proof assistant. We use SciviK to specify and verify security properties for 12 benchmark contracts and a real-world Decentralized Finance (DeFi) smart contract. Among all 158 specified security properties (in six types), 151 properties can be automatically verified within 2 seconds, five properties can be automatically verified after moderate modifications, and two properties are manually proved with around 200 lines of Coq code.