Bertrand Meyer, Alisa Arkadova, Alexander Kogtenkov
Class invariants -- consistency constraints preserved by every operation on objects of a given type -- are fundamental to building, understanding and verifying object-oriented programs. For verification, however, they raise difficulties, which have not yet received a generally accepted solution. The present work introduces a proof rule meant to address these issues and allow verification tools to benefit from invariants. It clarifies the notion of invariant and identifies the three associated problems: callbacks, furtive access and reference leak. As an example, the 2016 Ethereum DAO bug, in which $50 million were stolen, resulted from a callback invalidating an invariant. The discussion starts with a simplified model of computation and an associated proof rule, demonstrating its soundness. It then removes one by one the three simplifying assumptions, each removal raising one of the three issues, and leading to a corresponding adaptation to the proof rule. The final version of the rule can tackle tricky examples, including "challenge problems" listed in the literature.
Blockchain technology has developed significantly over the last decade. One of the reasons for this is its sustainability architecture, which does not allow modification of the history of committed transactions. That means that developers should consider blockchain vulnerabilities and eliminate them before the deployment of the system. In this paper, we demonstrate a statistical model checking approach for the verification of blockchain systems on three real-world attack scenarios. We build and verify models of DNS attack, double-spending with memory pool flooding, and consensus delay scenario. After that, we analyze experimental results and propose solutions to avoid these kinds of attacks.
Lu Liu, Lili Wei, Wuqi Zhang, Ming Wen · 6 authors
Smart contracts are programs stored on blockchains to execute transactions. When input constraints or security properties are violated at runtime, the transaction being executed by a smart contract needs to be reverted to avoid undesirable consequences. On Ethereum, the most popular blockchain that supports smart contracts, developers can choose among three transaction-reverting statements (i.e., require, if…revert, and if…throw) to handle anomalous transactions. While these transaction-reverting statements are vital for preventing smart contracts from exhibiting abnormal behaviors or suffering malicious attacks, there is limited understanding of how they are used in practice. In this work, we perform the first empirical study to characterize transaction-reverting statements in Ethereum smart contracts. We measured the prevalence of these statements in 3,866 verified smart contracts from popular dapps and built a taxonomy of their purposes via manually analyzing 557 transaction-reverting statements. We also compared template contracts and their corresponding custom contracts to understand how developers customize the use of transaction-reverting statements. Finally, we analyzed the security impact of transaction-reverting statements by removing them from smart contracts and comparing the mutated contracts against the original ones. Our study led to important findings. For example, we found that transaction-reverting statements are commonly used to perform seven types of authority verifications or validity checks, and missing such statements may compromise the security of smart contracts. We also found that current smart contract security analyzers cannot effectively handle transaction-reverting statements when detecting security vulnerabilities. Our findings can shed light on further research in the broad area of smart contract quality assurance and provide practical guidance to smart contract developers on the appropriate use of transaction-reverting statements.
Aug 19, 2021·2021 IEEE Intl Conf on Dependable, Autonomic and Secure Computing, Intl Conf on Pervasive Intelligence and Computing, Intl Conf on Cloud and Big Data Computing, Intl Conf on Cyber Science and Technology Congress (DASC/PiCom/CBDCom/CyberSciTech)
Shiv Sondhi, Sherif Saad, Kevin Shi, Mohammad Abdullah Al Mamun · 5 authors
A critical component of any blockchain or distributed ledger technology (DLT) platform is the consensus algorithm. Blockchain consensus algorithms are the primary vehicle for the nodes within a blockchain network to reach an agreement. In recent years, many blockchain consensus algorithms have been proposed mainly for private and permissioned blockchain networks. However, the performance of these algorithms and their reliability in hostile environments or the presence of byzantine and other network failures are not well understood. In addition, the testing and validation of blockchain applications come with many technical challenges. In this paper, we apply chaos engineering and testing to understand the performance of consensus algorithms in the presence of different loads, byzantine failure and other communication failure scenarios. We apply chaos engineering to evaluate the performance of three different consensus algorithms (PBFT, Clique, Raft) and their respective blockchain platforms. We measure the blockchain network's throughput, latency, and success rate while executing chaos and load tests. We develop lightweight blockchain applications to execute our test in a semi-production environment. Our results show that using chaos engineering helps understand how different consensus algorithms perform in a hostile or unreliable environment and the limitations of blockchain platforms. Our work demonstrates the benefits of using chaos engineering in testing complex distributed systems such as blockchain networks.
Scott Wesley, Maria Christakis, Jorge A. Navas, Richard Trefler · 6 authors
Solidity smart contracts are programs that manage up to 2^160 users on a\nblockchain. Verifying a smart contract relative to all users is intractable due\nto state explosion. Existing solutions either restrict the number of users to\nunder-approximate behaviour, or rely on manual proofs. In this paper, we\npresent local bundles that reduce contracts with arbitrarily many users to\nsequential programs with a few representative users. Each representative user\nabstracts concrete users that are locally symmetric to each other relative to\nthe contract and the property. Our abstraction is semi-automated. The\nrepresentatives depend on communication patterns, and are computed via static\nanalysis. A summary for the behaviour of each representative is provided\nmanually, but a default summary is often sufficient. Once obtained, a local\nbundle is amenable to sequential static analysis. We show that local bundles\nare relatively complete for parameterized safety verification, under moderate\nassumptions. We implement local bundle abstraction in SmartACE, and show\norder-of-magnitude speedups compared to a state-of-the-art verifier.\n
Decentralized autonomous organizations are a new form of smart contract based governance. Decentralized autonomous organization platforms, which support the creation of such organizations, are becoming increasingly popular, such as Aragon and Colony. Selecting the best fitting platform is challenging for organizations, as a significant number of decision criteria, such as popularity, developer availability, governance issues, and consistent documentation of such platforms, should be considered. Additionally, decision-makers at the organizations are not experts in every domain, so they must continuously acquire volatile knowledge regarding such platforms. Supporting decision-makers in selecting the right decentralized autonomous organizations by designing an effective decision model is the main objective of this study. We aim to provide more insight into their selection process and reduce time and effort significantly by designing a decision model. This study presents a decision model for the decentralized autonomous organization platform selection problem. The decision model captures knowledge regarding such platforms and concepts systematically. The decision model is based on an existing theoretical framework that assists software engineers with a set of Multi-Criteria Decision-Making problems in software production. We conducted three industry case studies in the context of three decentralized autonomous organizations to evaluate the effectiveness and efficiency of the decision model in assisting decision-makers. The case study participants declared that the decision model provides significantly more insight into their selection process and reduces time and effort. We observe in the empirical evidence from the case studies that decision-makers can make more rational, efficient, and effective decisions with the decision model. Furthermore, the reusable form of captured knowledge regarding Decentralized Autonomous Organization Platforms can be employed by other researchers in their future investigations.
Intuitively there is a drastic distinction between the pure decentralized block-chain systems like Defis and those that only utilize block-chain as an enhancing technology but remain centralized with real-world business model and conventional technologies like database, application server, etc. Our study explores extensively this distinction from a methodological point of view, classifies them into blockchain-complete and blockchain-partial, analyzes key features of the two types, and reveals the root cause of this distinction. We analyze the function or, in more strong words, the "ultimate purpose" of blockchain in the blockchain-partial systems, and present a conceptual model we named proof-chain that quite satisfactorily represented the general paradigm of blockchain in blockchain-partial systems. A universal tension between strength of proof-chain and privacy is then revealed and the zero-knowledge based proof-chain takes shape. Several case studies demonstrate the explaining power of our proof-chain methodology. We then apply proof-chain methodology to the analysis of the ecosystem of a collaborating group of blockchain-partial systems, representing the paradigm of public and private data domain whose border the proof-chain crosses. Finally, some derived guidelines from this methodology speak usefulness of our methodology.
In recent years, as blockchain adoption has been expanding across a wide range of domains, e.g., digital asset, supply chain finance, etc., the confidentiality of smart contracts is now a fundamental demand for practical applications. However, while new privacy protection techniques keep coming out, how existing ones can best fit development settings is little studied. Suffering from limited architectural support in terms of programming interfaces, state-of-the-art solutions can hardly reach general developers. In this paper, we proposed the CLOAK framework for developing confidential smart contracts. The key capability of CLOAK is allowing developers to implement and deploy practical solutions to multi-party transaction (MPT) problems, i.e., transact with secret inputs and states owned by different parties by simply specifying it. To this end, CLOAK introduced a domain-specific annotation language for declaring privacy specifications and further automatically generating confidential smart contracts to be deployed with trusted execution environment (TEE) on blockchain. In our evaluation on both simple and real-world applications, developers managed to deploy business services on blockchain in a concise manner by only developing CLOAK smart contracts whose size is less than 30% of the deployed ones.
With its unique advantages such as decentralization and immutability, blockchain technology has been widely used in various fields in recent years. The smart contract running on the blockchain is also playing an increasingly important role in decentralized application scenarios. Therefore, the automatic detection of security vulnerabilities in smart contracts has become an urgent problem in the application of blockchain technology. Hyperledger Fabric is a smart contract platform based on enterprise-level licensed distributed ledger technology. However, the research on the vulnerability detection technology of Hyperledger Fabric smart contracts is still in its infancy. In this paper, we propose HFContractFuzzer, a method based on Fuzzing technology to detect Hyperledger Fabric smart contracts, which combines a Fuzzing tool for golang named go-fuzz and smart contracts written by golang. We use HFContractFuzzer to detect vulnerabilities in five contracts from typical sources and discover that four of them have security vulnerabilities, proving the effectiveness of the proposed method.
Since the emergence of Ethereum, blockchain-based decentralized applications (DApps) have become increasingly popular and important. To balance the security, performance, and costs, a DApp typically consists of two layers: an on-chain layer to execute transactions and store crucial data on the blockchain and an off-chain layer to interact with users. A DApp needs to synchronize its off-chain layer with the on-chain layer proactively. Otherwise, the inconsistent data in the off-chain layer could mislead users and cause undesirable consequences, e.g., loss of transaction fees. However, transactions sent to the blockchain are not guaranteed to be executed and could even be reversed after execution due to chain reorganization. Such non-determinism in the transaction execution is unique to blockchain. DApp developers may fail to perform the on-chain-off-chain synchronization accurately due to their lack of familiarity with the complex transaction lifecycle. In this work, we investigate the challenges of synchronizing on-chain and off-chain data in Ethereum-based DApps. We present two types of bugs that could result in inconsistencies between the on-chain and off-chain layers. To help detect such on-chain-off-chain synchronization bugs, we introduce a state transition model to guide the testing of DApps and propose two effective oracles to facilitate the automatic identification of bugs. We build the first testing framework, DArcher, to detect on-chain-off-chain synchronization bugs in DApps. We have evaluated DArcher on 11 popular real-world DApps. DArcher achieves high precision (99.3%), recall (87.6%), and accuracy (89.4%) in bug detection and significantly outperforms the baseline methods. It has found 15 real bugs in the 11 DApps. So far, six of the 15 bugs have been confirmed by the developers, and three have been fixed. These promising results demonstrate the usefulness of DArcher.
Context: Decentralized applications on blockchain platforms are realized through smart contracts. However, participants who lack programming knowledge often have difficulties reading the smart contract source codes, which leads to potential security risks and barriers to participation. Objective: Our objective is to translate the smart contract source codes into natural language descriptions to help people better understand, operate, and learn smart contracts. Method: This paper proposes an automated translation tool for Solidity smart contracts, termed SolcTrans, based on an abstract syntax tree and formal grammar. We have investigated 3,000 smart contracts and determined the part of speeches of corresponding blockchain terms. Among them, we further filtered out contract snippets without detailed comments and left 811 snippets to evaluate the translation quality of SolcTrans. Results: Experimental results show that even with a small corpus, SolcTrans can achieve similar performance to the state-of-the-art code comments generation models for other programming languages. In addition, SolcTrans has consistent performance when dealing with code snippets with different lengths and gas consumption. Conclusion: SolcTrans can correctly interpret Solidity codes and automatically convert them into comprehensible English text. We will release our tool and dataset for supporting reproduction and further studies in related fields.
Sota Sato, Ryotaro Banno, Jun Furuse, Kohei Suenaga · 5 authors
A Merkle tree is a data structure for representing a key-value store as a tree. Each node of a Merkle tree is equipped with a hash value computed from those of their descendants. A Merkle tree is often used for representing a state of a blockchain system since it can be used for efficiently auditing the state in a trustless manner. Due to the safety-critical nature of blockchains, ensuring the correctness of their implementation is paramount. We show our formally verified implementation of the core part of Plebeia using F*. Plebeia is a library to manipulate an extension of Merkle trees (called Plebeia trees). It is being implemented as a part of the storage system of the Tezos blockchain system. To this end, we gradually ported Plebeia to F*; the OCaml code extracted from the modules ported to F* is linked with the unverified part of Plebeia. By this gradual porting process, we can obtain a working code from our partially verified implementation of Plebeia; we confirmed that the binary passes all the unit tests of Plebeia. More specifically, we verified the following properties on the implementation of Plebeia: (1) Each tree-manipulating function preserves the invariants on the data structure of a Plebeia tree and satisfies the functional requirements as a nested key-value store; (2) Each function for serializing/deserializing a Plebeia tree to/from the low-level storage is implemented correctly; and (3) The hash function for a Plebeia tree is relatively collision-resistant with respect to the cryptographic safety of the blake2b hash function. During porting Plebeia to F*, we found a bug in an old version of Plebeia, which was overlooked by the tests bundled with the original implementation. To the best of our knowledge, this is the first work that verifies a production-level implementation of a Merkle-tree library by F*.
Millions of smart contracts have been deployed onto Ethereum for providing various services, whose functions can be invoked. For this purpose, the caller needs to know the function signature of a callee, which includes its function id and parameter types. Such signatures are critical to many applications focusing on smart contracts, e.g., reverse engineering, fuzzing, attack detection, and profiling. Unfortunately, it is challenging to recover the function signatures from contract bytecode, since neither debug information nor type information is present in the bytecode. To address this issue, prior approaches rely on source code, or a collection of known signatures from incomplete databases or incomplete heuristic rules, which, however, are far from adequate and cannot cope with the rapid growth of new contracts. In this paper, we propose a novel solution that leverages how functions are handled by Ethereum virtual machine (EVM) to automatically recover function signatures. In particular, we exploit how smart contracts determine the functions to be invoked to locate and extract function ids, and propose a new approach named type-aware symbolic execution (TASE) that utilizes the semantics of EVM operations on parameters to identify the number and the types of parameters. Moreover, we develop SigRec, a new tool for recovering function signatures from contract bytecode without the need of source code and function signature databases. The extensive experimental results show that SigRec outperforms all existing tools, achieving an unprecedented 98.7 percent accuracy within 0.074 seconds. We further demonstrate that the recovered function signatures are useful in attack detection, fuzzing and reverse engineering of EVM bytecode.
Mahdi Fahmideh, John Grundy, Aakash Ahmad, Jun Shen · 11 authors
Many scientific and practical areas have shown increasing interest in reaping the benefits of blockchain technology to empower software systems. However, the unique characteristics and requirements associated with Blockchain-based Software (BBS) systems raise new challenges across the development lifecycle that entail an extensive improvement of conventional software engineering. This article presents a systematic literature review of the state-of-the-art in BBS engineering research from the perspective of the software engineering discipline. We characterize BBS engineering based on the key aspects of theoretical foundations, processes, models , and roles . Based on these aspects, we present a rich repertoire of development tasks, design principles, models, roles, challenges, and resolution techniques. The focus and depth of this survey not only give software engineering practitioners and researchers a consolidated body of knowledge about current BBS development but also underpin a starting point for further research in this field.
First come, first served: Critical choices between alternative actions are often made based on events external to an organization, and reacting promptly to their occurrence can be a major advantage over the competition. In Business Process Management (BPM), such deferred choices can be expressed in process models, and they are an important aspect of process engines. Blockchain-based process execution approaches are no exception to this, but are severely limited by the inherent properties of the platform: The closed-world environment prevents direct access to external entities and data, and the passive runtime based entirely on atomic transactions impedes continual monitoring and detection of events. In this paper we provide an in-depth examination of the semantics of deferred choice, and transfer them to environments such as the blockchain. We introduce and compare several oracle architectures able to satisfy certain requirements, and show that they can be implemented using state-of-the-art blockchain technology.
Adrián Silveira, Gustavo Betarte, Maximiliano Cristiá, Carlos Luna
MimbleWimble (MW) is a privacy-oriented cryptocurrency technology which provides security and scalability properties that distinguish it from other protocols of its kind. We present and discuss those properties and outline the basis of a model-driven verification approach to address the certification of the correctness of the protocol implementations. In particular, we propose an idealized model that is key in the described verification process, and identify and precisely state sufficient conditions for our model to ensure the verification of relevant security properties of MW. Since MW is built on top of a consensus protocol, we develop a Z specification of one such protocol and present an excerpt of the $\{log\}$ prototype generated from the Z specification. This $\{log\}$ prototype can be used as an executable model where simulations can be run. This allows us to analyze the behavior of the protocol without having to implement it in a low level programming language. Finally, we analyze the Grin and Beam implementations of MW in their current state of development.
Shanshan Jiang, Kine Jakobsen, Letizia Jaccheri, Jingyue Li
Blockchain is an emerging technology with potential to address issues related to sustainability. Literature reviews on blockchain and sustain ability exist, but there is a need to consolidate existing results, in particular, in terms of Sustainable Development Goals (SDG). This extended abstract presents an ongoing tertiary study based on existing literature reviews to investigate the relationship between blockchain and sustain ability in terms of SDGs. Results from a pilot analysis of 18 reviews using thematic analysis are presented.
Decentralized services are increasingly being developed and their proper usage in different areas is being experimented with. Autonomous codes, which are also called smart contracts, can be developed with Integrated Development Environments (IDE). However, these tools lack live environment tests. The underlying blockchain technologies are also evolving and it is not easy to catch all the developments. There is a need for an easy-to-use interface by which the developers can see the results of their codes. Tubu-io decentralized application development workbench is developed to serve as an efficient way for the programmers to deploy smart contracts on the blockchain networks and interact with them easily. It can also be used for teaching decentralized application programming for junior blockchain developers on blockchain testbeds. Finally, it will have an effect in decreasing the development time and the costs of developing decentralized application projects.
Specific testing solutions targeting blockchain-based software are gaining huge attention as blockchain technologies are being increasingly incorporated into enterprise systems. As blockchain-based software enters production systems, it is paramount to follow proper engineering practices, ensure the required level of testing, and assess the readiness of the developed system. The existing research aims at addressing the testing-related issues and challenges of engineering blockchain-based software by providing suitable techniques and tools. However, like any emerging discipline, the best practices and tools for testing blockchain-based systems are not yet sufficiently developed. In this paper, we provide a comprehensive survey on the testing of Blockchain-based Applications (BC-Apps). First, we provide a discussion on identified challenges that are associated with BCApp testing. Second, we use a layered approach to discuss the state-of-the-art testing efforts in the area of BC technologies. In particular, we present an overview of the existing testing tools and techniques that provide testing solutions either for different components at various layers of the BC-App stack or across the whole stack. Third, we provide a set of future research directions based on the identified BC testing challenges and gaps in the literature review of existing testing solutions for BC-Apps. Moreover, we reflect on the specificity of BC-based software development procedure, which makes some of the existing tools or techniques inadequate, and call for the definition of standardised testing procedures and techniques for BC-Apps. The aim of our study is to highlight the importance of BC-based software testing and to pave the way for disciplined, testable, and verifiable BC software development.
Smart contracts are self-enforcing agreements that are employed to exchange assets without the approval of trusted third parties. This feature has encouraged various sectors to make use of smart contracts when transacting. Experience shows that many deployed contracts are vulnerable to exploitation due to their poor design, which allows attackers to steal valuable assets from the involved parties. Therefore, an assessment approach that allows developers to recognise the consequences of deploying vulnerable contracts is needed. In this paper, we propose a debt-aware approach for assessing security design vulnerabilities in smart contracts. Our assessment approach involves two main steps: (i) identification of design vulnerabilities using security analysis techniques and (ii) an estimation of the ramifications of the identified vulnerabilities leveraging the technical debt metaphor, its principal and interest. We use examples of vulnerable contracts to demonstrate the applicability of our approach. The results show that our assessment approach increases the visibility of security design issues. It also allows developers to concentrate on resolving smart contract vulnerabilities through technical debt impact analysis and prioritisation. Developers can use our approach to inform the design of more secure contracts and for reducing unintentional debts caused by a lack of awareness of security issues.
Recently, Blockchain technology adoption has expanded to many application areas due to the evolution of smart contracts. However, developing smart contracts is non-trivial and challenging due to the lack of tools and expertise in this field. A promising solution to overcome this issue is to use Model-Driven Engineering (MDE), however, using models still involves a learning curve and might not be suitable for non-technical users. To tackle this challenge, chatbot or conversational interfaces can be used to assess the non-technical users to specify a smart contract in gradual and interactive manner. In this paper, we propose iContractBot, a chatbot for modeling and developing smart contracts. Moreover, we investigate how to integrate iContractBot with iContractML, a domain-specific modeling language for developing smart contracts, and instantiate intention models from the chatbot. The iContractBot framework provides a domain-specific language (DSL) based on the user intention and performs model-to-text transformation to generate the smart contract code. A smart contract use case is presented to demonstrate how iContractBot can be utilized for creating models and generating the deployment artifacts for smart contracts based on a simple conversation.
Filippo Contro, Marco Crosara, Mariano Ceccato, Mila Dalla Preda
Motivated by the immutable nature of Ethereum smart contracts and of their transactions, quite many approaches have been proposed to detect defects and security problems before smart contracts become persistent in the blockchain and they are granted control on substantial financial value. Because smart contracts source code might not be available, static analysis approaches mostly face the challenge of analysing compiled Ethereum bytecode, that is available directly from the official blockchain. However, due to the intrinsic complexity of Ethereum bytecode (especially in jump resolution), static analysis encounters significant obstacles that reduce the accuracy of exiting automated tools. This paper presents a novel static analysis algorithm based on the symbolic execution of the Ethereum operand stack that allows us to resolve jumps in Ethereum bytecode and to construct an accurate control-flow graph (CFG) of the compiled smart contracts. EtherSolve is a prototype implementation of our approach. Experimental results on a significant set of real world Ethereum smart contracts show that EtherSolve improves the accuracy of the execrated CFGs with respect to the state of the art available approaches. Many static analysis techniques are based on the CFG representation of the code and would therefore benefit from the accurate extraction of the CFG. For example, we implemented a simple extension of EtherSolve that allows to detect instances of the re-entrancy vulnerability.
The great influence of Bitcoin has promoted the rapid development of blockchain-based digital currencies, especially the altcoins, since 2013. However, most altcoins share similar source codes, resulting in concerns about code innovations. In this paper, an empirical study on existing altcoins is carried out to offer a thorough understanding of various aspects associated with altcoin innovations. Firstly, we construct the dataset of altcoins, including source code repositories, GitHub fork relations, and market capitalizations (cap). Then, we analyze the altcoin innovations from the perspective of source code similarities. The results demonstrate that more than 85% of altcoin repositories present high code similarities. Next, a temporal clustering algorithm is proposed to mine the inheritance relationship among various altcoins. The family pedigrees of altcoin are constructed, in which the altcoin presents similar evolution features as biology, such as power-law in family size, variety in family evolution, etc. Finally, we investigate the correlation between code innovations and market capitalization. Although we fail to predict the price of altcoins based on their code similarities, the results show that altcoins with higher innovations reflect better market prospects.
Code comment has been an important part of computer programs, greatly facilitating the understanding and maintenance of source code. However, high-quality code comments are often unavailable in smart contracts, the increasingly popular programs that run on the blockchain. In this paper, we propose a Multi-Modal Transformer-based (MMTrans) code summarization approach for smart contracts. Specifically, the MMTrans learns the representation of source code from the two heterogeneous modalities of the Abstract Syntax Tree (AST), i.e., Structure-based Traversal (SBT) sequences and graphs. The SBT sequence provides the global semantic information of AST, while the graph convolution focuses on the local details. The MMTrans uses two encoders to extract both global and local semantic information from the two modalities respectively, and then uses a joint decoder to generate code comments. Both the encoders and the decoder employ the multi-head attention structure of the Transformer to enhance the ability to capture the long-range dependencies between code tokens. We build a dataset with over 300K pairs of smart contracts, and evaluate the MMTrans on it. The experimental results demonstrate that the MMTrans outperforms the state-of-the-art baselines in terms of four evaluation metrics by a substantial margin, and can generate higher quality comments.