In this study, firstly, a dataset of 10,476 annotated vulnerable ERC-20 standard token smart contracts (belonging to a set of 33 common smart contract vulnerabilities) has been collected from a publicly available repository. Secondly, using the SolMet smart contract metrics measurement tool, the object-oriented software attributes (i.e., metrics) from each smart contract's source code has been extracted. Lastly, using the source code metrics and the vulnerability annotations (i.e., labels) as the input in supervised machine learning (classification) algorithms, the accuracy of each individual algorithm is evaluated against the accuracy of an ensemble classifier (namely voting). The model accuracies demonstrate the feasibility of identifying and prioritising smart contracts for further inspection prior to deployment to the blockchain network. The ensemble classifier performed better (accuracy = 0.79) compared to each classifier when used individually.
Proof-of-Work~(PoW) based blockchains typically allocate only a tiny fraction (e.g., less than 1% for Ethereum) of the average interarrival time~$\mathbbI $ between blocks for validating smart contracts present in transactions. In such systems, block validation and PoW mining are typically performed sequentially, the former by CPUs and the latter by ASICs. A trivial increase in validation time~$(τ)$ introduces the popularly known Verifier's Dilemma, and as we demonstrate, causes more forking and hurts fairness. Large τ also reduces the tolerance for safety against a Byzantine adversary. Solutions that offload validation to a set of non-chain nodes (a.k.a. off-chain approaches) suffer from trust and performance issues that are non-trivial to resolve. In this paper, we present Tuxedo, the first on-chain protocol to theoretically scale τ/\mathbbI \approx 1$ in PoW blockchains. The key innovation in Tuxedo is to perform CPU-based block processing in \em parallel to ASIC mining. We achieve this by allowing miners to delay validation of transactions in a block by up to ζ blocks, where ζ is a system parameter. We perform security analysis of Tuxedo considering all possible adversarial strategies in a synchronous network with maximum end-to-end delay Δ and demonstrate that Tuxedo achieves security equivalent to known results for longest chain PoW Nakamoto consensus. Our prototype implementation of Tuxedo atop Ethereum demonstrates that it can scale τ without suffering the harmful effects of naïve scaling up of τ/\mathbbI $ in existing blockchains.
Yibin Yang, David Heath, Vladimir Kolesnikov, David Devecsery
Recent work has produced interactive Zero Knowledge (ZK) proof systems that can express proofs as arbitrary C programs (Heath et al., 2021, henceforth referred to as ZEE); these programs can be executed by a simulated ZK processor that runs in the 10KHz range. In this work, we demonstrate that such proof systems are amenable to high degrees of parallelism. Our epoch parallelism-based approach allows the prover and verifier to divide the ZK proof into pieces such that each piece can be executed on a different machine. These proof snippets can then be glued together, and the glued parallel proofs are equivalent to the original sequential proof. We implemented and we experimentally evaluate an epoch parallel version of the ZEE proof system. By running the prover and verifier each across 31 2-core machines, we achieve a ZK processor that runs at up to 394KHz. This allowed us to run a benchmark involving the Linux program bzip2, which would have required at least 11 days with the former ZEE system, in only 8.5 hours.
EOSIO smart contracts are programs that can be collectively executed by a network of mutually untrusted nodes. As EOSIO smart contracts manage valuable assets, they become high-value targets and are subjected to more and more attacks. Tools for protecting EOSIO smart contracts are imperative. This paper proposes EOSIOAnalyzer, an effective static secu-rity analysis framework for EOSIO smart contracts to counter the three most common attacks. The framework consists of three components, the control flow graph builder, the static analyzer and the vulnerability detector. This paper implements an approach to transforming low-level Wasm bytecode into a high-level intermediate representation (Register Transfer Language). Besides, this paper also implements vulnerability detection speci-fications for three popular EOSIO smart contracts vulnerabilities, including Fake EOS Transfer, Forged Transfer Notification and Block Information Dependency. As a proof of concept, this paper conducts experiments to evaluate the effectiveness and efficiency of the EOSIOAnalyzer. The experiment results show that the detection accuracy of the three vulnerabilities is 100 %, 98.8 % and 100%, respectively.
Rim Ben Fekih, Mariam Lahami, Mohamed Jmaïel, Ahmed Ben Ali · 5 authors
Smart contracts' vulnerabilities are widely dependent on developed code. Due to blockchain immutability, once this code is deployed it cannot be reversed. In this context, formal verification techniques are widely used to check smart contracts' correctness with respect to a given specification. In light of this, we introduce a model checking-based approach for solidity smart contracts and their blockchain environment using the nuXmv model checker. Our model-based approach considers the transaction pricing mechanism set by the Ethereum proposal EIP-1559 [1] and consists of three main steps, respectively, representing a smart contract with its blockchain behavior into an Extended Finite State Machine (EFSM) meanwhile, providing an over-approximation of the contract gas usage following the EIP-1559 proposal, then, encoding the modeled EFSM into nuXmv input language and, finally, specifying safety and liveness properties that will be checked against the model. Our contributions reason about modelling and checking gas usage consumption which makes it failure-aware. We illustrate this approach through a voting case study.
Smart contracts are self-executing programs that run on the blockchain and make it possible for peers to enforce agreements without a third-party guarantee. The smart contract on Ethereum is the fundamental element of decentralized finance with billions of US dollars in value. Smart contracts cannot be changed after deployment and hence the code needs to be verified for potential vulnerabilities. However, smart contracts are far from being secure and attacks exploiting vulnerabilities that have led to losses valued in the millions. In this work, we explore the current state of smart contracts security, prevalent vulnerabilities, and security-analysis tool support, through reviewing the latest advancement and research published in the past five years. We study 13 vulnerabilities in Ethereum smart contracts and their countermeasures, and investigate nine security-analysis tools. Our findings indicate that a uniform set of smart contract vulnerability definitions does not exist in research work and bugs pertaining to the same mechanisms sometimes appear with different names. This inconsistency makes it difficult to identify, categorize, and analyze vulnerabilities. We explain some safeguarding approaches and best practices. However, as technology improves new vulnerabilities may emerge. Regarding tool support, SmartCheck, DefectChecker, contractWard, and sFuzz tools are better choices in terms of more coverage of vulnerabilities; however, tools such as NPChecker, MadMax, Osiris, and Sereum target some specific categories of vulnerabilities if required. While contractWard is relatively fast and more accurate, it can only detect pre-defined vulnerabilities. The NPChecker is slower, however, can find new vulnerability patterns.
Quang-Thang Nguyen, Do Bao Son, Thi Tam Nguyen, Ba-Lam Do
Currently, the number of smart contracts using Solidity language in Ethereum increases at a breakneck speed. In this context, optimizing gas fees in smart contracts becomes necessary to save costs for both developers and users who interact directly with these contracts. To optimize gas, developers typically need to have deep knowledge of blockchain and programming languages, making it a significant challenge for new programmers. In this paper, we introduce GasSaver - an open-source tool that analyzes Solidity-based contracts and suggests modifications to reduce transaction fees. Our tool, which relies on a set of seven rules for identifying non-optimized codes, shows that 6,333 in a total of 10,245 top most interactive contracts on Ethereum contain at least one optimization problem and the total problems are more than 30,000. Hence, the use of this tool can reduce a considerable cost for the deployment and interaction of smart contracts.
Kunjian Song, Nedas Matulevicius, Eddie B. de Lima Filho, Lucas C. Cordeiro
Smart contracts written in Solidity are programs used in blockchain networks, such as Etherium, for performing transactions. However, as with any piece of software, they are prone to errors and may present vulnerabilities, which malicious attackers could then use. This paper proposes a solidity frontend for the efficient SMT-based context-bounded model checker (ESBMC), named ESBMC-Solidity, which provides a way of verifying such contracts with its framework. A benchmark suite with vulnerable smart contracts was also developed for evaluation and comparison with other verification tools. The experiments performed here showed that ESBMC-Solidity detected all vulnerabilities, was the fastest tool and provided a counterexample for each benchmark. A demonstration is available at https://youtu.be/3UH8_1QAVN0.
The detection of smart contracts vulnerability is a valuable research problem because smart contracts hold a huge amount of cryptocurrency. In the past, popular detection tools were mainly based on some traditional techniques such as fuzzing and symbolic execution, which rely on fixed expert features or patterns and often miss many vulnerabilities. Recent machine learning approaches alleviate this issue but do not notice the semantic information in the source code. In this paper, we develop a system called SVChecker to classify the smart contract source code written in Solidity. To show the superiority of our system, we conduct experiments on more than 40,000 smart contracts collected from Ethereum. Empirically, our experimental results demonstrate that our system outperforms all popular detection tools.
Blockchain technologies have found important and concrete applications in the real world. Active solutions leverage Smart Contracts for the management of cryptocurrencies, sensitive data, and other valuable assets. One of the core objectives of blockchain-oriented software engineering (BOSE) is ensuring that Smart Contracts receive adequate pre-release testing to guarantee the deployment of reliable code. However, the novelty and the complexity of the blockchain environment pose new challenges to the validation and verification of Smart Contract based software. In this paper, we analyze the aforementioned challenges to foster the discussion on the specific topic of Smart Contract testing and identify relevant research directions.
Mixing schemes have been applied by Bitcoin users to break their payment links in the blockchain to enhance privacy. However, most mixing schemes cannot provide secure mixing service without compromising efficiency since they are relying on complex cryptographic techniques or interactive protocols. To provide secure yet efficient mixing service, researchers introduce Intel SGX enclave, which provides Trusted Execution Environment (TEE) with confidentiality and integrity guarantees to execute mixing operations. Unfortunately, users will lose their mixing funds if a malicious service provider compromises the confidentiality guarantee of his/her enclave. Moreover, the scheme cannot scale to a large number of users in a single mixing round, that is, limited scalability. In this paper, we present a novel decentralized mixing scheme with multiple enclaves run by different service providers, which uses Shamir secret sharing scheme and additive homomorphic property of keys in Elliptic Curve Cryptography to tolerate a subset of enclaves to be compromised. Moreover, our scheme also provides stronger scalability so it achieves anonymity sets by orders of magnitude higher than the existing TEE-based mixing scheme. The experiment shows our scheme can provide stronger security and anonymity guarantees without compromising efficiency which outperforms existing mixing schemes.
Bernd Finkbeiner, Jana Hofmann, Florian Kohn, Noemi Passing
Smart contracts are small but highly error-prone programs that implement agreements between multiple parties. We present a reactive synthesis approach for the automatic construction of smart contract state machines. Towards this end, we extend temporal stream logic (TSL) with universally quantified parameters over infinite domains. Parameterized TSL is a convenient logic to specify the temporal control flow, i.e., the correct order of transactions, as well as the data flow of the contract's fields. We develop a two-step approach that 1) synthesizes a finite representation of the - in general - infinite-state system and 2) splits the system into a compact hierarchical architecture that enables the implementation of the state machine in Solidity. We implement the approach in our prototype tool SCSynt, which - within seconds - automatically constructs Solidity code that realizes the specified control flow.
It has been recognized that one of the bottlenecks in the UTXO-based blockchain systems is the slow block validation - the process of validating a newly-received block by a node before locally storing it and further broadcasting it. As a block contains multiple inputs, the block validation mainly involves checking the inputs against the status data, which is also known as the Unspent Transaction Outputs (UTXO) set. As time goes by, the UTXO set becomes more and more expansive, most of which can only be stored on disks. This considerably slows down the input checking and thus block validation, which can potentially compromise system security. To deal with the above problem, we disassemble the function of input checking into three parts: existence validation (EV), unspent validation (UV), and script validation (SV). Based on the disassembly, we propose EBV, an efficient block validation mechanism to speed up EV, UV, and SV individually. First, EBV changes the representation of status data, from UTXO set to a bit-vector set, which drastically reduces its size. The smaller status data can be entirely maintained in memory, thereby accelerating UV and also block validation. Second, EBV requires each transaction to carry the proof data, which enables EV and SV without accessing the disks. Furthermore, we also cope with two challenges in the design of EBV, namely transaction inflation and fake positions. To evaluate the EBV mechanism, we implement a prototype on top of Bitcoin, the most widely known UTXO-based blockchain, and conduct extensive experiments to compare EBV and Bitcoin. The experimental results demonstrate that EBV successfully reduces the memory requirement by 93.1 % and the block validation time by up to 93.5%.
Smart contracts are usually financial-related, which makes them attractive attack targets. Many static analysis tools have been developed to facilitate the contract audit process, but not all of them take account of two special features of smart contracts: (1) The external variables, like time, are constrained by real-world factors; (2) The internal variables persist between executions. Since these features import implicit constraints into contracts, they significantly affect the performance of static tools, such as causing errors in reachability analysis and resulting in false positives. In this paper, we conduct a systematic study on implicit constraints from three aspects. First, we summarize the implicit constraints in smart contracts. Second, we evaluate the impact of such constraints on the state-of-the-art static tools. Third, we propose a lightweight but effective mitigation method named ConSym to deal with such constraints and integrate it into OSIRIS. The evaluation result shows that ConSym can filter out 96% of false positives and reduce false negatives by two-thirds.
Min Fang, Xinna Zhou, Zhao Zhang, Cheqing Jin · 5 authors
The current blockchain system suffers from serious scalability bottleneck, which greatly limits the application in large-scale. Furthermore, with the emergence of high-throughput consensus algorithms in permissioned blockchain, how to efficiently execute smart contracts becomes a critical challenge. To solve this issue, a two-phase concurrent execution mechanism has been adopted recently, where the primary executes a batch of transactions concurrently in the first phase, then the rest replays them in the second phase to achieve consistency. However, these works only enable intra-node concurrency, not inter-node concurrency. This demonstration showcases SEFrame, a novel execution framework for smart contracts of permissioned blockchain to achieve intra- and inter-node concurrency with the confidentiality guarantee of Intel Software Guard Extensions (SGX). We use real-time dashboards containing the output of SEFrame, which allows attendees to interactively explore how SEFrame achieves efficient inter- and intra-node concurrency.
Smart cities deploy large numbers of sensors and collect a tremendous amount of data from them. For example, Advanced Metering Infrastructures (AMIs), which consist of physical meters that collect usage data about public utilities such as power and water, are an important building block in a smart city. In a typical sensor network, the measurement devices are connected through a computer network, which exposes them to cyber attacks. Furthermore, the data is centrally managed at the operator's servers, making it vulnerable to insider threats. Our goal is to protect the integrity of data collected by large-scale sensor networks and the firmware in measurement devices from cyber attacks and insider threats. To this end, we first develop a comprehensive threat model for attacks against data and firmware integrity, which can target any of the stakeholders in the operation of the sensor network. Next, we use our threat model to analyze existing defense mechanisms, including signature checks, remote firmware attestation, anomaly detection, and blockchain-based secure logs. However, the large size of the Trusted Computing Base and a lack of scalability limit the applicability of these existing mechanisms. We propose the Feather-Light Blockchain Infrastructure (FLBI) framework to address these limitations. Our framework leverages a two-layer architecture and cryptographic threshold signature chains to support large networks of low-capacity devices such as meters and data aggregators. We have fully implemented the FLBI's end-to-end functionality on the Hyperledger Fabric and private Ethereum blockchain platforms. Our experiments show that the FLBI is able to support millions of end devices.
This document provides a clear description of the COLLABS level-2 security components. In particular, it describes fine-grained authorization for constrained environments, relying on distributed ledger technologies for exchanges between different involved mechanisms. We show how COLLABS ledger-based security modules can secure inter-device communications and enhance the trust level in inter-<br> The project COLLABS has received funding from the European Union’s Horizon 2020 research and innovation programme under grant agreement No 871518.<br> device collaboration, on several aspects of the Smart Factory lifecycle. We describe how COLLABS ensures that all the data collected from connected objects, and all the actions are authorized following an effective security policy. This document also illustrates the main data flows with sequence diagrams, describing and visualizing processes involving each component, as well as mapping of COLLABS level-2 security components to the use case scenarios.
Chao Ni, Cong Tian, Kaiwen Yang, David Lo · 6 authors
Smart contract, a special software code running on and resided in the blockchain, enlarges the general application of blockchain and exchanges assets without dependence of external parties. With blockchain’s characteristic of immutability, they cannot be modified once deployed. Thus, the contract and the records are persisted on the blockchain forever, including failed transactions that are caused by runtime errors and result in the waste of computation, storage, and fees. In this paper, we refer to smart contracts which will cause runtime errors as crash-inducing smart contracts. However, automatic identification of crash-inducing smart contracts is limited investigated in the literature. The existing approaches to identify crash-inducing smart contracts are either limited in finding vulnerability (e.g., pattern-based static analysis) or very expensive (e.g., program analysis), which is insufficient for Ethereum.To reduce runtime errors on Ethereum, we propose an efficient, generalizable, and machine learning-based crash-inducing smart contract detector, CRASHSCDET, to automatically identify crash-inducing smart contracts. To investigate the effectiveness of CRASHSCDET, we firstly propose 34 static source code metrics from four dimensions (i.e., complexity metrics, count metrics, object-oriented metrics, and Solidity-specific metrics) to characterize smart contracts. Then, we collect a large-scale dataset of verified smart contracts (i.e., 54,739) and label these smart contracts based on their execution traces on Etherscan. We make a comprehensive comparison with three state-of-the-art approaches and the results show that CRASHSCDET can achieve good performance (i.e., 0.937 of F1-measure and 0.980 of AUC on average) and statistically significantly improve the baselines by 0.5%-60.4% in terms of F1-measure and by 41.2%-44.3% in terms of AUC, which indicates the effectiveness of static source code metrics in identifying crash-inducing smart contracts. We further investigate the importance of different types of metrics and find that metrics in different dimensions have varying abilities to depict the characteristic of smart contracts. Especially, metrics belonging to the "Count" dimension are the most discriminative ones but combining all metrics can achieve better prediction performance.
Smart contracts on the Ethereum blockchain greatly benefit from cutting-edge analysis techniques and pose significant challenges. A primary challenge is the extremely low-level representation of deployed contracts. We present Elipmoc, a decompiler for the next generation of smart contract analyses. Elipmoc is an evolution of Gigahorse, the top research decompiler, dramatically improving over it and over other state-of-the-art tools, by employing several high-precision techniques and making them scalable. Among these techniques are a new kind of context sensitivity (termed “transactional sensitivity”) that provides a more effective static abstraction of distinct dynamic executions; a path-sensitive (yet scalable, through path merging) algorithm for inference of function arguments and returns; and a fully context sensitive private function reconstruction process. As a result, smart contract security analyses and reverse-engineering tools built on top of Elipmoc achieve high scalability, precision and completeness. Elipmoc improves over all notable past decompilers, including its predecessor, Gigahorse, and the state-of-the-art industrial tool, Panoramix, integrated into the primary Ethereum blockchain explorer, Etherscan. Elipmoc produces decompiled contracts with fully resolved operands at a rate of 99.5% (compared to 62.8% for Gigahorse), and achieves much higher completeness in code decompilation than Panoramix—e.g., up to 67% more coverage of external call statements—while being over 5x faster. Elipmoc has been the enabler for recent (independent) discoveries of several exploitable vulnerabilities on popular protocols, over funds in the many millions of dollars.
Distributed ledger systems have become more prominent and successful in recent years, with a focus on blockchains and cryptocurrency. This has led to various misunderstandings about both the technology itself and its capabilities, as in many cases blockchain and cryptocurrency is used synonymously and other applications are often overlooked. Therefore, as a whole, the view of distributed ledger technology beyond blockchains and cryptocurrencies is very limited. Existing vocabularies and ontologies often focus on single aspects of the technology, or in some cases even just on one product. This potentially leads to other types of distributed ledgers and their possible use cases being neglected. In this paper, we present a knowledge graph and an ontology for distributed ledger technologies, which includes security considerations to model aspects such as threats and vulnerabilities, application domains, as well as relevant standards and regulations. Such a knowledge graph improves the overall understanding of distributed ledgers, reveals their strengths, and supports the work of security personnel, i.e. analysts and system architects. We discuss potential uses and follow semantic web best practices to evaluate and publish the ontology and knowledge graph.
Despite the benefits that the Blockchain technology brings to many application fields, its adoption does not come without challenges. Smart contracts, which are at the core of 2nd generation blockchains, can often be riddled with vulnerabilities that can be exploited to attack the platform and threaten its security. It is therefore crucial for the protection of the designed systems to prove the correctness of the smart contracts to be deployed. Approaches have been proposed to detect generic vulnerabilities like reentrancy, but the results would often include false positives where the detected bug is either non existent or not exploitable. Besides, such approaches do not offer to check contract-specific properties. The work presented in this paper is situated as part of a formal approach that we have proposed in an attempt to bridge this gap. This previously outlined approach is based on the transformation of Solidity smart contracts into Coloured Petri nets, which provides the possibility to verify smart contracts with reference to properties expressed as Linear Temporal Logic (LTL) formulae. Herein we extend our previous work on mainly two levels: first, by taking into account the concept of function calls in the transformation and second, by focusing on the LTL properties that can define the correctness of a smart contract. Such properties can be specific to the control- or data-flow of the contracts being checked. They can also be used to express vulnerabilities as we showcase by proposing LTL formalizations for six vulnerabilities from the literature. We then leverage the capability of the Helena model checker to detect these vulnerabilities while discerning their exploitability, as well as check temporal-based contract-specific properties.
Pietro Ferraro, Andreas Penzkofer, Christopher King, Robert Shorten
In this article, we present a feedback approach to the design of an attack mitigation policy for directed acyclic graph (DAG)-based distributed ledgers. We develop a model to analyze the behavior of the ledger under the so-calledTips Inflation Attack, which endangers the liveness of transactions, and we design a control strategy to counteract this attack strategy. The efficacy of this approach is showcased through a theoretical analysis, in the form of two theorems about the stability properties of the ledger with and without the controller, and extensive Monte Carlo simulations of an agent-based model of the distributed ledger.