Kai Hu, Zhu Jian, Yi Ding, Xiaomin Bai · 5 authors
A smart contract is the algorithmic description of a contractual transaction protocol that is automatically executed together with the information provided by its parties. It is written in a simplified programming language that is specific to a particular domain. Not only correctness and unambiguity are its essential formal properties, but also conformance to any legislation governing the matter of the transaction. Finally, and importantly, the trustworthiness, safety and security of the platform executing the transactions are its main attributes. An emerging challenge is to define a proper engineering process to meet the demanding requirements while supporting mass production and distribution. This paper proposes the concept of smart contract engineering (SCE) to facilitate the generation of smart legal contracts, which is the combination of software engineering, formal methods and computational law. SCE aims to reduce the potential errors and improve efficiency during the contract development process, meanwhile promote the standardization of contract design methodologies. In this paper, the roadmap of an iterative refinement-based, model-driven formal design methodology is introduced, not only to validate smart contracts but also to support the whole life cycle of their engineering.
Smart contracts — computer protocols that regulate the exchange of crypto-assets in trustless environments — have become popular with the spread of blockchain technologies. A landmark security property of smart contracts is liquidity: in a non-liquid contract, it may happen that some assets remain frozen, i.e. not redeemable by anyone. The relevance of this issue is witnessed by recent liquidity attacks to Ethereum, which have frozen hundreds of USD millions. We address the problem of verifying liquidity on BitML, a DSL for smart contracts with a secure compiler to Bitcoin, featuring primitives for currency transfers, contract renegotiation and consensual recursion. Our main result is a verification technique for liquidity. We first transform the infinite-state semantics of BitML into a finite-state one, which focusses on the behaviour of a chosen set of contracts, abstracting from the moves of the context. With respect to the chosen contracts, this abstraction is sound, i.e. if the abstracted contract is liquid, then also the concrete one is such. We then verify liquidity by model-checking the finite-state abstraction. We implement a toolchain that automatically verifies liquidity of BitML contracts and compiles them to Bitcoin, and we assess it through a benchmark of representative contracts.
Smart contracts - computer protocols that regulate the exchange of crypto-assets in trustless environments - have become popular with the spread of blockchain technologies. A landmark security property of smart contracts is liquidity: in a non-liquid contract, it may happen that some assets remain frozen, i.e. not redeemable by anyone. The relevance of this issue is witnessed by recent liquidity attacks to Ethereum, which have frozen hundreds of USD millions. We address the problem of verifying liquidity on BitML, a DSL for smart contracts with a secure compiler to Bitcoin, featuring primitives for currency transfers, contract renegotiation and consensual recursion. Our main result is a verification technique for liquidity. We first transform the infinite-state semantics of BitML into a finite-state one, which focusses on the behaviour of a chosen set of contracts, abstracting from the moves of the context. With respect to the chosen contracts, this abstraction is sound, i.e. if the abstracted contract is liquid, then also the concrete one is such. We then verify liquidity by model-checking the finite-state abstraction. We implement a toolchain that automatically verifies liquidity of BitML contracts and compiles them to Bitcoin, and we assess it through a benchmark of representative contracts.
Filipe Martins, David R. Matos, Miguel L. Pardal, Miguel Correia
Blockchain systems allow storing digital assets in a tamper-proof, consensus-based, append-only ledger in a decentralized fashion, where no single party has full control. A blockchain is an immutable, append-only, log of transactions. Unfortunately, in some cases there is the need to undo transactions that result from intrusions, e.g., when the private keys of a wallet are stolen, when one of the transaction participants does not comply with what was agreed upon, or when smart contract vulnerabilities are exploited by attackers. There are also accidental scenarios, e.g., when private keys are lost leaving the associated digital assets inaccessible. Although there have been a few proposals which allow modifications to the blockchain, they break the basic guarantees they are supposed to provide. We propose an approach for wallet owners to recover from attacks against their digital assets and accidental loss, while still assuring fundamental properties of the blockchain technology. We implemented the mechanism for Ethereum / EVM.
Callbacks are an effective programming discipline for implementing event-driven programming, especially in environments like Ethereum which forbid shared global state and concurrency. Callbacks allow a callee to delegate the execution back to the caller. Though effective, they can lead to subtle mistakes principally in open environments where callbacks can be added in a new code. Indeed, several high profile bugs in smart contracts exploit callbacks. We present the first static technique ensuring modularity in the presence of callbacks and apply it to verify prominent smart contracts. Modularity ensures that external calls to other contracts cannot affect the behavior of the contract. Importantly, modularity is guaranteed without restricting programming. In general, checking modularity is undecidable—even for programs without loops. This paper describes an effective technique for soundly ensuring modularity harnessing SMT solvers. The main idea is to define a constructive version of modularity using commutativity and projection operations on program segments. We believe that this approach is also accessible to programmers, since counterexamples to modularity can be generated automatically by the SMT solvers, allowing programmers to understand and fix the error. We implemented our approach in order to demonstrate the precision of the modularity analysis and applied it to real smart contracts, including a subset of the 150 most active contracts in Ethereum. Our implementation decompiles bytecode programs into an intermediate representation and then implements the modularity checking using SMT queries. Overall, we argue that our experimental results indicate that the method can be applied to many realistic contracts, and that it is able to prove modularity where other methods fail.
Static analysis of smart contracts as-deployed on the Ethereum blockchain has received much recent attention. However, high-precision analyses currently face significant challenges when dealing with the Ethereum VM (EVM) execution model. A major such challenge is the modeling of low-level, transient “memory” (as opposed to persistent, on-blockchain “storage”) that smart contracts employ. Statically understanding the usage patterns of memory is non-trivial, due to the dynamic allocation nature of in-memory buffers. We offer an analysis that models EVM memory, recovering high-level concepts (e.g., arrays, buffers, call arguments) via deep modeling of the flow of values. Our analysis opens the door to Ethereum static analyses with drastically increased precision. One such analysis detects the extraction of ERC20 tokens by unauthorized users. For another practical vulnerability (redundant calls, possibly used as an attack vector), our memory modeling yields analysis precision of 89%, compared to 16% for a state-of-the-art tool without precise memory modeling. Additionally, precise memory modeling enables the static computation of a contract’s gas cost. This gas-cost analysis has recently been instrumental in the evaluation of the impact of the EIP-1884 repricing (in terms of gas costs) of EVM operations, leading to a reward and significant publicity from the Ethereum Foundation.
Alley El-Dorry, Mohamed Reda, Sherif Abd El Khalek, Shehab El-Din Mohamed · 6 authors
The forgery of certificates is a long-term problem in the academic community of Egypt. It has become common to get a fake certificate, that claims an individual has graduated from a public/private university, and apply for jobs easily and be considered as qualified as someone who has a legit certificate. Blockchain, which is known for its reliability and trust, is used as a solution for that problem. The proposed system aims at creating digital certificates for Egyptian higher education as a solution for the forgery problem. This proposed system enables the tracking of a student's certificates; hence, the organizations and institutions can verify the obtained certificates. The proposed system is implemented using Linux Foundation's Hyperledger Fabric.
As cloud storage services have become popular nowadays, the integrity of outsourced data stored at untrusted servers received increased attention. Provable data possession (PDP) provides an effective and efficient solution for cloud data integrity by asking the cloud server to prove that the stored data are not tampered with or maliciously discarded without returning the actual data to users. In this article, we propose an efficient identity-based privacy-preserving provable data possession scheme (ID-P$^3$DP) based on the RSA assumption for secure cloud storage. In ID-P$^3$DP, a cloud user takes the outsourcing file and a global parameter in a time period as inputs to generate identity-based homomorphic authenticators, and any third-party auditor (TPA) can check the integrity of the outsourced file by verifying the validity of homomorphic authenticators. The distinguished feature of ID-P$^3$DP is to support the aggregation of identity-based homomorphic authenticators generated by different users under the RSA assumption, which is an open problem in provable data possession. Specifically, we transfer the identity-based homomorphic authenticators generated in distinct time periods into those with the same period parameter, and the cloud can compress the homomorphic authenticators of different users to generate a data possession proof for integrity verification. Besides, by exploiting zero-knowledge proof, the leakage of outsourced data to TPA can be prevented. The soundness of ID-P$^3$DP is proved based on the RSA assumption, and the privacy against TPA is perfectly preserved. Finally, we demonstrate ID-P$^3$DP is more efficient on integrity verification than the existing BLS-based schemes, and cross-user aggregate verification can significantly reduce computational and communication overhead for TPA.
Vankamamidi Srinivasa Naresh, V. V. L. Divakar Allavarpu, Sivaranjani Reddi
Abstract With the rapid increase in the popularity of groupware applications whose security mainly relied on the key being used, which made multi‐party/group secret key agreements significant. However, the brute‐force attacks to interpret the group key made group communication vulnerable. The logical solution to overcome this is changing the group key frequently. In this direction, we propose blockchain‐based multiple shared keys agreement among a group of participants. As with conventional methods, the proposed protocol does not rely on strong random number generation and/or master key. In this technique, the privacy‐preserving smart contract acts as group controller (GC) and forms two parties with each of the other nodes. The GC, while generating these two‐party keys in the first round instead of exchanging one public key, it exchanges “ m ” public keys with each of the other nodes and generates m 2 shared two‐party keys with each of the respective nodes. Now in the second round, GC generates m 2 sequential products of two‐party shared keys and stores them securely as private data objects in the privacy‐preserving smart contract. Next GC computes m 2 sequential public keys to each of the respective nodes by multiplying these products with the inverse of individual members shared keys sequentially of the group nodes in trusted execution environment and shares them with respective group nodes. On receiving respective public keys, each group node computes the multiple multiparty shared keys by multiplying it with their individual shared keys. Furthermore, an upper limit for the number of shared keys obtained in terms of the number of keys exchanged.
Giuseppe Antonio Pierro, Roberto Tonelli, Michele Marchesi
Many empirical software engineering studies show that there is a great need for repositories where source code is acquired, filtered and classified. During the last few years, Ethereum block explorer services have emerged as a popular project to explore and search Ethereum blockchain data such as transactions, addresses, tokens, smart-contracts' source code, prices and other activities taking place on the Ethereum blockchain. Despite the availability of this kind of services, retrieving specific information useful to empirical software engineering studies, such as the study of smart-contracts' software metrics might require many sub-tasks, such as searching specific transactions in a block, parsing files in HTML format and filtering the smart-contracts to remove duplicated code or unused smart-contracts. In this paper we afford this problem creating Smart Corpus', a Corpus of Smart Contracts in an organized reasoned and up to date repository where Solidity source code and other metadata about Ethereum smart contracts can easily and systematically be retrieved. We present the Smart Corpus' design and its initial implementation and we show how the data-set of smart contracts' source code in a variety of programming languages can be queried and processed, get useful information on smart contracts and their software metrics. The Smart Corpus aims to create a smart-contracts' repository where smart contracts data (source code, ABI and byte-code) are freely and immediately available and also classified based on the main software metrics identified in the scientific literature. Smart-contracts source code has been validated by EtherScan and each contract comes with its own associated software metrics as computed by the freely available software PASO. Moreover, Smart Corpus can be easily extended, as the number of new smart-contracts increases day by day.
Smart contracts encode critical application logic for realizing digital agreements in a tamper-proof form. Blockchains guarantee that smart contracts cannot be altered after the first deployment and that the execution is strictly followed. Smart contracts can only operate on data available on-chain. Oracles are bridging the gap between on-chain and off-chain data. Oracles introduce a wide range of security risks, which were already exploited in publicly known hacks. In this paper OraclesLink is proposed, which is a secure and developer-friendly architecture for using oracles within smart contracts. The goal of the architecture is to eliminate single points of failure and single sources of truth through distribution. In order to demonstrate feasibility, a proof-of-concept implementation is provided.
In recent years, the Bitcoin (BTC) payment is increasingly popular in retailers and service providers. A BTC transaction (tx) needs six confirmations (one hour) to be validated, making it not suitable for fast-pay scenarios. Theoretically, a shorter waiting time period increases the success possibility of a double-spending attack. To address this problem, we propose BTCFast scheme to support fast BTC tx. BTCFast is a novel, decentralized, escrow-based scheme on top of the programmable smart contract (PSC)-enabled blockchains (e.g. Ethereum, EOS). We develop a smart contract (PayJudger) to work as a trusted payment judger, which guarantees the tx fairness. In addition, we devise a proof-of-work (PoW)-based payment judgment mechanism for PayJudger to resolve a BTC payment dispute. Our theoretical and experimental results show that BTCFast can reduce the waiting time to be less than 1 second with comparable security as the current approach (i.e., waiting for six confirmations) with no extra operation fee.
Ahmed Akhtar, Basit Shafiq, Jaideep Vaidya, Ayesha Afzal · 6 authors
The use of blockchain technology has been proposed to provide auditable access control for individual resources. However, when all resources are owned by a single organization, such expensive solutions may not be needed. In this work we focus on distributed applications such as business processes and distributed workflows. These applications are often composed of multiple resources/services that are subject to the security and access control policies of different organizational domains. Here, blockchains can provide an attractive decentralized solution to provide auditability. However, the underlying access control policies may be overlapping in terms of the component conditions/rules, and simply using existing solutions would result in repeated evaluation of user's authorization separately for each resource, leading to significant overhead in terms of cost and computation time over the blockchain. To address this challenge, we propose an approach that formulates a constraint optimization problem to generate an optimal composite access control policy. This policy is in compliance with all the local access control policies and minimizes the policy evaluation cost over the blockchain. The developed smart contract(s) can then be deployed to the blockchain, and used for access control enforcement. We also discuss how the access control enforcement can be audited using a game-theoretic approach to minimize cost. We have implemented the initial prototype of our approach using Ethereum as the underlying blockchain and experimentally validated the effectiveness and efficiency of our approach.
Luís Pedro Arrojado da Horta, João Santos Reis, Simão Melo de Sousa, Mário Pereira
This paper introduces a deductive verification tool for smart contracts written in Michelson, which is the low-level language of the Tezos blockchain. Our tool accepts a formally specified Michelson contract and automatically translates it to an equivalent program written in WhyML, the programming and specification language of the Why3 framework. Smart contract instructions are mapped into a corresponding WhyML shallow-embedding of the their axiomatic semantics, which we also developed in the context of this work. One major advantage of this approach is that it allows an out-of-the-box integration with the Why3 framework, namely its VCGen and the backend support for several automated theorem provers. We also discuss the use of our tool to automatically prove the correctness of diverse annotated smart contracts.
Smart contract is a computer protocol running on the blockchain, which is widely used in various fields. However, its security problems continue to emerge. Therefore, it is necessary to audit the security of smart contract before it is deployed on the blockchain. Traditional testing methods cannot guarantee a high reliability and correctness required by the smart contract. This paper shows a method for using modeling, simulation and verification language (MSVL) and propositional projection temporal logic (PPTL) to model and verify the smart contract. First, a converter tool SOL2M which can convert Solidity program to MSVL program is developed. Then, the security properties of the smart contract are described by PPTL and a standardized process to verify the contract is designed through UMC4M (Unified Model Checker for MSVL). Finally, an example is given to illustrate the feasibility and practicability of this method in smart contract verification.
Yuichiro Chinen, Naoto Yanai, Jason Paul Cruz, Shingo Okamura
Ethereum smart contracts are programs that are deployed and executed in a consensus-based blockchain managed by a peer-to-peer network. Several re-entrancy attacks that aim to steal Ether, the cryptocurrency used in Ethereum, stored in deployed smart contracts were found in the recent years. A countermeasure to such attacks is based on dynamic analysis that executes the smart contracts themselves, but it requires the spending of Ether and knowledge of attack patterns for analysis in advance. In this paper, we present a static analysis tool named RA (Re-entrancy Analyzer), a combination of symbolic execution and equivalence checking by a satisfiability modulo theories solver to analyze smart contract vulnerabilities against re-entrancy attacks. In contrast to existing tools, RA supports analysis of inter-contract behaviors by using only the Ethereum Virtual Machine bytecodes of target smart contracts, i.e., even without prior knowledge of attack patterns and without spending Ether. Furthermore, RA can verify existence of vulnerabilities against re-entrancy attacks without execution of smart contracts and it does not provide false positives and false negatives. We also present an implementation of RA to evaluate its performance in analyzing the vulnerability of deployed smart contracts against re-entrancy attacks and show that RA can precisely determine which smart contracts are vulnerable.
This paper follows the line of works that design concretely efficient transparent sublinear zero-knowledge Interactive Oracle Proofs (IOP). Arguments obtained via this paradigm have the advantages of not relying on public-key cryptography, not requiring a trusted setup, and resistance to known quantum attacks. In the realm of transparent systems, Ligero and Aurora stand out with incomparable advantages where the former has a fast prover algorithm somewhat succinct proofs and the latter has somewhat fast prover and succinct proofs. In this work, we introduce Ligero++ that combines the best features of both approaches to achieve the best of both worlds. We implement our protocol and benchmark the results.
Behzad Abdolmaleki, Sebastian Ramacher, Daniel Slamanig
Zero-knowledge proofs and in particular succinct non-interactive zero-knowledge proofs (so called zk-SNARKs) are getting increasingly used in real-world applications, with cryptocurrencies being the prime example. Simulation extractability (SE) is a strong security notion for zk-SNARKs which informally ensures non-malleability of proofs. The high importance of this property is acknowledged by leading companies in this field such as Zcash and underpinned by various attacks against the malleability of cryptographic primitives in the past. Another problematic issue for the practical use of zk-SNARKs is the requirement of a fully trusted setup, as especially for large-scale decentralized applications finding a trusted party that runs the setup is practically impossible. Quite recently, the study of approaches to relax or even remove the trust in the setup procedure, and in particular subversion as well as updatable zk-SNARKs (with latter being the most promising approach), has been initiated and received considerable attention since then. Unfortunately, so far SE-SNARKs with the aforementioned properties are only constructed in an ad-hoc manner and no generic techniques are available.
Blockchain technology supports building transparent and decentralized systems in which the executed transactions can be easily traceable. Suppose one such system is intended to manage and process personal data. In that case, complementary mechanisms are required that make it possible for the system to comply, for instance, with data protection regulations. This work studies the integration of off-chain capabilities in blockchain-based solutions. In particular, we have focused on mechanisms that support safely moving data or computational operations outside the core blockchain network. We have carried out a thorough analysis of the European data protection regulation and discussed the weaknesses and strengths regarding the security and privacy requirements established by that regulation of solutions built using traditional blockchain technology.As a direct consequence of this study, we have conceived, and present in this paper, a system architecture for the design of privacy-aware solutions that use that kind of technology and put forward a systematic approach for performing a security and privacy threat analysis of one such solution. We illustrate the use of the proposed methodological tools, presenting and discussing the high-level design and security and privacy assessment of a system that provides services to handle, store, and validate digital academic certificates.
Winkle protects any validator-based byzantine fault tolerant consensus mechanisms, such as those used in modern Proof-of-Stake blockchains, against long-range attacks where old validators' signature keys get compromised. Winkle is a decentralized secondary layer of client-based validation, where a client includes a single additional field into a transaction that they sign: a hash of the previously sequenced block. The block that gets a threshold of signatures (confirmations) weighted by clients' coins is called a "confirmed" checkpoint. We show that under plausible and flexible security assumptions about clients the confirmed checkpoints can not be equivocated. We discuss how client key rotation increases security, how to accommodate for coins' minting and how delegation allows for faster checkpoints. We evaluate checkpoint latency experimentally using Bitcoin and Ethereum transaction graphs, with and without delegation of stake.
Package managers have become essential for software distribution and management. Their goal is to allow users to install programs, drivers, or updates in their systems in a secure, quick, and often, unattended way. However, in recent years, attackers have found severe flaws in software distribution systems and used them as a stealthy launch pad for malicious software. Moreover, it was proved that actors of the software supply-chain are ineffective in detecting and stopping attacks on user devices.
Smart contracts are Turing-complete programs running on the blockchain. They cannot be modified, even when bugs are detected. The Selfdestruct function is the only way to destroy a contract on the blockchain system and transfer all the Ethers on the contract balance. Thus, many developers use this function to destroy a contract and redeploy a new one when bugs are detected. In this paper, we propose a deep learning-based method to find security issues of Ethereum smart contracts by finding the updated version of a destructed contract. After finding the updated versions, we use open card sorting to find security issues.
Michael Rodler, Wenting Li, Ghassan Karame, Lucas Davi
Recent attacks exploiting errors in smart contract code had devastating consequences thereby questioning the benefits of this technology. It is currently highly challenging to fix errors and deploy a patched contract in time. Instant patching is especially important since smart contracts are always online due to the distributed nature of blockchain systems. They also manage considerable amounts of assets, which are at risk and often beyond recovery after an attack. Existing solutions to upgrade smart contracts depend on manual and error-prone processes. This paper presents a framework, called EVMPatch, to instantly and automatically patch faulty smart contracts. EVMPatch features a bytecode rewriting engine for the popular Ethereum blockchain, and transparently/automatically rewrites common off-the-shelf contracts to upgradable contracts. The proof-of-concept implementation of EVMPatch automatically hardens smart contracts that are vulnerable to integer over/underflows and access control errors, but can be easily extended to cover more bug classes. Our extensive evaluation on 14,000 real-world (vulnerable) contracts demonstrate that our approach successfully blocks attack transactions launched on these contracts, while keeping the intended functionality of the contract intact. We perform a study with experienced software developers, showing that EVMPatch is practical, and reduces the time for converting a given Solidity smart contract to an upgradable contract by 97.6 %, while ensuring functional equivalence to the original contract.