- Foundations for the Security Analysis of Distributed Blockchain Applications
Author: Clara Schneidewind
Cryptocurrencies do not only allow for money transfers in the absence of a trusted third party but also enable the execution of distributed applications. Due to the rapid pace of development of cryptocurrencies, the foundations of such applications have not been rigorously studied. This is particularly problematic since in these applications, real money is at stake, and security breaches regularly cause severe financial losses.
In this thesis, we present two systematic approaches to reliably verify the security of distributed blockchain applications based on formal foundations. To this end, we focus on the cryptocurrencies with the highest market capitalization, Bitcoin and Ethereum. In Ethereum, distributed applications are realized as smart contracts, reactive programs written in Ethereumâs expressive scripting language. In contrast, Bitcoin supports only a basic scripting language, and advanced applications are realized as peer-to-peer cryptographic protocols that resort to the execution of simple smart contracts in case of disputes among peers. As a result, the challenge in verifying distributed applications on the Ethereum blockchain lies in the study and abstraction of the semantics of Ethereumâs evolved scripting language, whereas Bitcoin, the study of distributed applications, requires a systematic analysis of the cryptographic protocols.
In the thesis, we first formalize the formerly under-specified semantics of Ethereumâs native smart contract language EVM bytecode and implement the semantics in the proof assistant. In this context, we formally characterize relevant generic properties for smart contract security, which capture real-world attack scenarios.
We then survey existing automated static analyzers for Ethereum smart contracts unveiling the weaknesses in the semantic foundations of these tools and the practical impact of these weaknesses on the analysis results. Based on these findings, we propose our own automatic static analysis tool for Ethereum smart contracts, which comes with a rigorous soundness proof while still showing competitive performance. In this course, we also propose a general framework for the modular and semantic-driven development of automatic static analyzers.
Finally, we study the security of payment channel networks for Bitcoin. Payment channel networks are distributed protocols that allow for efficient and cheap payments between Bitcoin users and offer a promising solution to Bitcoinâs scalability problems. We unveil a security issue in Bitcoinâs existing payment channel network implementation and formally characterize the relevant security and privacy notions in this context. We further develop a cryptographic primitive for the construction of payment channel networks with formal security guarantees.
- Summary of: A Federated Society of Bots for Smart Contract Testing
Authors: Emanuele Viglianisi, Mariano Ceccato, and Paolo Tonella
The peculiar novelty of smart contracts is a computational model where irreversible transactions are stored in a distributed persistent data storage, namely the blockchain. The technical nature of this new type of software opens to new kinds of faults, which require specific test capabilities to be revealed. In this paper we present SOCRATES, an extensible and modular framework to automatically test smart contracts. The distinctive features of SOCRATES are: (1) a collection of composable behaviours that exercise smart contracts in the blockchain; (2) it deploys a society of bots, with the purpose of detecting defects arising from multi-user interactions, which are impossible to reveal when deploying a single bot. Our empirical investigation demonstrates that SOCRATES is able expose both known and previously unknown faults in smart contracts that are actively run in the official Ethereum blockchain. Moreover, we show that a society of multiple bots is more efficient in fault exposure than a single bot alone.
- A Formal Specification Smart-Contract Language for Legally Binding Decentralized Autonomous Organizations
Authors: Vimal Dwivedi, Alex Norta, Alexander Wulf, Benjamin Leiding, Sandeep Saxena, and Chibuzor Udokwu
Blockchain- and smart-contract technology enhance the effectiveness and automation of business processes. The rising interest in the development of decentralized autonomous organizations (DAO) shows that blockchain technology has the potential to reform business and society. A DAO is an organization wherein business rules are encoded in smart-contract programs that are executed when specified rules are met. The contractual- and business semantics are sine qua non for drafting a legally-binding smart contract in DAO collaborations. Several smart-contract languages (SCLs) exist, such as SPESC, or Symboleo to specify a legally-binding contract. However, their primary focus is on designing and developing smart contracts with the cooperation of IT- and non-IT users. Therefore, this paper fills a gap in the state of the art by specifying a smart-legal-contract markup language (SLCML) for legal- and business constructs to draft a legally-binding DAO. To achieve the paper objective, we first present a formal SCL ontology to describe the legal- and business semantics of a DAO. Secondly, we translate the SCL ontology into SLCML, for which we present the XML schema definition. We demonstrate and evaluate our SLCML language through the specification of a real life-inspired Sale-of-Goods contract. Finally, the SLCML use-case code is translated into Solidity to demonstrate its feasibility for blockchain platform implementations.
- The Complex Community Structure of the Bitcoin Address Correspondence Network
Authors: Jan Alexander Fischer, Andres Palechor, Daniele DellâAglio, Abraham Bernstein, and Claudio J. Tessone
Bitcoin is built on a blockchain, an immutable decentralised ledger that allows entities (users) to exchange Bitcoins in a pseudonymous manner. Bitcoins are associated with alpha-numeric addresses and are transferred via transactions. Each transaction is composed of a set of input addresses (associated with unspent outputs received from previous transactions) and a set of output addresses (to which Bitcoins are transferred). Despite Bitoin was designed with anonymity in mind, different heuristic approaches exist to detect which addresses in a specific transaction belong to the same entity. By applying these heuristics, we build an Address Correspondence Network: in this representation, addresses are nodes are connected with edges if at least one heuristic detects them as belonging to the same entity. In this paper, we analyse for the first time the Address Correspondence Network and show it is characterised by a complex topology, signalled by a broad, skewed degree distribution and a power-law component size distribution. Using a large-scale dataset of addresses for which the controlling entities are known, we show that a combination of external data coupled with standard community detection algorithms can reliably identify entities. The complex nature of the Address Correspondence Network reveals that usage patterns of individual entities create statistical regularities; and that these regularities can be leveraged to more accurately identify entities and gain a deeper understanding of the Bitcoin economy as a whole.
Link: https://arxiv.org/pdf/2105.09078.pdf
- LNGate: Powering IoT with Next Generation Lightning Micro-payments using Threshold Cryptography
Author: Ahmet Kurt, Suat Mercan, Omer Shlomovits, Enes Erdin, and Kemal Akkaya
Bitcoin has emerged as a revolutionary payment system with its decentralized ledger concept however it has significant problems such as high transaction fees and long confirmation times. Lightning Network (LN), which was introduced much later, solves most of these problems with an innovative concept called off-chain payments. With this advancement, Bitcoin has become an attractive venue to perform micro-payments which can also be adopted in many IoT applications (e.g. toll payments). Nevertheless, it is not feasible to host LN and Bitcoin on IoT devices due to the storage, memory, and processing requirements. Therefore, in this paper, we propose an efficient and secure protocol that enables an IoT device to use LN through an untrusted gateway node. The gateway hosts LN and Bitcoin nodes, and can open & close LN channels, send LN payments on behalf of the IoT device. This delegation approach is powered by a (2,2)-threshold scheme that requires the IoT device and the LN gateway to jointly perform all LN operations which in turn secures both partiesâ funds. Specifically, we propose to thresholdize LNâs Bitcoin public and private keys as well as its commitment points. With these and several other protocol level changes, IoT device is protected against revoked state broadcast, collusion and ransom attacks. We implemented the proposed protocol by changing LNâs source code and thoroughly evaluated its performance using a Raspberry Pi. Our evaluation results show that computational and communication delays associated with the protocol are negligible. To the best of our knowledge, this is the first work that implemented threshold cryptography in LN.
Link: https://arxiv.org/pdf/2105.08902.pdf
- Legendre PRF (Multiple) Key Attacks and the Power of Preprocessing
Authors: Alexander May and Floyd Zweydinger
Due to its amazing speed and multiplicative properties the Legendre PRF recently finds widespread applications e.g. in Ethereum 2.0, multiparty computation and in the quantum-secure signature proposal LegRoast. However, its security is not yet extensively studied.
The Legendre PRF computes for a key k on input x the Legendre symbol Lk(x) = x+k p in some finite field Fp. As standard notion, PRF security is analysed by giving an attacker oracle access to Lk(¡). Khovratovichâs collision-based algorithm recovers k using Lk(¡) in time âp with constant memory. It is a major open problem whether this birthday-bound complexity can be beaten.
We show a somewhat surprising wide-ranging analogy between the discrete logarithm problem and Legendre symbol computations. This analogy allows us to adapt various algorithmic ideas from the discrete logarithm setting.
More precisely, we present a small memory multiplekey attack on m Legendre keys k1, . . . , km in time âmp, i.e. with amortized cost p p/m per key. This multiplekey attack might be of interest in the Ethereum context, since recovering many keys simultaneously maximizes an attackerâs profit.
Moreover, we show that the Legendre PRF admits precomputation attacks, where the precomputation depends on the public p only â and not on a key k. Namely, an attacker may compute e.g. in precomputation time p 2 3 a hint of size p 1 3 . On receiving access to Lk(¡) in an online phase, the attacker then uses the hint to recover the desired key k in time only p 1 3 . Thus, the attackerâs online complexity again beats the birthday-bound.
In addition, our precomputation attack can also be combined with our multiple-key attack. We explicitly give various tradeoffs between precomputation and online phase. E.g. for attacking m keys one may spend time mp 2 3 in the precomputation phase for constructing a hint of size m2 p 1 3 . In an online phase, one then finds all m keys in total time only p 1 3 .
Precomputation attacks might again be interesting in the Ethereum 2.0 context, where keys are frequently changed such that a heavy key-independent precomputation pays off.
Link: https://eprint.iacr.org/2021/645.pdf
- FairMM: A Fast and Frontrunning-Resistant Crypto Market-Maker
Author: Michele Ciampi, Muhammad Ishaq, Malik Magdon-Ismail, Rafail Ostrovsky, and Vassilis Zikas
As new and emerging markets, crypto(-currency/-token) markets are susceptible to manipulation and illiquidity. The theory of market economics, offers market makers that bear the promise of bootstrapping/stabilizing such markets and boosting their liquidity. In order, however, to achieve these goals, the market maker operator (typically an exchange) is assumed trusted against manipulations. Common attempts to remove/weaken this trust assumption require several on-chain rounds per trade or use expensive MPC machinery, and/or are susceptible to manipulative market-maker operators that perform informed front-running attacksâi.e., manipulate the sequence of trades using future trade information. Our work proposes a market-maker-based exchange which is resilient against a wide class of front-running (in particular, reordering attacks). When instantiated with a monopolistic profit seeking market maker our system yields a market where the trading price of crypto-tokens converges to a bid-ask spread centered around their true valuation. Importantly, after an initial setup of appropriate smart contracts, the trades are done in an off-chain fashion and smart contracts are invoked asynchronously to the trades. Our methodology yields a highly efficient exchange, where the market makerâs compliance is ensured by a combination of a rational market analysis, cryptographic mechanisms, and smart-contract-based collaterals. We have implemented our exchange in Ethereum and showcase its competitive throughput, its performance under attack, and the associate gas costs.
Link: https://eprint.iacr.org/2021/609.pdf
- Non-Fungible Token (NFT): Overview, Evaluation, Opportunities and Challenges
Authors: Qin Wang, Rujia Li, Qi Wang, and Shiping Chen
The Non-Fungible Token (NFT) market is mushrooming in the recent couple of years. The concept of NFT originally comes from a token standard of Ethereum, aiming to distinguish each token with distinguishable signs. This type of tokens can be bound with virtual/digital properties as their unique identifications. With NFTs, all marked properties can be freely traded with customized values according to their ages, rarity, liquidity, etc. It has greatly stimulated the prosperity of the decentralized application (DApp) market. At the time of writing (May 2021), the total money used on completed NFT sales has reached 34 , 530 , 649 .86 USD. The thousandfold return on its increasing market draws huge attention worldwide. However, the development of the NFT ecosystem is still in its early stage, and the technologies of NFTs are pre-mature. Newcomers may get lost in their frenetic evolution due to the lack of systematic summaries. In this technical report, we explore the NFT ecosystems in several aspects. We start with an overview of state-of-the-art NFT solutions, then provide their technical components, protocols, standards and desired proprieties. Afterwards, we give a security evolution, with discussions on the perspectives of their design models, opportunities and challenges. To the best of our knowledge, this is the first systematic study on the current NFT ecosystems.
Link: https://arxiv.org/pdf/2105.07447.pdf
- Evaluation of Ethereum End-to-end Transaction Latency
Authors: Lin Zhang, Brian Lee, Yuhang Ye, and Yuansong Qiao
Ethereum is a promising but revolutionary blockchain approach to support rich computational services enabled by Turing-complete instructions, also known as smart contract. Using smart contract as âback-endâ, any party can publish its Decentralized Applications (DApps) available to all Internet users. In other words, blockchain and smart contract enable evolving existing Internet services and applications to decentralised versions. With the developments of versatile Internet applications, the QoS requirements can be very different. For example, new-age applications such as AR/VR can be quite sensitive to even millisecond delays. End-to-end transaction latency in blockchain is a critical factor that affects the performance of DApps. It is the time duration from sending out a transaction (from the client) to having the transaction recorded on the chain. In this paper, we experimentally evaluate the end-to-end latency in Ethereum and discuss the factors that may affect latency on the Ethereum main-net. It has a particular focus on the gas price because it is a key parameter controlled by users. The experiment results demonstrate some counter intuitive finding, e.g. increasing gas price does not reduce the Ethereum end-to-end latency significantly for a certain range of gas prices.
Link: Evaluation of Ethereum End-to-end Transaction Latency | IEEE Conference Publication | IEEE Xplore
- On the Randomness Complexity of Interactive Proofs and Statistical Zero-Knowledge Proofs
Authors: Benny Applebaum and Eyal Golombek
We study the randomness complexity of interactive proofs and zero-knowledge proofs. In particular, we ask whether it is possible to reduce the randomness complexity, R, of the verifier to be comparable with the number of bits, CV , that the verifier sends during the interaction. We show that such randomness sparsification is possible in several settings. Specifically, unconditional sparsification can be obtained in the non-uniform setting (where the verifier is modelled as a circuit), and in the uniform setting where the parties have access to a (reusable) common-random-string (CRS). We further show that constant-round uniform protocols can be sparsified without a CRS under a plausible worst-case complexity-theoretic assumption that was used previously in the context of derandomization.
All the above sparsification results preserve statistical-zero knowledge provided that this property holds against a cheating verifier. We further show that randomness sparsification can be applied to honest-verifier statistical zero-knowledge (HVSZK) proofs at the expense of increasing the communication from the prover by RâF bits, or, in the case of honest-verifier perfect zero-knowledge (HVPZK) by slowing down the simulation by a factor of 2 RâF . Here F is a new measure of accessible bit complexity of an HVZK proof system that ranges from 0 to R, where a maximal grade of R is achieved when zeroknowledge holds against a âsemi-maliciousâ verifier that maliciously selects its random tape and then plays honestly. Consequently, we show that some classical HVSZK proof systems, like the one for the complete Statistical-Distance problem (Sahai and Vadhan, JACM 2003) admit randomness sparsification with no penalty.
Along the way we introduce new notions of pseudorandomness against interactive proof systems, and study their relations to existing notions of pseudorandomness.
Link: https://eprint.iacr.org/2021/605.pdf
- Analysis of Bitcoin Vulnerability to Bribery Attacks Launched Through Large Transactions
Authors: Ghader Ebrahimpour and Mohammad Sayad Haghighi
Bitcoin uses blockchain technology to maintain transactions order and provides probabilistic guarantee to prevent double-spending, assuming that an attackerâs computational power does not exceed %50 of the network power. In this paper, we design a novel bribery attack and show that this guarantee can be hugely undermined. Miners are assumed to be rational in this setup and they are given incentives that are dynamically calculated. In this attack, the adversary misuses the Bitcoin protocol to bribe miners and maximize their gained advantage. We will reformulate the bribery attack to propose a general mathematical foundation upon which we build multiple strategies. We show that, unlike Whale Attack, these strategies are practical. If the rationality assumption holds, this shows how vulnerable blockchain-based systems like Bitcoin are. We suggest a soft fork on Bitcoin to fix this issue at the end.
Link: https://arxiv.org/pdf/2105.07501.pdf
- Towards A First Step to Understand Flash Loan and Its Applications in DeFi Ecosystem
Authors: Dabao Wang, Siwei Wu, Ziling Lin, Lei Wu, Xingliang Yuan, Yajin Zhou, Haoyu Wang, and Kui Ren
Flash Loan, as an emerging service in the decentralized finance ecosystem, allows users to request a non-collateral loan. While providing convenience, it also enables attackers to launch malicious operations with a large amount of asset that they do not have. Though there exist spot media reports of attacks that leverage Flash Loan, there lacks a comprehensive understanding of existing Flash Loan services.
In this work, we take the first step to study the Flash Loan service provided by three popular platforms. Specifically, we first illustrate the interactions between Flash Loan providers and users. Then, we design three patterns to identify Flash Loan transactions. Based on the patterns, 76, 303 transactions are determined. The evaluation results show that the Flash Loan services get more popular over time. At last, we present four Flash Loan applications with real-world examples and propose two potential research directions.