In recent years we have seen a great deal of attention to the topic of security analysis in smart contracts, especially those developed for the Ethereum blockchain. As a result, there seems to be an evergrowing demand for secure smart contracts to protect what could potentially be worth billions. In this paper, we introduce Etherolic as a robust, scalable and efficient fuzzing tool based on concolic testing for performing security analysis on smart contracts. Our approach works based on a successful combination of dynamic taint tracking (DTA) and concolic testing that allows users to analyze the bytecode of smart contracts being run on the Ethereum Virtual Machine. Moreover, Etherolic is not only able to identify a wide spectrum of recent vulnerabilities in smart contracts, but also it generates exploits to trigger unknown errors in the code. In order to demonstrate the usefulness of our approach, we evaluated Etherolic on a crafted benchmark suite, comprising several real-world and synthetic smart contracts along with 98 safety features. The result of our preliminary evaluation reveals 204 security violations in the benchmarks.
Michael Coblenz, Jonathan Aldrich, Brad A. Myers, Joshua Sunshine
Some blockchain programs (smart contracts) have included serious security vulnerabilities. Obsidian is a new typestate-oriented programming language that uses a strong type system to rule out some of these vulnerabilities. Although Obsidian was designed to promote usability to make it as easy as possible to write programs, strong type systems can cause a language to be difficult to use. In particular, ownership, typestate, and assets, which Obsidian uses to provide safety guarantees, have not seen broad adoption together in popular languages and result in significant usability challenges. We performed an empirical study with 20 participants comparing Obsidian to Solidity, which is the language most commonly used for writing smart contracts today. We observed that Obsidian participants were able to successfully complete more of the programming tasks than the Solidity participants. We also found that the Solidity participants commonly inserted asset-related bugs, which Obsidian detects at compile time.
Although blockchain-based smart contracts promise a ``trustless'' way of enforcing agreements even with monetary consequences, they suffer from multiple security issues. Many of these issues could be mitigated via an effective access control system, however, its realization is challenging due to the properties of current blockchain platforms (like lack of privacy, costly on-chain resources, or latency). To address this problem, we propose the SMACS framework, where updatable and sophisticated Access Control Rules (ACRs)} for smart contracts can be realized with low cost. SMACS shifts the burden of expensive ACRs validation and management operations to an off-chain infrastructure, while implementing on-chain only lightweight token-based access control. SMACS is flexible and in addition to simple access control lists can easily implement rules enhancing the runtime security of smart contracts. With dedicated ACRs backed by vulnerability-detection tools, SMACS can protect vulnerable contracts after deployment. We fully implement SMACS and evaluate it.
Vyper has been proposed as a new high-level language for Ethereum smart contract development due to numerous security vulnerabilities and attacks witnessed on contracts written in Solidity since the system's inception. Vyper aims to address these vulnerabilities by providing a language that focuses on simplicity, auditability and security. We present a survey where we study how well-known and commonly-encountered vulnerabilities in Solidity feature in Vyper's development environment. We analyze all such vulnerabilities individually and classify them into five groups based on their status in Vyper. To the best of our knowledge, our survey is the first attempt to study security vulnerabilities in Vyper.
Ningyu He, Ruiyi Zhang, Lei Wu, Haoyu Wang · 8 authors
The EOSIO blockchain, one of the representative Delegated Proof-of-Stake (DPoS) blockchain platforms, has grown rapidly recently. Meanwhile, a number of vulnerabilities and high-profile attacks against top EOSIO DApps and their smart contracts have also been discovered and observed in the wild, resulting in serious financial damages. Most of EOSIO's smart contracts are not open-sourced and they are typically compiled to WebAssembly (Wasm) bytecode, thus making it challenging to analyze and detect the presence of possible vulnerabilities. In this paper, we propose EOSAFE, the first static analysis framework that can be used to automatically detect vulnerabilities in EOSIO smart contracts at the bytecode level. Our framework includes a practical symbolic execution engine for Wasm, a customized library emulator for EOSIO smart contracts, and four heuristics-driven detectors to identify the presence of four most popular vulnerabilities in EOSIO smart contracts. Experiment results suggest that EOSAFE achieves promising results in detecting vulnerabilities, with an F1-measure of 98%. We have applied EOSAFE to all active 53,666 smart contracts in the ecosystem (as of November 15, 2019). Our results show that over 25% of the smart contracts are vulnerable. We further analyze possible exploitation attempts against these vulnerable smart contracts and identify 48 in-the-wild attacks (25 of them have been confirmed by DApp developers), resulting in financial loss of at least 1.7 million USD.
In recent years, smart contracts have suffered major exploits, cost- ing millions of dollars. Unlike traditional programs, smart contracts are deployed on a blockchain. As such, they cannot be modified once deployed. Though various tools have been proposed to detect vulnerable smart contracts, the majority fails to protect vulnera- ble contracts that have already been deployed on the blockchain. Only very few solutions have been proposed so far to tackle the issue of post-deployment. However, these solutions suffer from low precision and are not generic enough to prevent any type of attack. In this work, we introduce ÆGIS, a dynamic analysis tool that protects smart contracts from being exploited during runtime. Its capability of detecting new vulnerabilities can easily be extended through so-called attack patterns. These patterns are written in a domain-specific language that is tailored to the execution model of Ethereum smart contracts. The language enables the description of malicious control and data flows. In addition, we propose a novel mechanism to streamline and speed up the process of managing attack patterns. Patterns are voted upon and stored via a smart contract, thus leveraging the benefits of tamper-resistance and transparency provided by the blockchain. We compare ÆGIS to current state-of-the-art tools and demonstrate that our solution achieves higher precision in detecting attacks. Finally, we perform a large-scale analysis on the first 4.5 million blocks of the Ethereum blockchain, thereby confirming the occurrences of well reported and yet unreported attacks in the wild.
In recent years, smart contracts have suffered major exploits, costing\nmillions of dollars. Unlike traditional programs, smart contracts are deployed\non a blockchain. As such, they cannot be modified once deployed. Though various\ntools have been proposed to detect vulnerable smart contracts, the majority\nfails to protect vulnerable contracts that have already been deployed on the\nblockchain. Only very few solutions have been proposed so far to tackle the\nissue of post-deployment. However, these solutions suffer from low precision\nand are not generic enough to prevent any type of attack.\n In this work, we introduce {\\AE}GIS, a dynamic analysis tool that protects\nsmart contracts from being exploited during runtime. Its capability of\ndetecting new vulnerabilities can easily be extended through so-called attack\npatterns. These patterns are written in a domain-specific language that is\ntailored to the execution model of Ethereum smart contracts. The language\nenables the description of malicious control and data flows. In addition, we\npropose a novel mechanism to streamline and speed up the process of managing\nattack patterns. Patterns are voted upon and stored via a smart contract, thus\nleveraging the benefits of tamper-resistance and transparency provided by the\nblockchain. We compare {\\AE}GIS to current state-of-the-art tools and\ndemonstrate that our solution achieves higher precision in detecting attacks.\nFinally, we perform a large-scale analysis on the first 4.5 million blocks of\nthe Ethereum blockchain, thereby confirming the occurrences of well reported\nand yet unreported attacks in the wild.\n
Peter Robinson, Raghavendra Ramesh, John Brainard, Sandra Johnson
Atomic Crosschain Transaction technology allows composable programming across private Ethereum blockchains. It allows for inter-contract and inter-blockchain function calls that are both synchronous and atomic: if one part fails, the whole call graph of function calls is rolled back. It is not based on existing techniques such as Hash Time Locked Contracts, relay chains, block header transfer, or trusted intermediaries. BLS Threshold Signatures are used to prove to validators on one blockchain that information came from another blockchain and that a majority of the validators of that blockchain agree on the information. Coordination Contracts are used to manage the state of a Crosschain Transaction and as a repository of Blockchain Public Keys. Dynamic code analysis and signed nested transactions are used together with live argument checking to ensure execution only occurs if the execution results in valid state changes. Contract Locking and Lockability enable atomic updates.
Blockchain technology has attracted more and more attention from academia and industry recently. Ethereum, which uses blockchain technology, is a distributed computing platform and operating system. Smart contracts are small programs deployed to the Ethereum blockchain for execution. Errors in smart contracts will lead to huge losses. Formal verification can provide a reliable guarantee for the security of blockchain smart contracts. In this paper, the formal method is applied to inspect the security issues of smart contracts. We summarize five kinds of security issues in smart contracts and present formal verification methods for these issues, thus establishing a formal verification framework that can effectively verify the security vulnerabilities of smart contracts. Furthermore, we present a complete formal verification of the Binance Coin (BNB) contract. It shows how to formally verify the above security issues based on the formal verification framework in a specific smart contract. All the proofs are checked formally using the Coq proof assistant in which contract model and specification are formalized. The formal work of this paper has a variety of essential applications, such as the verification of blockchain smart contracts, program verification, and the formal establishment of mathematical and computer theoretical foundations.
We try to verify properties of the Bitcoin-S library, a Scala implementation of parts of the Bitcoin protocol. We use the Stainless verifier which supports programs in a fragment of Scala called Pure Scala. Since Bitcoin-S is not written in this fragment, we extract the relevant code from it and rewrite it until we arrive at code that we successfully verify. In that process we find and fix two bugs in Bitcoin-S.
Blaž Podgorelec, Marjan Herieko, Muhamed Turkanović
Currently, developers and researchers are dedicated to finding better ways to achieve greater scalability of various blockchain platforms. Focused on the Ethereum blockchain platform, the state channels are currently the only maturely researched and implemented a solution for achieving scalability. However, there are still several problems, such as transparency of state channel networks, transaction traceability, and the incapability that the off-chain state is transferred back on the blockchain network in an ad-hoc manner. To solve the aforementioned problems, we propose a novel state channel solution in the form of a State Channel as a Service, which, although off-chain, still incorporates a secure distributed and decentralized network. This solves the challenge of transparency and traceability while giving users the confidence that only the valid last off-chain state is transferred back on the blockchain network. With the proposed solution, there is no need for users to monitor state channel activities for possible malicious actions. Implementation was performed in the form of a payment channel system, presenting a potential use case for the SCaaS. Furthermore, we performed a security and performance analysis, which shows that the solution is secure and by a factor of 12 more efficient than the classical on-chain payment systems. To evaluate and prove the contributions of the proposed solution, quantitative, and qualitative comparisons with selected related works (i.e., Raiden and Celer) were also performed.
Traditional centralized access control has some shortcomings in robustness, trustworthiness and circulation. Blockchains have the advantages of fault tolerance and trust. Smart contracts have the characteristics of automatic execution and flexible expansion. Tokens can well record credential information and transfer easily. In this paper, blockchain, smart contract and token are integrated and applied to access control to solve the shortcomings of traditional access control. First, access control, blockchain, smart contract and token are briefly described. Second, this paper proposes a solution by giving the general data structure of access control token, elaborating the equivalence, split, merge and verification algorithms of access control token, and explaining the system architecture of token-based access control. Last, this paper uses a token-based access control simulation system to verify that token-based access control has certain comparative advantages in robustness, trustworthiness, circulation, concurrency and so on.
Cryptocurrencies are more than a decade old and several issues have been discovered since their then. One of these issues is a partial negation of the intent to “democratize” money by decentralizing control of the infrastructure that creates, transmits, and stores monetary data. The Programmatic Proof of Work (ProgPoW) algorithm is intended as a possible solution to this problem for the Ethereum cryptocurrency. This paper examines ProgPow’s claim to be Application Specific Integrated Circuit (ASIC) resistant. This is achieved by isolating the proof-of-work code from the Ethereum blockchain, inserting the ProgPoW algorithm, and measuring the performance of the new implementation as a multithread CPU program, as well as a GPU implementation. The most remarkable difference between the ProgPoW algorithm and the currently implemented Ethereum Proof-of Work is the addition of a random sequence of math operations in the main loop that require increased memory bandwidth. Analyzing and comparing the performance of the CPU and GPU implementations should provide an insight into how the ProgPoW algorithm might perform on an ASIC.
The OWASP Top Ten List is a widely-recognized tool for identifying vulnerabilities in web applications. Since blockchain-specific security guidance is currently lacking, mapping existing frameworks, such as OWASP, to the blockchain can help in the identification of potential vulnerabilities in blockchain systems. While the OWASP Top Ten List is designed to describe the vulnerabilities that web application developers face, nine of ten of the OWASP vulnerabilities also apply to blockchain systems. The exception, XML External Entities (XXE), is not applicable due to the lack of use of XML in blockchain.
We study adaptive security of delayed-input Sigma protocols and non-interactive zero-knowledge (NIZK) proof systems in the common reference string (CRS) model. Our contributions are threefold:
We exhibit a generic compiler taking any delayed-input Sigma protocol and returning a delayed-input Sigma protocol satisfying adaptive-input special honest-verifier zero knowledge (SHVZK). In case the initial Sigma protocol also satisfies adaptive-input special soundness, our compiler preserves this property.
We revisit the recent paradigm by Canetti et al. (STOC 2019) for obtaining NIZK proof systems in the CRS model via the Fiat-Shamir transform applied to so-called trapdoor Sigma protocols, in the context of adaptive security. In particular, assuming correlation-intractable hash functions for all sparse relations, we prove that Fiat-Shamir NIZKs satisfy either:
(i)
Adaptive soundness (and non-adaptive zero knowledge), so long as the challenge is obtained by hashing both the prover’s first round and the instance being proven;
(ii)
Adaptive zero knowledge (and non-adaptive soundness), so long as the challenge is obtained by hashing only the prover’s first round, and further assuming that the initial trapdoor Sigma protocol satisfies adaptive-input SHVZK.
We exhibit a generic compiler taking any Sigma protocol and returning a trapdoor Sigma protocol. Unfortunately, this transform does not preserve the delayed-input property of the initial Sigma protocol (if any). To complement this result, we also give yet another compiler taking any delayed-input trapdoor Sigma protocol and returning a delayed-input trapdoor Sigma protocol with adaptive-input SHVZK.
Mikhail Mandrykin, Jake O’Shannessy, Jacob Payne, Ilya Shchepetkov
As smart contracts are growing in size and complexity, it becomes harder and harder to ensure their correctness and security. Due to the lack of isolation mechanisms a single mistake or vulnerability in the code can bring the whole system down, and due to this smart contract upgrades can be especially dangerous. Traditional ways to ensure the security of a smart contract, including DSLs, auditing and static analysis, are used before the code is deployed to the blockchain, and thus offer no protection after the deployment. After each upgrade the whole code need to be verified again, which is a difficult and time-consuming process that is prone to errors. To address these issues a security protocol and framework for smart contracts called Cap9 was developed. It provides developers the ability to perform upgrades in a secure and robust manner, and improves isolation and transparency through the use of a low level capability-based security model. We have used Isabelle/HOL to develop a formal specification of the Cap9 framework and prove its consistency. The paper presents a refinement-based approach that we used to create the specification, as well as discussion of some encountered difficulties during this process.
Many important cryptographic primitives offer probabilistic guarantees of security that can be specified as quantitative hyperproperties; these are specifications that stipulate the existence of a certain number of traces in the system satisfying certain constraints. Verification of such hyperproperties is extremely challenging because they involve simultaneous reasoning about an unbounded number of different traces. In this paper, we introduce a technique for verification of quantitative hyperproperties based on the notion of trace enumeration relations. These relations allow us to reduce the problem of trace-counting into one of model-counting of formulas in first-order logic. We also introduce a set of inference rules for machine-checked reasoning about the number of satisfying solutions to first-order formulas (aka model counting). Putting these two components together enables semi-automated verification of quantitative hyperproperties on infinite state systems. We use our methodology to prove confidentiality of access patterns in Path ORAMs of unbounded size, soundness of a simple interactive zero-knowledge proof protocol as well as other applications of quantitative hyperproperties studied in past work.
Abstract Solidity is the dominant programming language for Ethereum smart contracts. This paper presents a high-level formalization of the Solidity language with a focus on the memory model. The presented formalization covers all features of the language related to managing state and memory. In addition, the formalization we provide is effective: all but few features can be encoded in the quantifier-free fragment of standard SMT theories. This enables precise and efficient reasoning about the state of smart contracts written in Solidity. The formalization is implemented in the SOLC-VERIFY verifier and we provide an extensive set of tests that covers the breadth of the required semantics. We also provide an evaluation on the test set that validates the semantics and shows the novelty of the approach compared to other Solidity-level contract analysis tools.
João Santos Reis, Paul Crocker, Simão Melo de Sousa
This paper introduces Tezla, an intermediate representation of Michelson smart contracts that eases the design of static smart contract analysers. This intermediate representation uses a store and aims to preserve the semantics, flow and resource usage of the original smart contract. This enables properties like gas consumption to be statically verified. We provide an automated decompiler of Michelson smart contracts to Tezla. In order to support our claim about the adequacy of Tezla, we develop a static analyser that takes advantage of the Tezla representation of Michelson smart contracts to prove simple but non-trivial properties.
We study Nakamoto’s Bitcoin protocol that implements a distributed ledger on peer-to-peer asynchronous networks. In particular, we define a principled formal model of key participants - the miners - as stochastic processes and describe the whole system as a parallel composition of miners. We therefore compute the probability that ledgers turn into a state with more severe inconsistencies, e.g. with longer forks, under the assumptions that messages are not lost and nodes are not hostile. We also study how the presence of hostile nodes mining blocks in wrong positions impacts on the consistency of the ledgers. Our theoretical results agree with the simulations performed on a probabilistic model checker that we extended with dynamic datatypes in order to have a faithful description of miners' behaviour.