Eder J. Scheid, Manuel Keller, Muriel Figueredo Franco, Burkhard Stiller
Current projects applying blockchain technology to enhance the trust of NFV environments do not consider the VNF repository. However, the blockchain’s properties can enhance trust by allowing to verify a VNF package’s integrity without relying (a) on a Trusted Third Party (TTP) for remote attestation or (b) a secure database. This paper presents BUNKER , a Blockchain-based trUsted VNF packagE Repository, intended to be integrated with traditional database-based package verification environments, acting as a trusted repository containing VNF package information. Moreover, BUNKER allows users to acquire VNFs without the need of a TTP using an Ethereum Smart Contract (SC). The SC automatically transfers license fees to the vendor once a VNF is acquired, and sends the VNF package’s link to the buyer before verifying its integrity.
Among the zero-knowledge succinct non-interactive arguments of knowledge (zk-SNARK), the simulation-extractable zk-SNARK (SE-SNARK) introduces a security notion of non-malleability. The existing pairing-based zk-SNARKs designed from linear encoding are known to be vulnerable to algebraic manipulation of the proof. The latest SE-SNARKs check the proof consistency by increasing the proof size and the verification cost. In particular, the number of pairings increases almost doubles due to further verification. In this article, we propose two novel SE-SNARK constructions with a single verification. The consistency check is subsumed in a single verification through employing a hash function. The proof size and verification time of the proposed SE-SNARK schemes are minimal in that it is the same as the state-of-the-art zk-SNARK without non-malleability. The proof in our SE-SNARK constructions comprises only three group elements (type III) in the QAP-based scheme and two group elements (type I) in the SAP-based scheme. The verification time in both requires only 3 pairings. The soundness of the proposed schemes is proven under the hash-algebraic knowledge (HAK) assumption and the (linear) collision-resistant hash assumption.
Ethereum smart contracts are executable programs, deployed on a peer-to-peer network and executed in a consensus-based fashion. Their bytecode is public, immutable and once deployed to the blockchain, cannot be patched anymore. As smart contracts may hold Ether worth of several million dollars, they are attractive targets for attackers and indeed some contracts have successfully been exploited in the recent past, resulting in tremendous financial losses. The correctness of smart contracts is thus of utmost importance. While first approaches on formal verification exist, they demand users to be well-versed in formal methods which are alien to many developers and are only able to analyze individual contracts, without considering their execution environment, i.e., calls to external contracts, sequences of transaction, and values from the actual blockchain storage. In this paper, we present Annotary, a concolic execution framework to analyze smart contracts for vulnerabilities, supported by annotations which developers write directly in the Solidity source code. In contrast to existing work, Annotary supports analysis of inter-transactional, inter-contract control flows and combines symbolic execution of EVM bytecode with a resolution of concrete values from the public Ethereum blockchain. While the analysis of Annotary tends to weight precision higher than soundness, we analyze inter-transactional call chains to eliminate false positives from unreachable states that traditional symbolic execution would not be able to handle. We present the annotation and analysis concepts of Annotary, explain its implementation on top of the Laser symbolic virtual machine, and demonstrate its usage as a plugin for the Sublime Text editor.
Rewriting-history attacks can erase all valid records of blockchain-based systems, which is extremely devastating. To deter such attacks, we design a new smart contract-based secure model to make such attacks ineffective. Each node who creates a new block is required to register with the smart contract to get a voucher required for the subsequent block validation. We introduce the design idea and the structure of the proposed model in detail. We also present the algorithms of the smart contract and analyze the security performance of the proposed model in different cases. To prove the feasibility of the proposed model, we use the Solidity language to implement the smart contract in this model and simulate it on the Ethereum test network. We also show simulation results in terms of runtime and resource consumption.
Block-chain world is very dynamic and there is need for strong governance and underlying technology architecture to be robust to face challenges. This paper considers Ethereum, a leading block chain. We deep dive into the nature of this block chain, wherein for software upgrades forks are performed. They types of forks and impact is discussed. A specific Ethereum hack led to a hard fork and focus is provided on understanding the hack and overcoming it from a novel approach. The current model has been unable to handle multiple Ethereum attacks. Thus the current approach is compared against a novel approach providing a security and scaling solution. Here the architecture draws upon combining block-chain layers into operating system level. The approach can have tremendous benefits to block chain world and improve the way decentralized application teams perform. The benefits of the novel architecture is discussed. The approach helps safe guard block chain projects, making them safer and chain agnostic.
The Fiat-Shamir (FS) transform is a well known and widely used technique to convert any constant-round public-coin honest-verifier zero-knowledge (HVZK) proof or argument system \(\mathsf {HVZK}=(\mathcal {P},\mathcal {V})\) in a non-interactive zero-knowledge (NIZK) argument system
Current architectures to validate, certify, and manage identity are based on centralised, top-down approaches that rely on trusted authorities and third-party operators. We approach the problem of digital identity starting from a human rights perspective, with a primary focus on identity systems in the developed world. We assert that individual persons must be allowed to manage their personal information in a multitude of different ways in different contexts and that to do so, each individual must be able to create multiple unrelated identities. Therefore, we first define a set of fundamental constraints that digital identity systems must satisfy to preserve and promote privacy as required for individual autonomy. With these constraints in mind, we then propose a decentralised, standards-based approach, using a combination of distributed ledger technology and thoughtful regulation, to facilitate many-to-many relationships among providers of key services. Our proposal for digital identity differs from others in its approach to trust in that we do not seek to bind credentials to each other or to a mutually trusted authority to achieve strong non-transferability. Because the system does not implicitly encourage its users to maintain a single aggregated identity that can potentially be constrained or reconstructed against their interests, individuals and organisations are free to embrace the system and share in its benefits.
The adoption of blockchain based distributed ledgers is growing fast due to their ability to provide reliability, integrity, and auditability without trusted entities. One of the key capabilities of these emerging platforms is the ability to create self-enforcing smart contracts. However, the development of smart contracts has proven to be error-prone in practice, and as a result, contracts deployed on public platforms are often riddled with security vulnerabilities. This issue is exacerbated by the design of these platforms, which forbids updating contract code and rolling back malicious transactions. In light of this, it is crucial to ensure that a smart contract is secure before deploying it and trusting it with significant amounts of cryptocurrency. To this end, we introduce the VeriSolid framework for the formal verification of contracts that are specified using a transition-system based model with rigorous operational semantics. Our model-based approach allows developers to reason about and verify contract behavior at a high level of abstraction. VeriSolid allows the generation of Solidity code from the verified models, which enables the correct-by-design development of smart contracts.
The second generation of blockchain represented by smart contracts has been developing vigorously in recent years. However, frequent smart contract vulnerability incidents pose a serious risk to blockchain ecosystem security. Since current symbol execution tools often fall into path explosion and thus lead to inefficient detection, this paper expands Mythril's framework to optimize its performance. Firstly, it finds out potential vulnerable code regions using static analysis and identifies critical paths that may have security defects. Then, aiming at the problem that traditional search algorithms cannot actively locate and explore critical paths, this paper presents a multi-objective oriented path search (MOPS) strategy based on path priority. This strategy guides dynamic symbolic execution to cover critical paths quickly, avoiding blind traversal of program execution paths. Finally, it describes security rules and proposes corresponding detection logics for different vulnerability categories. This paper analyzes over 1000 smart contracts extracted from Etherscan. Compared with existing tools based on symbolic execution, the proposed method can reduce time consumption by around 35% while ensuring the accuracy of vulnerability detection. Moreover, existing tools often issue warnings that do not actually cause financial losses. But the proposed method only concentrates on code regions related to transfer of funds, so it can reduce the false alarm rate to some extent.
Ethereum smart contracts are programs that can be collectively executed by a network of mutually untrusted nodes. Smart contracts handle and transfer assets of values, offering strong incentives for malicious attacks. Intrusion attacks are a popular type of malicious attacks. In this article, we propose ContractGuard, the first intrusion detection system (IDS) to defend Ethereum smart contracts against such attacks. Like IDSs for conventional programs, ContractGuard detects intrusion attempts as abnormal control flow. However, existing IDS techniques/tools are inapplicable to Ethereum smart contracts due to Ethereum's decentralized nature and its highly restrictive execution environment. To address these issues, we design ContractGuard by embedding it in the contracts to profile context-tagged acyclic paths, and optimizing it under the Ethereum gas-oriented performance model. The main goal is to minimize the overheads, to which the users will be extremely sensitive since the cost needs to be paid upfront in digital concurrency. Empirical investigation using real-life contracts deployed in the Ethereum mainnet shows that on average, ContractGuard only adds to 36.14 percent of the deployment overhead and 28.27 percent of the runtime overhead. Furthermore, we conducted controlled experiments and show that ContractGuard successfully guard against attacks on all real-world vulnerabilities and 83 percent of the seeded vulnerabilities.
Yuepeng Wang, Shuvendu K. Lahiri, Shuo Chen, Rong Pan · 7 authors
Ensuring correctness of smart contracts is paramount to ensuring trust in blockchain-based systems. This paper studies the safety and security of smart contracts in the \emph{Azure Blockchain Workbench}, an enterprise Blockchain-as-a-Service offering from Microsoft. As part of this study, we formalize \emph{semantic conformance} of smart contracts against a state machine model with access-control policy and develop a highly-automated formal verifier for Solidity that can produce proofs as well as counterexamples. We have applied our verifier {\sc VeriSol} to analyze {\it all} contracts shipped with the Azure Blockchain Workbench, which includes application samples as well as a governance contract for Proof of Authority (PoA). We have found previously unknown bugs in these published smart contracts. After fixing these bugs, {\sc VeriSol} was able to successfully perform full verification for all of these contracts.
Michael Rodler, Wenting Li, Ghassan Karame, Lucas Davi
Recently, a number of existing blockchain systems have witnessed major bugs and vulnerabilities within smart contracts. Although the literature features a number of proposals for securing smart contracts, these proposals mostly focus on proving the correctness or absence of a certain type of vulnerability within a contract, but cannot protect deployed (legacy) contracts from being exploited. In this paper, we address this problem in the context of re-entrancy exploits and propose a novel smart contract security technology, dubbed Sereum (Secure Ethereum), which protects existing, deployed contracts against re-entrancy attacks in a backwards compatible way based on run-time monitoring and validation. Sereum does neither require any modification nor any semantic knowledge of existing contracts. By means of implementation and evaluation using the Ethereum blockchain, we show that Sereum covers the actual execution flow of a smart contract to accurately detect and prevent attacks with a false positive rate as small as 0.06% and with negligible run-time overhead. As a by-product, we develop three advanced re-entrancy attacks to demonstrate the limitations of existing offline vulnerability analysis tools.
André Greubel, Alexandra Dmitrienko, Samuel Kounev
In the Tor anonymity network, the distribution of topology information relies on the correct behavior of five out of the nine trusted directory authority servers. This centralization is concerning since a powerful adversary might compromise these servers and conceal information about honest nodes, leading to the full de-anonymization of all Tor users. Our work aims at distributing the work of these trusted authorities, such increasing resilience against attacks on core infrastructure components of the Tor network. In particular, we leverage several emerging technologies, such as blockchains, smart contracts, and trusted execution environments to design and prototype a system called SmarTor. This system replaces the directory authorities with a smart contract and a distributed network of untrusted entities responsible for bandwidth measurements. We prototyped SmarTor using Ethereum smart contracts and Intel SGX secure hardware. In our evaluation, we show that SmarTor produces significantly more reliable and precise measurements compared to the current measurement system. Overall, our solution improves the decentralization of the Tor network, reduces trust assumptions and increases resilience against powerful adversaries like law enforcement and intelligence services.
Christof Ferreira Torres, Julian Schütte, Radu State
The capability of executing so-called smart contracts in a decentralised manner is one of the compelling features of modern blockchains. Smart contracts are fully fledged programs which cannot be changed once deployed to the blockchain. They typically implement the business logic of distributed apps and carry billions of dollars worth of coins. In that respect, it is imperative that smart contracts are correct and have no vulnerabilities or bugs. However, research has identified different classes of vulnerabilities in smart contracts, some of which led to prominent multi-million dollar fraud cases. In this paper we focus on vulnerabilities related to integer bugs, a class of bugs that is particularly difficult to avoid due to some characteristics of the Ethereum Virtual Machine and the Solidity programming language.
Xu Wang, Xuan F. Zha, Guangsheng Yu, Wei Ni · 8 authors
Ethereum, as the first Turing-complete blockchain platform, provides various application program interfaces for developers. Although blockchain has highly improved security, faulty configuration and usage can result in serious vulnerabilities. In this paper, we focus on the security vulnerabilities of the official Go-version Ethereum client (geth). The vulnerabilities are because of the insecure API design and the specific Ethereum wallet mechanism. We demonstrate attacks exploiting these vulnerabilities in an Ethereum testbed. The vulnerabilities are confirmed by the scanning results on the public Internet. Finally, corresponding countermeasures against attacks are provided to enhance the security of the Ethereum platform.
Elvira Albert, Pablo Gordillo, Albert Rubio, Ilya Sergey
Gas is a measurement unit of the computational effort that it will take to execute every single operation that takes part in the Ethereum blockchain platform. Each instruction executed by the Ethereum Virtual Machine (EVM) has an associated gas consumption specified by Ethereum. If a transaction exceeds the amount of gas allotted by the user (known as gas limit), an out-of-gas exception is raised. There is a wide family of contract vulnerabilities due to out-of-gas behaviours. We report on the design and implementation of GASTAP, a Gas-Aware Smart contracT Analysis Platform, which takes as input a smart contract (either in EVM, disassembled EVM, or in Solidity source code) and automatically infers sound gas upper bounds for all its public functions. Our bounds ensure that if the gas limit paid by the user is higher than our inferred gas bounds, the contract is free of out-of-gas vulnerabilities.
Elvira Albert, Pablo Gordillo, Albert Rubio, Ilya Sergey
Gas is a measurement unit of the computational effort that it will take to execute every single operation that takes part in the Ethereum blockchain platform. Each instruction executed by the Ethereum Virtual Machine (EVM) has an associated gas consumption specified by Ethereum. If a transaction exceeds the amount of gas allotted by the user (known as gas limit), an out-of-gas exception is raised. There is a wide family of contract vulnerabilities due to out-of-gas behaviours. We report on the design and implementation of GASTAP, a Gas-Aware Smart contracT Analysis Platform, which takes as input a smart contract (either in EVM, disassembled EVM, or in Solidity source code) and automatically infers sound gas upper bounds for all its public functions. Our bounds ensure that if the gas limit paid by the user is higher than our inferred gas bounds, the contract is free of out-of-gas vulnerabilities.
Jianbo Gao, Han Liu, Chao Liu, Qingshan Li · 6 authors
While Ethereum smart contracts enabled a wide range of blockchain applications, they are extremely vulnerable to different forms of security attacks. Due to the fact that transactions to smart contracts commonly involve cryptocurrency transfer, any successful attacks can lead to money loss or even financial disorder. In this paper, we focus on the overflow attacks in Ethereum, mainly because they widely rooted in many smart contracts and comparatively easy to exploit. We have developed EASYFLOW, an overflow detector at Ethereum Virtual Machine level. The key insight behind EASYFLOW is a taint analysis based tracking technique to analyze the propagation of involved taints. Specifically, EASYFLOW can not only divide smart contracts into safe contracts, manifested overflows, well-protected overflows and potential overflows, but also automatically generate transactions to trigger potential overflows. In our preliminary evaluation, EASYFLOW managed to find potentially vulnerable Ethereum contracts with little runtime overhead. A demo video of EASYFLOW is at https://youtu.be/QbUJkQI0L6o.
Ashar Ahmad, Muhammad Saad, Mostafa Bassiouni, Aziz Mohaisen
Audit logs serve as a critical component in the enterprise business systems that are used for auditing, storing, and tracking changes made to the data. However, audit logs are vulnerable to a series of attacks, which enable adversaries to tamper data and corresponding audit logs. In this paper, we present BlockAudit: a scalable and tamper-proof system that leverages the design properties of audit logs and security guarantees of blockchains to enable secure and trustworthy audit logs. Towards that, we construct the design schema of BlockAudit, and outline its operational procedures. We implement our design on Hyperledger and evaluate its performance in terms of latency, network size, and payload size. Our results show that conventional audit logs can seamlessly transition into BlockAudit to achieve higher security, integrity, and fault tolerance.
We investigate a family of bugs in blockchain-based smart contracts, which we call event-ordering (or EO) bugs. These bugs are intimately related to the dynamic ordering of contract events, i.e., calls of its functions on the blockchain, and enable potential exploits of millions of USD worth of Ether. Known examples of such bugs and prior techniques to detect them have been restricted to a small number of event orderings, typicall 1 or 2. Our work provides a new formulation of this general class of EO bugs as finding concurrency properties arising in long permutations of such events. The technical challenge in detecting our formulation of EO bugs is the inherent combinatorial blowup in path and state space analysis, even for simple contracts. We propose the first use of partial-order reduction techniques, using happen-before relations extracted automatically for contracts, along with several other optimizations built on a dynamic symbolic execution technique. We build an automatic tool called ETHRACER that requires no hints from users and runs directly on Ethereum bytecode. It flags 7-11% of over ten thousand contracts analyzed in roughly 18.5 minutes per contract, providing compact event traces that human analysts can run as witnesses. These witnesses are so compact that confirmations require only a few minutes of human effort. Half of the flagged contracts have subtle EO bugs, including in ERC-20 contracts that carry hundreds of millions of dollars worth of Ether. Thus, ETHRACER is effective at detecting a subtle yet dangerous class of bugs which existing tools miss.
Oct 26, 2018·Proceedings of the 2018 26th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering
Daejun Park, Yi Zhang, Manasvi Saxena, Philip Daian · 5 authors
In this paper, we present a formal verification tool for the Ethereum Virtual Machine (EVM) bytecode. To precisely reason about all possible behaviors of the EVM bytecode, we adopted KEVM, a complete formal semantics of the EVM, and instantiated the K-framework's reachability logic theorem prover to generate a correct-by-construction deductive verifier for the EVM. We further optimized the verifier by introducing EVM-specific abstractions and lemmas to improve its scalability. Our EVM verifier has been used to verify various high-profile smart contracts including the ERC20 token, Ethereum Casper, and DappHub MakerDAO contracts.
Neville Grech, Michael Kong, Anton Jurisevic, Lexi Brent · 6 authors
Ethereum is a distributed blockchain platform, serving as an ecosystem for smart contracts: full-fledged inter-communicating programs that capture the transaction logic of an account. Unlike programs in mainstream languages, a gas limit restricts the execution of an Ethereum smart contract: execution proceeds as long as gas is available. Thus, gas is a valuable resource that can be manipulated by an attacker to provoke unwanted behavior in a victim's smart contract (e.g., wasting or blocking funds of said victim). Gas-focused vulnerabilities exploit undesired behavior when a contract (directly or through other interacting contracts) runs out of gas. Such vulnerabilities are among the hardest for programmers to protect against, as out-of-gas behavior may be uncommon in non-attack scenarios and reasoning about it is far from trivial. In this paper, we classify and identify gas-focused vulnerabilities, and present MadMax: a static program analysis technique to automatically detect gas-focused vulnerabilities with very high confidence. Our approach combines a control-flow-analysis-based decompiler and declarative program-structure queries. The combined analysis captures high-level domain-specific concepts (such as "dynamic data structure storage" and "safely resumable loops") and achieves high precision and scalability. MadMax analyzes the entirety of smart contracts in the Ethereum blockchain in just 10 hours (with decompilation timeouts in 8% of the cases) and flags contracts with a (highly volatile) monetary value of over $2.8B as vulnerable. Manual inspection of a sample of flagged contracts shows that 81% of the sampled warnings do indeed lead to vulnerabilities, which we report on in our experiment.
Blockchain technology adds records to a list using cryptographic links. Therefore, the security of blockchain smart contracts is among the most popular contemporary research topics. To improve the theorem-proving technology in this field, we are developing an extensible hybrid verification tool chain, denoted as FSPVM-E, for Ethereum smart contract verification. This hybrid system extends the proof assistants in Coq, a formal proof-management system. Combining symbolic execution with higher-order theorem-proving, it solves consistency, automation, and reusability problems by standard theorem-proving approaches. This article completes the FSPVM-E by developing its proof engine. FSPVM-E is an extensible definitional interpreter based on our previous work FEther, which is totally developed in the Coq proof assistant. It supports almost all semantics of the Solidity programing language, and simultaneously executes multiple types of symbols. FEther also contains a set of automatic strategies that execute and verify the smart contracts in Coq with a high level of automation. The functional correctness of FEther was verified in Coq. In standard tutorials, the execution efficiency of FEther far exceeded that of the interpreters developed in Coq.
Decentralization, which has backed the hyper growth of many blockchains, comes at the cost of scalability. To understand this fundamental limitation, this paper proposes a quantitative measure of blockchain decentralization, and discusses its implications to various trust models and consensus algorithms. Further, we identify the major challenges in blockchain decentralization. Our key findings are that true decentralization is hard to achieve due to the skewed mining power and that a fully decentralized blockchain inherently limits scalability as it incurs a throughput upper bound and prevents scaling smart contract execution. To address these challenges, we outline three research directions to explore the trade-offs between decentralization and scalability.