A smart contract is a computer protocol intended to digitally facilitate and enforce the negotiation of a contract in undependable environment. However, the number of attacks using the vulnerabilities of the smart contracts is also growing in recent years. Many solutions have been proposed in order to deal with them, such as documenting vulnerabilities or setting the security strategies. Among them, the most influential progress is made by the formal verification method. In this paper, we propose a formal verification method based on Colored Petri Nets (CPN) to verify smart contracts in blockchain system. First, we develop the smart contract models with possible attacker models based on hierarchical CPN modeling, then the smart contract models are executed by step-by-step simulation to validate their functional correctness, and finally we utilize the branch timing logic ASK-CTL based model checking technology in the CPN tools to detect latent vulnerabilities in smart contracts. We demonstrate that our CPN modeling based verification method can not only detect the logical vulnerabilities of the smart contract, but also consider the impacts of users behavior to find out potential non-logical vulnerabilities in the contracts, such as the vulnerabilities caused by the limitations of the Solidity language.
Decentralized attestation methods for blockchains are currently being discussed and standardized for use cases such as certification, identity and existence proofs. In a blockchain-based attestation, a claim made about the existence of information can be cryptographically verified publicly and transparently. In this paper we explore the attestation of models through globally unique identifiers as a first step towards decentralized applications based on models. As a proof-of-concept we describe a prototypical implementation of a software connector for the ADOxx metamodeling platform. The connector allows for (a.) the creation of claims bound to the identity of an Ethereum account and (b.) their verification on the blockchain by anyone at a later point in time. For evaluating the practical applicability, we demonstrate the application on the Ethereum network and measure and evaluate limiting factors related to transaction cost and confirmation times.
Zero-knowledge proofs have become an important tool for addressing privacy and scalability concerns in cryptographic protocols. For zero-knowledge proofs used in blockchain applications, it is desirable to have small proof sizes and fast verification. Yet by design, existing constructions with these properties such as zk-SNARKs also have a secret trapdoor embedded in a relation dependent structured reference string (SRS). Knowledge of this trapdoor suffices to break the security of these proofs. The SRSs required by zero-knowledge proofs are usually constructed with multiparty computation protocols, but the resulting parameters are specific to each individual circuit. In this thesis, we propose a model for constructing zero-knowledge arguments (i.e. zero-knowledge proofs with computational soundness) in which the generation of the SRS is directly considered in the security analysis. In our model the same SRS can be used across multiple applications. Further, the model is updatable i.e. users can update the universal SRS and the SRS is considered secure provided at least one of these users is honest. We propose two zero-knowledge arguments with updatable and universal SRSs, as well as a third which is neither updatable nor universal, but which through similar techniques achieves simulation extractability. The proposed arguments are practical, with proof sizes never more than a constant number of group elements. Verification for two of our constructions consist of a small number of pairing operations. For our other construction, which has the desirable property of a linear sized updatable and universal SRS, we describe efficient batching techniques so that verification is fast in the amortised setting.
Ethereum smart contracts are public, immutable and distributed and, as such, they are prone to vulnerabilities sourcing from programming mistakes of developers. This paper presents SAFEVM, a verification tool for Ethereum smart contracts that makes use of state-of-the-art verification engines for C programs. SAFEVM takes as input an Ethereum smart contract (provided either in Solidity source code, or in compiled EVM bytecode), optionally with assert and require verification annotations, and produces in the output a report with the verification results. Besides general safety annotations, SAFEVM handles the verification of array accesses: it automatically generates SV-COMP verification assertions such that C verification engines can prove safety of array accesses. Our experimental evaluation has been undertaken on all contracts pulled from etherscan.io (more than 24,000) by using as back-end verifiers CPAchecker, SeaHorn and VeryMax.
Modern blockchain systems support creation of smart contracts -- stateful programs hosted and executed on a blockchain. Smart contracts hold and transfer significant amounts of digital currency which makes them an attractive target for security attacks. It has been shown that many contracts deployed to public ledgers contain security vulnerabilities. Moreover, the design of blockchain systems does not allow the code of the smart contract to be changed after it has been deployed to the system. Therefore, it is important to guarantee the correctness of smart contracts prior to their deployment. Formal verification is widely used to check smart contracts for correctness with respect to given specification. In this work we consider program synthesis techniques in which the specification is used to generate correct-by-construction programs. We focus on one of the special cases of program synthesis where programs are modeled with finite state machines (FSMs). We show how FSM synthesis can be applied to the problem of automatic smart contract generation. Several case studies of smart contracts are outlined: crowdfunding platform, blinded auction and a license contract. For each case study we specify the corresponding smart contract with a set of formulas in linear temporal logic (LTL) and use this specification together with test scenarios to synthesize a FSM model for that contract. These models are later used to generate executable Solidity code which can be directly used in a blockchain system.
Public blockchains in support of Smart Contracts (SC), like Ethereum enable everyone to represent scarce, valuable resources (like cryptocurrencies) as so-called tokens. Token issuing and management was the first blockchain use case. However, programming languages and runtime systems used in the current blockchains for their SCs lack a secure and straightforward way to implement and handle tokens. The unnecessary complexity in doing so can lead to erroneous implementation of tokens and applications built on top of these, including the loss or theft of tokens as it happened. The most known attack was "TheDAO" attack which led to the "loss" of tokens, valued at that time at approximately 60 M US Dollar. A better and secure token representation directly embedded into a SC runtime and SC programming language could prevent loss of tokens. Thus this paper presents an approach including parts of a programming language using it. The core of the model is to use opaque and substructural data types together with an onchain soundness checker to generically represent tokens securely as values similar to integers and booleans. Such opaque data types enforce that only a designated piece of code can create values of that type. The substructural data types allow arbitrary values to express scarcity by preventing the duplication and elimination of values. The on-chain soundness checker ensures that the deployed code does not violate guarantees given by the type system, which includes opaque and substructural data types.
We consider IoT resources with a Trusted Execution Environment (TEE) and propose a model to provide trusted resource access that is linked to blockchain payments, ensuring the integrity and confidentiality of the IoT data. The model is built on the widely used OAuth 2.0 open authorization framework, which provides delegated authorization for IoT resources. We utilize hash-lock and time-lock mechanisms to cryptographically link trusted resource access, provided by the IoT resource's TEE, to authorization grants and blockchain payments. The model is implemented in the OP-TEE open source port for the Raspberry Pi that uses ARM's TrustZone and is evaluated on the Rinkeby public Ethereum testnet.
A blockchain based system integrity (BCSI) framework for assuring the integrity of information system processes is presented. BCSI is well suited for a broad class of large scale real-world information systems. Under the BCSI framework, the integrity of any information system I is assured by executing the finite state machine model for system I processes in a blockchain network. The BCSI framework is compared and contrasted with the Clark-Wilson (CW) system integrity model, and existing blockchain based frameworks like Ethereum.
There are more than 1 million smart contracts in Ethereum and the number of ethers managed by smart contracts has exceeded 100 million, but the security vulnerabilities in smart contracts seriously jeopardize the financial security of Ethereum users. Existing method for defect detection of smart contract bytecode using symbolic execution does not take care of the accuracy and detection realtime at same time. In this paper a smart contract bytecode defect detection algorithm based on parallel symbolic execution is proposed. We split a smart contract in units of functions by analyzing the smart contract function selection process. A symbolic execution tree is constructed for each function to predict the function execution path. Then we partition the symbolic execution tree into multiple sub-trees evenly. Finally, a process pool is used to perform parallel symbolic execution on those sub-trees to reduce the analysis time of smart contract defect detection. Experimental data shows our method has a significant improvement in detection efficiency compared with existing symbolic execution method. The speedup ratio is up to 3.1x in a 4-core computer. Besides, it does not introduce false positives or false negatives.
Due to the immutable nature of distributed ledger technology such as blockchain, it is of utter importance that a smart contract works as intended before employment outside test network. This is since any bugs or errors will become permanent once published to the live network, and could lead to substantial economic losses; as manifested in the infamous DAO smart contract exploit hack in 2016. In order to avoid this, formal verification methods can be used to ensure that the contract behaves according to given specifications. This paper presents a survey of the state of the art of formal verification of smart contracts. Being a relatively new research area, a standard or best practice for formal verification of smart contracts has not yet been established. Thus, several different methods and approaches have been used to perform the formal verification. The survey presented in this paper shows that some variant of model checking or theorem proving methodology seems to be most successful. However, as of today, formal verification is only successful on simple contracts, and does not support more advanced smart contract syntax.
The wide deployment of tokens for digital assets on top of Ethereum implies the need for powerful trading platforms. Vickrey auctions have been known to determine the real market price of items as bidders are motivated to submit their own monetary valuations without leaking their information to the competitors. Recent constructions have utilized various cryptographic protocols such as ZKP and MPC, however, these approaches either are partially privacy-preserving or require complex computations with several rounds. In this paper, we overcome these limits by presenting Trustee as a Vickrey auction on Ethereum which fully preserves bids' privacy at relatively much lower fees. Trustee consists of three components: a front-end smart contract deployed on Ethereum, an Intel SGX enclave, and a relay to redirect messages between them. Initially, the enclave generates an Ethereum account and ECDH key-pair. Subsequently, the relay publishes the account's address and ECDH public key on the smart contract. As a prerequisite, bidders are encouraged to verify the authenticity and security of Trustee by using the SGX remote attestation service. To participate in the auction, bidders utilize the ECDH public key to encrypt their bids and submit them to the smart contract. Once the bidding interval is closed, the relay retrieves the encrypted bids and feeds them to the enclave that autonomously generates a signed transaction indicating the auction winner. Finally, the relay submits the transaction to the smart contract which verifies the transaction's authenticity and the parameters' consistency before accepting the claimed auction winner. As part of our contributions, we have made a prototype for Trustee available on Github for the community to review and inspect it. Additionally, we analyze the security features of Trustee and report on the transactions' gas cost incurred on Trustee smart contract.
The development of blockchain technologies has enabled the trustless execution of so-called smart contracts, i.e. programs that regulate the exchange of assets (e.g., cryptocurrency) between users. In a decentralized blockchain, the state of smart contracts is collaboratively maintained by a peer-to-peer network of mutually untrusted nodes, which collect from users a set of transactions (representing the required actions on contracts), and execute them in some order. Once this sequence of transactions is appended to the blockchain, the other nodes validate it, re-executing the transactions in the same order. The serial execution of transactions does not take advantage of the multi-core architecture of modern processors, so contributing to limit the throughput. In this paper we propose a true concurrent model of smart contract execution. Based on this, we show how static analysis of smart contracts can be exploited to parallelize the execution of transactions.
Solidity is an object-oriented and high-level language for writing smart contracts that are used to execute, verify and enforce credible transactions on permissionless blockchains. In the last few years, analysis of smart contracts has raised considerable interest and numerous techniques have been proposed to check the presence of vulnerabilities in them. Current techniques lack traceability in source code and have widely differing work flows. There is no single unifying framework for analysis, instrumentation, optimisation and code generation of Solidity contracts. In this paper, we present SIF, a comprehensive framework for Solidity contract analysis, query, instrumentation, and code generation. SIF provides support for Solidity contract developers and testers to build source level techniques for analysis, understanding, diagnostics, optimisations and code generation. We show feasibility and applicability of the framework by building practical tools on top of it and running them on 1838 real smart contracts deployed on the Ethereum network.
Blockchain-based decentralized applications (DApp) have been widely adopted in different areas and trusted by more and more users due to the fact that the back end code of a DApp is publicly run on the blockchain and cannot be modified implicitly. However, there are few effective methods and tools for testing DApps and bugs can be easily introduced by inexperienced developers. The existing testing techniques either focus on testing front-end programs or back-end code but ignore the interaction between them, which makes it difficult to apply the techniques directly on DApp. In this paper, we present an automated testing technique for DApps which works in a two-phase manner. First, we employ random events to infer an abstract relation between browser-side events and blockchain-side contracts. Second, our technique generates a set of test cases under the guidance of inferred relations and orders the test cases based on a read-write graph. We also use taint analysis to track data flow of the smart contract and feed it to the generation procedure for following test cases. We have developed a tool called Sungari to implement our approach, and evaluated it on representative real-world DApps. The preliminary evaluation results demonstrated the potential of Sungari in achieving a significant optimization compared to random testing approaches.
Matthias Grundmann, Marc Leinweber, Hannes Hartenstein
We explore challenges of and present a concept for a decentralized payment service which is based on trusted execution environments. The system guarantees that users can always cash out their funds without depending on the cooperation of other network members, hence minimizing the trust required in other network members. We present an overview of the system, motivate key components for a secure architecture and provide a communication protocol. We prove that the payment service users can cash out their funds at any time without any dependence on other network members.
Blockchain-based cryptocurrencies have gained increasing adoption in recent years, and many hope that they may usher in a new era of decentralized electronic money. Unfortunately, they perform the core functions of money quite poorly due to their extremely volatile market value. On the other hand, blockchain “stablecoins” aiming to reduce this volatility, usually through a peg to an external currency like the US dollar, tend to greatly sacrifice decentralization of the money supply that make cryptocurrencies so attractive in the first place. Elasticoin is a novel currency issuance algorithm which greatly reduces price volatility by using the cryptographic puzzle of proofs of sequential work to fix the cost of minting a coin to sequential computation time. This causes coin supply to be highly elastic, quickly responding to demand for new coins and greatly dampening price swings. We argue that Elasticoin's fixed-minting-cost approach to low volatility has significant advantages over using pegs or explicit measurement of demand to adjust supply.
In the current Bitcoin network, lightweight clients outsource most of the computational and storage tasks to full blockchain nodes in order to run on resource-constrained devices, such as mobile phones. In the interactions with the full node, the lightweight client leaks considerable information about the Bitcoin transactions or addresses associated with this client. Therefore, the benefit of using lightweight client comes at costs of privacy. Existing solutions cannot support the lightweight client to retrieve the relevant transactions from the full node in an efficient and privacy-preserving way. In this paper, we propose a new approach to protect the privacy of lightweight clients in Bitcoin. Our main idea is to use private information retrieval (PIR) to guarantee that the lightweight clients can fetch the relevant transactions from untrusted full nodes without revealing to those nodes which particular transactions are being fetched. Directly using existing PIR scheme incurs high communication overhead for lightweight clients. Therefore, we propose an optimized protocol utilizing two-step PIR to efficiently retrieve the queried transactions without leaking sensitive query information. We developed a prototype implementation to demonstrate the feasibility of our proposed scheme.
Michał Król, Alberto Sonnino, Mustafa Al-Bassam, Argyrios G. Tasiopoulos · 6 authors
As cryptographic tokens and altcoins are increasingly being built to serve as utility tokens, the notion of useful work consensus protocols is becoming ever more important. With useful work consensus protocols, users get rewards after they have carried out some specific tasks useful for the network. While in some cases the proof of some utility or service can be provided, the majority of tasks are impossible to verify reliably. To deal with such cases, we design “Proof-of-Prestige” (PoP)—a reward system that can run directly on Proof-of-Stake (PoS) blockchains or as a smart contract on top of Proof-of-Work (PoW) blockchains. PoP introduces “prestige,” which is a volatile resource that, in contrast to coins, regenerates over time. Prestige can be gained by performing useful work, spent when benefiting from services, and directly translates to users minting power. Our scheme allows us to reliably reward decentralized workers while keeping the system free for the end-users. PoP is resistant against Sybil and collusion attacks and can be used with a vast range of unverifiable tasks. We build a simulator to assess the cryptoeconomic behavior of the system and deploy a full prototype of a content dissemination platform rewarding its participants. We implement the blockchain component on both Ethereum (PoW) and Cosmos (PoS), provide a mobile application, and connect it with our scheme with a negligible memory footprint. Finally, we adapt a fair exchange protocol allowing us to atomically exchange files for rewards also in scenarios where not all the parties have Internet connectivity. Our evaluation shows that even for large Ethereum traces, PoP introduces sub-millisecond computational overhead for miners in Cosmos and less than 0.013$ smart contract invocation cost for users in Ethereum.
Neville Grech, Lexi Brent, Bernhard Scholz, Yannis Smaragdakis
The rise of smart contracts - autonomous applications running on blockchains - has led to a growing number of threats, necessitating sophisticated program analysis. However, smart contracts, which transact valuable tokens and cryptocurrencies, are compiled to very low-level bytecode. This bytecode is the ultimate semantics and means of enforcement of the contract. We present the Gigahorse toolchain. At its core is a reverse compiler (i.e., a decompiler) that decompiles smart contracts from Ethereum Virtual Machine (EVM) bytecode into a highlevel 3-address code representation. The new intermediate representation of smart contracts makes implicit data- and control-flow dependencies of the EVM bytecode explicit. Decompilation obviates the need for a contract's source and allows the analysis of both new and deployed contracts. Gigahorse advances the state of the art on several fronts. It gives the highest analysis precision and completeness among decompilers for Ethereum smart contracts - e.g., Gigahorse can decompile over 99.98% of deployed contracts, compared to 88% for the recently-published Vandal decompiler and under 50% for the state-of-the-practice Porosity decompiler. Importantly, Gigahorse offers a full-featured toolchain for further analyses (and a “batteries included” approach, with multiple clients already implemented), together with the highest performance and scalability. Key to these improvements is Gigahorse's use of a declarative, logic-based specification, which allows high-level insights to inform low-level decompilation.
This paper describes Slither, a static analysis framework designed to provide rich information about Ethereum smart contracts. It works by converting Solidity smart contracts into an intermediate representation called SlithIR. SlithIR uses Static Single Assignment (SSA) form and a reduced instruction set to ease implementation of analyses while preserving semantic information that would be lost in transforming Solidity to bytecode. Slither allows for the application of commonly used program analysis techniques like dataflow and taint tracking. Our framework has four main use cases: (1) automated detection of vulnerabilities, (2) automated detection of code optimization opportunities, (3) improvement of the user's understanding of the contracts, and (4) assistance with code review. In this paper, we present an overview of Slither, detail the design of its intermediate representation, and evaluate its capabilities on real-world contracts. We show that Slither's bug detection is fast, accurate, and outperforms other static analysis tools at finding issues in Ethereum smart contracts in terms of speed, robustness, and balance of detection and false positives. We compared tools using a large dataset of smart contracts and manually reviewed results for 1000 of the most used contracts.
The Ethereum ecosystem has introduced a pervasive blockchain platform with programmable transactions. Everyone is allowed to develop and deploy smart contracts. Such flexibility can lead to a large collection of similar contracts, i.e., clones, especially when Ethereum applications are highly domain-specific and may share similar functionalities within the same domain, e.g., token contracts often provide interfaces for money transfer and balance inquiry. While smart contract clones have a wide range of impact across different applications, e.g., security, they are relatively little studied. Although clone detection has been a long-standing research topic, blockchain smart contracts introduce new challenges, e.g., syntactic diversity due to trade-off between storage and execution, understanding high-level business logic etc.. In this paper, we highlighted the very first attempt to clone detection of Ethereum smart contracts. To overcome the new challenges, we introduce the concept of smart contract birthmark, i.e., a semantic-preserving and computable representation for smart contract bytecode. The birthmark captures high-level semantics by effectively sketching symbolic execution traces (e.g., data access dependencies, path conditions) and maintain syntactic regularities (e.g., type and number of instructions) as well. Then, the clone detection problem is reduced to a computation of statistical similarity between two contract birthmarks. We have implemented a clone detector called EClone and evaluated it on Ethereum. The empirical results demonstrated the potential of EClone in accurately identifying clones. We have also extended EClone for vulnerability search and managed to detect CVE-2018-10376 instances.
A bug or error is a common problem that any software or computer program may encounter. It can occur from badly writing the program, a typing error or bad memory management. However, errors can become a significant issue if the unsafe program is used for critical systems. Therefore, formal methods for these kinds of systems are greatly required. In this paper, we use a formal language that performs deductive verification on an Ethereum Blockchain application based on smart contracts, which are self-executing digital contracts. Blockchain systems manipulate cryptocurrency and transaction information. Therefore , if a bug occurs in the blockchain, serious consequences such as a loss of money can happen. Thus, the aim of this paper is to propose a language dedicated to deductive verification, called Why3, as a new language for writing formal and verified smart contracts, thereby avoiding attacks exploiting such contract execution vulnerabilities. We first write a Why3 smart contracts program; next we formulate specifications to be proved as absence of RunTime Error properties and functional properties, then we verify the behavior of the program using the Why3 system. Finally we compile the Why3 contracts to the Ethereum Virtual Machine (EVM). Moreover, we give a set of generic mathematical statements that allows verifying functional properties suited to any type of smart contracts holding cryptocurrency, showing that Why3 can be a suitable language to write smart contracts. To illustrate our approach, we describe its application to a realistic industrial use case.