Blockchain systems, such as Ethereum, use an approach called "metering" to assign a cost to smart contract execution, an approach which is designed to incentivise miners to operate the network and protect it against DoS attacks. In the past, the imperfections of Ethereum metering allowed several DoS attacks which were countered through modification of the metering mechanism. This paper presents a new DoS attack on Ethereum which systematically exploits its metering mechanism. We first replay and analyse several months of transactions, during which we discover a number of discrepancies in the metering model, such as significant inconsistencies in the pricing of the instructions. We further demonstrate that there is very little correlation between the execution cost and the utilised resources, such as CPU and memory. Based on these observations, we present a new type of DoS attack we call Resource Exhaustion Attack, which uses these imperfections to generate low-throughput contracts. To do this, we design a genetic algorithm that generates contracts with a throughput on average 200 times slower than typical contracts. We then show that all major Ethereum client implementations are vulnerable and, if running on commodity hardware, would be unable to stay in sync with the network when under attack. We argue that such an attack could be financially attractive not only for Ethereum competitors and speculators, but also for Ethereum miners. Finally, we discuss short-term and potential long-term fixes against such attacks. Our attack has been responsibly disclosed to the Ethereum Foundation and awarded a bug bounty reward of 5,000 USD.
Haijun Wang, Ye Liu, Yi Li, Shang‐Wei Lin · 7 authors
Despite the high stakes involved in smart contracts, they are often developed in an undisciplined manner, leaving the security and reliability of blockchain transactions at risk. In this article, we introduce ContraMaster—an oracle-supported dynamic exploit generation framework for smart contracts. Existing approaches mutate only single transactions; ContraMaster exceeds these by mutating the transaction sequences. ContraMaster uses data-flow, control-flow, and the dynamic contract state to guide its mutations. It then monitors the executions of target contract programs, and validates the results against a general-purpose semantic test oracle to discover vulnerabilities. Being a dynamic technique, it guarantees that each discovered vulnerability is a violation of the test oracle and is able to generate the attack script to exploit this vulnerability. In contrast to rule-based approaches, ContraMaster has not shown any false positives, and it easily generalizes to unknown types of vulnerabilities (e.g., logic errors). We evaluate ContraMaster on 218 vulnerable smart contracts. The experimental results confirm its practical applicability and advantages over the state-of-the-art techniques, and also reveal three new types of attacks.
Fan Zhang, Deepak Maram, Harjasleen Malvai, Steven Goldfeder · 5 authors
Thanks to the widespread deployment of TLS, users can access private data over channels with end-to-end confidentiality and integrity. What they cannot do, however, is prove to third parties the {\em provenance} of such data, i.e., that it genuinely came from a particular website. Existing approaches either introduce undesirable trust assumptions or require server-side modifications. As a result, the value of users' private data is locked up in its point of origin. Users cannot export their data with preserved integrity to other applications without help and permission from the current data holder. We propose DECO (short for \underline{dec}entralized \underline{o}racle) to address the above problems. DECO allows users to prove that a piece of data accessed via TLS came from a particular website and optionally prove statements about such data in zero-knowledge, keeping the data itself secret. DECO is the first such system that works without trusted hardware or server-side modifications. DECO can liberate data from centralized web-service silos, making it accessible to a rich spectrum of applications. To demonstrate the power of DECO, we implement three applications that are hard to achieve without it: a private financial instrument using smart contracts, converting legacy credentials to anonymous credentials, and verifiable claims against price discrimination.
U radu je opisana, implementirana i ispitana metoda authentikacije temeljena na neinteraktivnim dokazima bez poznavanja. Takva metoda omogućuje primatelju da authenticira pošiljatelja i izračuna dijeljeni ključ. Način razmjene odnosno računanja zajedničkog ključa inspiriran je Diffie-Hellman protokolom. Metoda je implementirana u C++ programskom jeziku te ispitana na prijenosnom računalu i Raspberry Pi-u. Ispitana je i uspoređena brzina authentikacije. U odnosu na srodne authentikacijske sheme, postignute su usporedive brzine uz usporedivu razinu sigurnosti.
In the context of Intelligent Transportation System (ITS), smart vehicles have become increasingly complex. Electronic Control Units (ECU) within smart vehicles are now capable of performing intricate operations which ensures reliable functioning of the smart vehicle even in emergency situations. However, these ECU(s) lack a trusted execution/storage environment (TEE/TSE). This makes it vulnerable to many security issues. In this paper, we propose a Blockchain and Secure Element(SE) based framework for smart vehicles called SaFe in which ECU(s) use SE for TEE and TSE. We justify the use of blockchain by showing how it securely facilitates application management on SE when ECU needs are changed. Leveraging on SaFe, we introduce the concept of non-repudiable responsibility. We present our realized framework and testbed based on NXP IMX6Q, Multos M5-P19, MultiChain. Finally, we show through our experimental results that how SaFe improves the performance of safety-critical operations within ECU by as much as 85%, all this while guaranteeing increased security, tamperproofness, immutability and reduced memory, storage, processing overhead.
Background: Millions of smart contracts have been deployed to Ethereum for providing various applications. Recent studies discovered many severe security and performance issues in smart contracts by applying static program analysis techniques to them. Given a smart contract, the majority of these analysis techniques need to first construct its control flow graph, which connects basic blocks through control flow transfers (CFTs), before conducting further analysis. Aims: The objective of this work is to understand the capabilities of static program analysis techniques to identify CFTs, and to investigate how static program analysis techniques can be improved if the CFTs are complemented. Method: We perform a comprehensive empirical study on six widely-used tools for smart contract analysis by using all deployed smart contracts to understand their capabilities to recognize CFTs. We capture all execution traces of all smart contracts to evaluate the number of CFTs covered by traces that are not found by those tools. We enhance a state-of-the-art tool, OYENTE for discovering vulnerabilities in smart contracts with the CFTs covered by traces to investigate how the tool is improved. Results: These studied tools fail to identify all CFTs due to several reasons, e.g., incomplete code patterns. Execution traces effectively complement these tool in recognizing CFTs. By including the CFTs covered by traces, the false negative rate of OYENTE can be reduced by up to 30%. Conclusions: Our study underlines the ineffectiveness of static analysis techniques due to the incapabilities of CFT identification.
Quan Nguyen, André Cronje, Michael Kong, Alex Kampa · 5 authors
This paper introduces a new consensus protocol, so-called \emph{\stair}, for fast consensus in DAG-based trustless system. In \stair, we propose a new approach to creating local block DAG, namely \emph{x-DAG} (cross-DAG), on each node. \emph{\stair} protocol is based on our Proof-of-Stake StakeDag framework \cite{stakedag} that distinguishes participants into users and validators by their stake. Both users and validators can create and validate event blocks. Unlike StakeDag's DAG, x-DAG ensures that each new block has to have parent blocks from both Users and Validators to achieve more safety and liveness. Our protocol leverages a pool of validators to expose more validating power to new blocks for faster consensus in a leaderless asynchronous system. Further, our framework allows participants to join as observers / monitors, who can retrieve DAG for post-validation, but do not participate in onchain validation.
Sunbeom So, Myungho Lee, Jisu Park, Heejo Lee · 5 authors
We present VERISMART, a highly precise verifier for ensuring arithmetic safety of Ethereum smart contracts. Writing safe smart contracts without unintended behavior is critically important because smart contracts are immutable and even a single flaw can cause huge financial damage. In particular, ensuring that arithmetic operations are safe is one of the most important and common security concerns of Ethereum smart contracts nowadays. In response, several safety analyzers have been proposed over the past few years, but state-of-the-art is still unsatisfactory; no existing tools achieve high precision and recall at the same time, inherently limited to producing annoying false alarms or missing critical bugs. By contrast, VERISMART aims for an uncompromising analyzer that performs exhaustive verification without compromising precision or scalability, thereby greatly reducing the burden of manually checking undiscovered or incorrectly-reported issues. To achieve this goal, we present a new domain-specific algorithm for verifying smart contracts, which is able to automatically discover and leverage transaction invariants that are essential for precisely analyzing smart contracts. Evaluation with real-world smart contracts shows that VERISMART can detect all arithmetic bugs with a negligible number of false alarms, far outperforming existing analyzers.
Ning Lu, Bin Wang, Yongxin Zhang, Wenbo Shi · 5 authors
Summary Ethereum is one of the currently popular trading platform, where any one can exchange, buy, or sell cryptocurrencies. Smart contract, a computer program, can help Ethereum to encode rules or scripts for processing transactions. Because the smart contract usually handles large number of cryptocurrencies worth billions of dollars apiece, its security has gained considerable attention. In this paper, we first investigate the security of smart contracts running on the Ethereum and introduce several new security vulnerabilities that allow adversaries to exploit and gain financial benefits. Then, we propose a more practical smart contract analysis tool termed NeuCheck, in which we introduce the syntax tree in the syntactical analyzer to complete the transformation from source code to intermediate representation, and then adopt the open source library working with XML to analyze such tree. We have built a prototype of NeuCheck for Ethereum and evaluate it with over 52 000 existing Ethereum smart contracts. The results show that (1) our new documented vulnerabilities are prevalent; (2) NeuCheck improves the analysis speed by at least 17.2 times compared to other popular analysis tools (eg, Securify and Mythril; and (3) allows for cross‐platform deployment.
Purathani Praitheeshan, Lei Pan, Jiangshan Yu, Joseph K. Liu · 5 authors
Smart contracts are software programs featuring both traditional applications\nand distributed data storage on blockchains. Ethereum is a prominent blockchain\nplatform with the support of smart contracts. The smart contracts act as\nautonomous agents in critical decentralized applications and hold a significant\namount of cryptocurrency to perform trusted transactions and agreements.\nMillions of dollars as part of the assets held by the smart contracts were\nstolen or frozen through the notorious attacks just between 2016 and 2018, such\nas the DAO attack, Parity Multi-Sig Wallet attack, and the integer\nunderflow/overflow attacks. These attacks were caused by a combination of\ntechnical flaws in designing and implementing software codes. However, many\nmore vulnerabilities of less severity are to be discovered because of the\nscripting natures of the Solidity language and the non-updateable feature of\nblockchains. Hence, we surveyed 16 security vulnerabilities in smart contract\nprograms, and some vulnerabilities do not have a proper solution. This survey\naims to identify the key vulnerabilities in smart contracts on Ethereum in the\nperspectives of their internal mechanisms and software security\nvulnerabilities. By correlating 16 Ethereum vulnerabilities and 19 software\nsecurity issues, we predict that many attacks are yet to be exploited. And we\nhave explored many software tools to detect the security vulnerabilities of\nsmart contracts in terms of static analysis, dynamic analysis, and formal\nverification. This survey presents the security problems in smart contracts\ntogether with the available analysis tools and the detection methods. We also\ninvestigated the limitations of the tools or analysis methods with respect to\nthe identified security vulnerabilities of the smart contracts.\n
Aug 9, 2019·Proceedings of the 2019 27th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering
Ethereum Virtual Machine (EVM) is the run-time environment for smart contracts and its vulnerabilities may lead to serious problems to the Ethereum ecology. With lots of techniques being continuously developed for the validation of smart contracts, the testing of EVM remains challenging because of the special test input format and the absence of oracles. In this paper, we propose EVMFuzzer, the first tool that uses differential fuzzing technique to detect vulnerabilities of EVM. The core idea is to continuously generate seed contracts and feed them to the target EVM and the benchmark EVMs, so as to find as many inconsistencies among execution results as possible, eventually discover vulnerabilities with output cross-referencing. Given a target EVM and its APIs, EVMFuzzer generates seed contracts via a set of predefined mutators, and then employs dynamic priority scheduling algorithm to guide seed contracts selection and maximize the inconsistency. Finally, EVMFuzzer leverages benchmark EVMs as cross-referencing oracles to avoid manual checking. With EVMFuzzer, we have found several previously unknown security bugs in four widely used EVMs, and 5 of which had been included in Common Vulnerabilities and Exposures (CVE) IDs in U.S. National Vulnerability Database. The video is presented at https://youtu.be/9Lejgf2GSOk.
Gustavo Betarte, Maximiliano Cristiá, Carlos Luna, Adrián Silveira · 5 authors
Emin Gün Sirer once said: It's clear that writing a robust, secure smart contract requires extreme amounts of diligence. It's more similar to writing code for a nuclear power reactor, than to writing loose web code [...] Yet the current Solidity language and underlying EVM seems designed more for the latter. Formal methods (FM) are mathematics-based software development methods aimed at producing "code for a nuclear power reactor". That is, due application of FM can produce bug-free, zero-defect, correct-by-construction, guaranteed, certified software. However, the software industry seldom use FM. One of the main reasons for such a situation is that there exists the perception (which might well be a fact) that FM increase software costs. On the other hand, FM can be partially applied thus producing high-quality software, although not necessarily bug-free. In this paper we outline some FM related techniques whose application the cryptocurrency community should take into consideration because they could bridge the gap between "loose web code" and "code for a nuclear power reactor".
Emmanuelle Anceaume, Marina Papatriantafilou, Maria Potop-Butucaru, Philippas Tsigas
This paper continues the recent line of academic effort dedicated to formalizing distributed ledgers. This work is the first one to propose a specification of distributed ledger register that matches the Lamport hierarchy from safe to atomic. Moreover, we propose implementations of distributed ledger registers with safe, regular and atomic guaranties in a model of communication specific to distributed ledgers technology that we also formalize. Then, we propose an implementation of a distributed ledger register that satisfies the atomic specification and the k-consistency property that characterises the permissionless distributed blockchains such as Bitcoin and Ethereum.
Bitcoin paper, published under a pseudonym Satoshi Nakamoto, opened a new era; cryptocurrencies, blockchain and distributed ledger technologies that are aiming distributed trust model. Even if there has been an ongoing extensive discussion both on the origin and the future about these developing technologies, number of products, studies and projects are increasing day by day. Among these the most crucial one is crypto wallets since the distributed trust and privacy preserving solutions are all relies on the underlying cryptographic primitives and the corresponding cryptographic keys. Almost all the cryptocurrencies require their users individually manage their own cryptographic keys or recommend use of cryptocurrency wallets. A cryptocurrency wallet or shortly, crypto wallet, has to generate and store one or more public-private keys and corresponding addresses. These keys authenticate corresponding transactions, hence any adversary who gains access to a wallet may seize all the assets secured with them. Therefore, cryptocurrency wallet solutions and products should be carefully analyzed and better to be certified if possible from the very beginning. \nIn this thesis, we mainly focus on to what extend and how a cryptocurrency wallet’s security analysis should be pursued. In order to formally portray the analysis framework, we propose to follow the Common Criteria (CC) Evaluation framework. CC evaluation framework is a formal evaluation methodology. For this purpose, assumptions, risks, threatsandsecurityvulnerabilitiesofthewalletswillbedefined. Also,objectivesshowing howthesethreatswillbecounteredinsidethewalletandwhatkindofmeasuresshouldbe taken by the environment and users will be detailed. In order to understand the security requirements, blockchain technology and Bitcoin which is the leading cryptocurrency will be explained and cryptocurrency wallets will be classified. In addition, we are going to propose a secure hardware wallet design in terms of physical and logical requirements. Then, we will compare the proposed wallet with other hardware wallets on the market. WebelievethatthisthesismaybebasicresourceforcreatingstandardizedCCdocuments such as Protection Profile(PP), Security Target(ST) etc. Furthermore, this study would be a brief source for cryptocurrency wallets’ design, test and analysis phases.
Musab A. Alturki, Jing Chen, Victor Luchangco, Brandon Moore · 7 authors
The Algorand blockchain is a secure and decentralized public ledger based on pure proof of stake rather than proof of work. At its core it is a novel consensus protocol with exactly one block certified in each round: that is, the protocol guarantees that the blockchain does not fork. In this paper, we report on our effort to model and formally verify the Algorand consensus protocol in the Coq proof assistant. Similar to previous consensus protocol verification efforts, we model the protocol as a state transition system and reason over reachable global states. However, in contrast to previous work, our model explicitly incorporates timing issues (e.g., timeouts and network delays) and adversarial actions, reflecting a more realistic environment faced by a public blockchain. Thus far, we have proved asynchronous safety of the protocol: two different blocks cannot be certified in the same round, even when the adversary has complete control of message delivery in the network. We believe that our model is sufficiently general and other relevant properties of the protocol such as liveness can be proved for the same model.
We present solc-verify, a source-level verification tool for Ethereum smart contracts. Solc-verify takes smart contracts written in Solidity and discharges verification conditions using modular program analysis and SMT solvers. Built on top of the Solidity compiler, solc-verify reasons at the level of the contract source code, as opposed to the more common approaches that operate at the level of Ethereum bytecode. This enables solc-verify to effectively reason about high-level contract properties while modeling low-level language semantics precisely. The contract properties, such as contract invariants, loop invariants, and function pre- and post-conditions, can be provided as annotations in the code by the developer. This enables automated, yet user-friendly formal verification for smart contracts. We demonstrate solc-verify by examining real-world examples where our tool can effectively find bugs and prove correctness of non-trivial properties with minimal user effort.
EOSIO is a blockchain platform utilizing a byzantine-fault-tolerance delegated-proof-of-stake (BFT-DPOS) consensus protocol to guarantee scalability. In EOSIO, a group of representatives called block producers (BPs) is elected by voting through a certain period, and is scheduled in an order to produce blocks. And new tokens are given to BPs every time they produce a block as a notion of reward. In this paper, we show that an attacker can disturb fairness of compensation policy by manipulating the production schedule of EOSIO. Such manipulation is possible through an attacker who has enough tokens to abuse the election process. In order to demonstrate the feasibility and the capability of our attack, we created a tool following EOSIO's voting and irreversible block generation procedure. Our simulation shows that an attacker can provide additional rewards or loss up to 3 BPs. Finally, we discuss the applicability of our attack against the real EOSIO mainnet, and at the same time, propose some countermeasures to prevent it.
Michael N. Jones, Matthew Johnson, Mark Shervey, Joel T. Dudley · 5 authors
BACKGROUND: The protection of private data is a key responsibility for research studies that collect identifiable information from study participants. Limiting the scope of data collection and preventing secondary use of the data are effective strategies for managing these risks. An ideal framework for data collection would incorporate feature engineering, a process where secondary features are derived from sensitive raw data in a secure environment without a trusted third party. OBJECTIVE: This study aimed to compare current approaches based on how they maintain data privacy and the practicality of their implementations. These approaches include traditional approaches that rely on trusted third parties, and cryptographic, secure hardware, and blockchain-based techniques. METHODS: A set of properties were defined for evaluating each approach. A qualitative comparison was presented based on these properties. The evaluation of each approach was framed with a use case of sharing geolocation data for biomedical research. RESULTS: We found that approaches that rely on a trusted third party for preserving participant privacy do not provide sufficiently strong guarantees that sensitive data will not be exposed in modern data ecosystems. Cryptographic techniques incorporate strong privacy-preserving paradigms but are appropriate only for select use cases or are currently limited because of computational complexity. Blockchain smart contracts alone are insufficient to provide data privacy because transactional data are public. Trusted execution environments (TEEs) may have hardware vulnerabilities and lack visibility into how data are processed. Hybrid approaches combining blockchain and cryptographic techniques or blockchain and TEEs provide promising frameworks for privacy preservation. For reference, we provide a software implementation where users can privately share features of their geolocation data using the hybrid approach combining blockchain with TEEs as a supplement. CONCLUSIONS: Blockchain technology and smart contracts enable the development of new privacy-preserving feature engineering methods by obviating dependence on trusted parties and providing immutable, auditable data processing workflows. The overlap between blockchain and cryptographic techniques or blockchain and secure hardware technologies are promising fields for addressing important data privacy needs. Hybrid blockchain and TEE frameworks currently provide practical tools for implementing experimental privacy-preserving applications.
When a Solidity smart contract has a problem in calling a function of another contract, the "fallback function" of the contract is supposed to be executed automatically. However, in many cases, a fallback function is arbitrarily created and called, with their behaviors unknown to developers, so that its execution is vulnerable to exploits by attackers. To reduce these risks, this paper proposes a method that provides developers with new keywords by modifying existing Solidity compiler and Ethereum Virtual Machine (EVM). Developers mark their intention using the newly introduced keywords, and the modified existing Solidity compiler and EVM uses flags and conditional statements to prevent calls of fallback functions to reduce the risk of calls to fallback functions.
In this paper we give an overview of the Blockchain. We explain quickly how it works thanks to the hash function and the distributed architecture. Then come the descriptions of the two most famous consensus algorithms: Proof of Work and Proof of Stake. We also present some security issues for each algorithm. This paper contains a little explanation of others consensus algorithms that are inspired of these two. Finally, a new consensus algorithm for private Blockchain is presented.
Gabor Madl, Luis Angel D. Bathen, German Flores, Divyesh Jadav
Emerging distributed ledger technologies - also known as blockchains - have recently become a hot research topic across a wide variety of industries due to their immutability, availability, security, and more importantly, their ability to execute multi-party agreements or business rules in the form of smart contracts. Smart contracts provide the means to automate and enforce contractual terms between the parties entering the agreement. It is important to guarantee the correctness of such contracts in order to avoid catastrophic events that may require human intervention. This paper presents a method that builds on the interface automata model of computation as a semantic domain to formalize smart contracts. The formal model of computation assigns a precise and unambiguous meaning to smart contracts. Loyalty points are discounts and bonuses provided by companies with the purpose of retaining their loyal customers. The proposed method is evaluated in the context of a loyalty points marketplace. The decentralized, distributed and immutable nature of blockchain provides an appealing platform for the implementation of a loyalty points marketplace, and the formal semantics based on interface automata ensure that violations of the agreement can be detected, and contractual clauses can be enforced by all parties involved in loyalty points transactions.
Patrick L. Chapman, Dianxiang Xu, Lin Deng, Yin Xiong
Blockchain in recent years has exploded in popularity with Ethereum being one of the leading blockchain platforms. Solidity is a widely used scripting language for creating smart contracts in Ethereum applications. Quality assurance in Solidity contracts is of critical importance because bugs or vulnerabilities can lead to a considerable loss of financial assets. However, it is unclear what level of quality assurance is provided in many of these applications. Mutation testing is the process of intentionally injecting faults into a target program and then running the provided test suite against the various injected faults. Mutation testing is used to evaluate the effectiveness of a test suite, measuring the test suite’s capability of covering certain types of faults. This thesis presents Deviant, the first implementation of a mutation testing tool for Solidity smart contracts. Deviant implements mutation operators that cover the unique features of Solidity according to our constructed fault model, in addition to traditional mutation operators that exist for other programming languages. Deviant has been applied to five open-source Solidity projects: MetaCoin [30], MultiSigWallet [31], Alice [29], aragonOS [32], and OpenZeppelin [33]. Experimental results show that the provided test suites result in low mutation scores. These results indicate that the provided tests cannot ensure high-level assurance of code quality. Such evaluation results offer important guidelines for Solidity developers to implement more effective tests in order to deliver trustworthy code and reduce the risk of financial loss.
Gbadebo Ayoade, Erick Bauman, Latifur Khan, Kevin W. Hamlen
An Ethereum bytecode rewriting and validation architecture is proposed and evaluated for securing smart contracts in decentralized cryptocurrency systems without access to contract source code. This addresses a wave of smart contract vulnerabilities that have been exploited by cybercriminals in recent years to steal millions of dollars from victims. Such attacks have motivated various best practices proposals for helping developers write safer contracts; but as the number of programming languages used to develop smart contracts increases, implementing these best practices can be cumbersome and hard to enforce across the development tool chain. Automated hardening at the bytecode level bypasses this source-level heterogeneity to enforce safety and code integrity properties of contracts independently of the sources whence they were derived. In addition, a binary code verification tool implemented atop the Coq interactive theorem prover establishes input-output equivalence between the original code and the modified code. Evaluation demonstrates that the system can enforce policies that protect against integer overflow and underflow vulnerabilities in real Ethereum contract bytecode, and overhead is measured in terms of instruction counts.