In recent years, as blockchain adoption has been expanding across a wide range of domains, e.g., supply chain finance, digital asset, 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. State-of-the-art solutions suffer from limited architectural support in terms of programming interfaces, thus can hardly reach general developers. This paper proposes Cloak, a pluggable and configurable framework for developing and deploying confidential smart contracts. The key capability of Cloakis 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 allows users to specify privacy invariants in a declarative way, automatically generate runtime with verifiably enforced privacy and deploy it to the existing platforms with TEE-Blockchain architecture to enable the MPT. In our evaluation on both examples and real-world applications, developers manage 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 and the gas cost of deployed MPTs reduces 19%.
The Industrial Internet of Things (IIoT) could enhance automation and analytics in industrial environments. Despite the promising benefits of IIoT, securely managing software updates is a challenging problem for those critical applications. This is due to at least the intrinsic lack of software protection mechanisms in legacy industrial systems. In this paper, to address the challenges in building a secure software supply chain for industrial environments, we propose a new approach that leverages distributed watchdogs with blockchain systems in protecting software supply chains. For this purpose, we bind every entity with a unique identity in the blockchain and employ the blockchain as a delegated authenticator by mapping every reporting action to a non-fungible token transfer. Moreover, we present a detailed specification to clearly define the behavior of systems and to apply model checking.
Francis Asuncion, Adam Brinckman, Dwayne Cole, Jeffrey H. Curtis · 28 authors
Blockchains have been around for more than ten years, and since 2015, a plethora of systems have been launched to target more flexible use cases. More recently, several enterprise blockchain systems, such as Consensys Quorum and Hyperledger Fabric, have been launched to make blockchain simpler to apply in complex organizational configurations. In this paper, we identify a specific Department of Defense use case, extrapolate requirements, and perform a thorough assessment of the different layers of the blockchain stack to identify the existing state of the art and undertake a gap analysis of the technology for this context. We describe a platform that meets many of these challenges and show how we architected, designed, and implemented a solution for this use case for deployment at NAVAIR. This solution connects transactions from two separate blockchain systems, Consensys Quorum and Hyperledger Fabric, by using a graph-based approach that preserves privacy while enabling full transparency across the military and supplier networks.
Ümit Cali, Murat Kuzlu, Manisa Pipattanasomporn, Onur Elma · 5 authors
Renewable energy sources (RES) are among the most popular emerging energy\nresources during the past two decades. Many countries have introduced various\nenergy policy instruments, such as renewable energy certificates (RECs), to\nsupport the growth of RES. RECs are tradable non-tangible assets, which have a\nmonetary value. Tracking and certification of the origin of an energy resource\nregardless of its type (e.g., a conventional power plant or RES) is a critical\noperation. In addition to the certification of origin, trading transactions are\nneeded to be performed using a secure method. Energy industry participants need\nto secure the data and applications related to RECs. Distributed ledger\ntechnology (DLT) is a perfect framework that can support such REC\nfunctionalities. This paper addresses the cybersecurity aspects in REC trading\nusing Blockchain and a distributed ledger technology, considering detailed\ncybersecurity perspectives.\n
Jonas Schiffl, Matthias Grundmann, Marc Leinweber, Oliver Stengele · 6 authors
Ethereum is a platform for deploying smart contracts, which due to their public nature and the financial value of the assets they manage are attractive targets for attacks. With asset management as a main task of smart contracts, access control aspects are naturally part of the application itself, but also of the functions implemented in a smart contract. Therefore, it is desirable to establish the correctness of smart contracts and their access control on application and single-function level through formal methods. However, there is no established methodology of formalising and verifying correctness properties of smart contracts. In this work, we make an attempt in this direction on the basis of a case study. We choose an existing smart contract application which aims to ascertain the integrity of binary files distributed over the Internet by means of decentralised identity management and access control. We formally specify and verify correctness at the level of single functions as well as temporal properties of the overall application. We demonstrate how to use verified low-level correctness properties for showing correctness at the higher level. In addition, we report on our experience with existing verification tools.
The security of distributed applications backed by blockchain technology relies mainly on keeping the associated cryptographic keys (i.e. private keys) in well-protected storage. Since they are the unique proof of ownership of the underlying digital assets. If the keys are stolen or lost, there is no way to recover the assets. The cold wallet is a good candidate for basic use cases, but it has a substantial challenge for more complex applications as it does not scale. Warm and hot wallets are more convenient options for blockchain-based solutions that aim to transact in a cloud environment. In this work, we focus on Hardware Security Module (HSM) based wallet. The HSM is the de-facto standard device designed to manage high-value cryptographic keys and to protect them against hacks. In this demonstration, we present an HSM-based working prototype that secures the entire life cycle of Ethereum public and private keys.
Christian Bräm, Marco Eilers, Péter Müller, Robin Sierra · 5 authors
Smart contracts are programs that execute inside blockchains such as Ethereum to manipulate digital assets. Since bugs in smart contracts may lead to substantial financial losses, there is considerable interest in formally proving their correctness. However, the specification and verification of smart contracts faces challenges that do not arise in other application domains. Smart contracts frequently interact with unverified, potentially adversarial outside code, which substantially weakens the assumptions that formal analyses can (soundly) make. Moreover, the core functionality of smart contracts is to manipulate and transfer resources; describing this functionality concisely requires dedicated specification support. Current reasoning techniques do not fully address these challenges, being restricted in their scope or expressiveness (in particular, in the presence of re-entrant calls), and offering limited means of expressing the resource transfers a contract performs.
In this paper, we present a novel specification methodology tailored to the domain of smart contracts. Our specification constructs and associated reasoning technique are the first to enable: (1) sound and precise reasoning in the presence of unverified code and arbitrary re-entrancy, (2) modular reasoning about collaborating smart contracts, and (3) domain-specific specifications based on resources and resource transfers, which allow expressing a contract's behavior in intuitive and concise ways and exclude typical errors by default. We have implemented our approach in 2vyper, an SMT-based automated verification tool for Ethereum smart contracts written in the Vyper language, and demonstrated its effectiveness in succinctly capturing and verifying strong correctness guarantees for real-world contracts.
Christian Bräm, Marco Eilers, Péter Müller, Robin Sierra · 5 authors
Smart contracts are programs that execute inside blockchains such as Ethereum to manipulate digital assets. Since bugs in smart contracts may lead to substantial financial losses, there is considerable interest in formally proving their correctness. However, the specification and verification of smart contracts faces challenges that do not arise in other application domains. Smart contracts frequently interact with unverified, potentially adversarial outside code, which substantially weakens the assumptions that formal analyses can (soundly) make. Moreover, the core functionality of smart contracts is to manipulate and transfer resources; describing this functionality concisely requires dedicated specification support. Current reasoning techniques do not fully address these challenges, being restricted in their scope or expressiveness (in particular, in the presence of re-entrant calls), and offering limited means of expressing the resource transfers a contract performs. In this paper, we present a novel specification methodology tailored to the domain of smart contracts. Our specification constructs and associated reasoning technique are the first to enable: (1) sound and precise reasoning in the presence of unverified code and arbitrary re-entrancy, (2) modular reasoning about collaborating smart contracts, and (3) domain-specific specifications based on resources and resource transfers, which allow expressing a contract's behavior in intuitive and concise ways and exclude typical errors by default. We have implemented our approach in 2vyper, an SMT-based automated verification tool for Ethereum smart contracts written in the Vyper language, and demonstrated its effectiveness in succinctly capturing and verifying strong correctness guarantees for real-world contracts.
We propose a novel framework for off-chain execution and verification of computationally-intensive smart contracts. Our framework is the first solution that avoids duplication of computing effort across multiple contractors, does not require trusted execution environments, supports computations that do not have deterministic results, and supports general-purpose computations written in a high-level language. Our experiments reveal that some intensive applications may require as much as 141 million gas, approximately 71x more than the current block gas limit for computation in Ethereum today, and can be avoided by utilizing the proposed framework.
This paper presents SAILFISH, a scalable system for automatically finding state-inconsistency bugs in smart contracts. To make the analysis tractable, we introduce a hybrid approach that includes (i) a light-weight exploration phase that dramatically reduces the number of instructions to analyze, and (ii) a precise refinement phase based on symbolic evaluation guided by our novel value-summary analysis, which generates extra constraints to over-approximate the side effects of whole-program execution, thereby ensuring the precision of the symbolic evaluation. We developed a prototype of SAILFISH and evaluated its ability to detect two state-inconsistency flaws, viz., reentrancy and transaction order dependence (TOD) in Ethereum smart contracts. Further, we present detection rules for other kinds of smart contract flaws that SAILFISH can be extended to detect. Our experiments demonstrate the efficiency of our hybrid approach as well as the benefit of the value summary analysis. In particular, we show that S SAILFISH outperforms five state-of-the-art smart contract analyzers (SECURITY, MYTHRIL, OYENTE, SEREUM and VANDAL ) in terms of performance, and precision. In total, SAILFISH discovered 47 previously unknown vulnerable smart contracts out of 89,853 smart contracts from ETHERSCAN .
Simon Joseph Aquilina, Fran Casino, Mark Vella, Joshua Ellul · 5 authors
Programming errors in Ethereum smart contracts can result in catastrophic financial losses from stolen cryptocurrency. While vulnerability detectors can prevent vulnerable contracts from being deployed, this does not mean that such contracts will not be deployed. Once a vulnerable contract is instantiated on the blockchain and becomes the target of attacks, the identification of exploit transactions becomes indispensable in assessing whether it has been actually exploited and identifying which malicious or subverted accounts were involved. In this work, we study the problem of post-factum investigation of Ethereum attacks using Indicators of Compromise (IoCs) specially crafted for use in the blockchain. IoC definitions need to capture the side-effects of successful exploitation in the context of the Ethereum blockchain. Therefore, we define a model for smart contract execution, comprising multiple abstraction levels that mirror the multiple views of code execution on a blockchain. Subsequently, we compare IoCs defined across the different levels in terms of their effectiveness and practicality through EtherClue, a prototype tool for investigating Ethereum security incidents. Our results illustrate that coarse-grained IoCs defined over blocks of transactions can detect exploit transactions with less computation; however, they are contract-specific and suffer from false negatives. On the other hand, fine-grained IoCs defined over virtual machine instructions can avoid these pitfalls at the expense of increased computation which are nevertheless applicable for practical use.
LibSWIFFT is an open-source, production-ready C/C++ library providing SWIFFT, one of the fastest available secure hash functions that is also collision-resistant. SWIFFT also facilitates post-quantum digital signature schemes and zero-knowledge proofs of knowledge of a preimage (ZKPoKP). LibSWIFFT is optimized for short blocks of input and runs at a rate of less than 5 cycles/byte single-threaded on a modern commodity computer with AVX2. Other software providing SWIFFT, which are not claiming production-readiness as LibSWIFFT is, are the original implementation by the authors of SWIFFT (Micciancio, 2016) and the SWIFFT 8-bit (Karati & Safavi-Naini, 2018b) and 16-bit (Karati & Safavi-Naini, 2018a) AVX2 implementations for the multi-signature scheme K2SN-MSS (Karati & Safavi-Naini, 2019).
Blockchain-based cryptocurrencies, facilitating the convenience of payment by providing a decentralized online solution, have not been widely adopted so far due to slow confirmation of transactions. Offline delegation offers an efficient way to exchange coins. However, in such an approach, the coins that have been delegated confront the risk of being spent twice since the delegator's behaviour cannot be restricted easily on account of the absence of effective supervision. Even if a third party can be regarded as a judge between the delegator and delegatee to secure transactions, she still faces the threat of being compromised or providing misleading assure. Moreover, the approach equipped with a third party contradicts the real intention of decentralized cryptocurrency systems. In this paper, we propose \textit{DelegaCoin}, an offline delegatable cryptocurrency system to mitigate such an issue. We exploit trusted execution environments (TEEs) as decentralized "virtual agents" to prevent malicious delegation. In DelegaCoin, an owner can delegate his coins through offline-transactions without interacting with the blockchain network. A formal model and analysis, prototype implementation, and further evaluation demonstrate that our scheme is provably secure and practically feasible.
With the rapid development of blockchain technology, different types of blockchains are adopted and interoperability across blockchains has received widespread attention. There have been many cross-chain solutions proposed in recent years, including notary scheme, sidechain, and relay chain. However, most of the existing platforms do not take confidentiality into account, although privacy has become an important concern for blockchain. In this paper, we present TrustCross, a privacy- preserving cross-chain platform to enable confidential interoperability across blockchains. The key insight behind TrustCross is to encrypt cross-chain communication data on the relay chain with the assistance of trusted execution environment and employ fine-grained access control to protect user privacy. Our experimental results show that TrustCross achieves reasonable latency and high scalability on the contract calls across heterogeneous blockchains.
Lital Badash, Nachiket Tapas, Asaf Nadler, Francesco Longo · 5 authors
Bug bounty programs are a popular solution for security researchers to disclose software vulnerabilities in exchange for compensation. They suffer, however, from two main drawbacks that limit their effectiveness: (i) they use a trusted intermediary that charges hefty commission fees and may have a conflict of interest with the software vendor, and (ii) they may mistreat security researchers by compensating less than guaranteed and no means to appeal against it. In this paper, we propose a permissioned Blockchain-based framework that addresses the drawbacks of existing bug bounty programs. The framework allows a confidential exchange of vulnerabilities and compensations using smart contracts. In cases of policy violation, security researchers can appeal to a trusted group of security experts called arbitrators, that can force the software vendors to compensate the security researchers fairly. A formal evaluation of the proposed framework using TLA+ specification supports the viability of the proposal. A Hyperledger Fabric-based prototype is implemented to simulate the proposed framework. The analysis of the framework uses a game-theoretic notion to argue that if the majority of arbitrators behave honestly, then the rational strategy of software vendors is to compensate security researchers that disclose vulnerabilities accurately. Similarly, rational security researchers do not gain any financial profit by playing unfairly.
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.
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.
Filippo Contro, Marco Crosara, Mariano Ceccato, Mila Dalla Preda
Motivated by the immutable nature of Ethereum smart contracts and of their\ntransactions, quite many approaches have been proposed to detect defects and\nsecurity problems before smart contracts become persistent in the blockchain\nand they are granted control on substantial financial value.\n Because smart contracts source code might not be available, static analysis\napproaches mostly face the challenge of analysing compiled Ethereum bytecode,\nthat is available directly from the official blockchain. However, due to the\nintrinsic complexity of Ethereum bytecode (especially in jump resolution),\nstatic analysis encounters significant obstacles that reduce the accuracy of\nexiting automated tools.\n This paper presents a novel static analysis algorithm based on the symbolic\nexecution of the Ethereum operand stack that allows us to resolve jumps in\nEthereum bytecode and to construct an accurate control-flow graph (CFG) of the\ncompiled smart contracts. EtherSolve is a prototype implementation of our\napproach. Experimental results on a significant set of real world Ethereum\nsmart contracts show that EtherSolve improves the accuracy of the execrated\nCFGs with respect to the state of the art available approaches.\n Many static analysis techniques are based on the CFG representation of the\ncode and would therefore benefit from the accurate extraction of the CFG. For\nexample, we implemented a simple extension of EtherSolve that allows to detect\ninstances of the re-entrancy vulnerability.\n
Abstract Blockchain‐based audit systems suffer from low scalability and high message complexity. The root cause of these shortcomings is the use of “Practical Byzantine Fault Tolerance” (PBFT) consensus protocol in those systems. Alternatives to PBFT have not been used in blockchain‐based audit systems due to the limited knowledge about their functional and operational requirements. Currently, no blockchain testbed supports the execution and benchmarking of different consensus protocols in a unified testing environment. This paper demonstrates building a blockchain testbed that supports the execution of five state‐of‐the‐art consensus protocols in a blockchain system; namely PBFT, Proof‐of‐Work (PoW), Proof‐of‐Stake (PoS), Proof‐of‐Elapsed Time (PoET), and Clique. Performance evaluation of those consensus algorithms is carried out using data from a real‐world audit system. These results show that the Clique protocol is best suited for blockchain‐based audit systems, based on scalability features.
Ryan Song, Zihan Zhao, Yuxi Cai, Andreas Veneris · 5 authors
This paper presents SigVM, a novel blockchain virtual machine that supports an event-driven execution model, enabling developers to build fully autonomous smart contracts. SigVM introduces another way for a contract to interact with another. Contracts in SigVM can emit signal events, on which other contracts can listen. Once an event is triggered, corresponding handler functions are automatically executed as signal transactions. We built an end-to-end blockchain platform SigChain and a contract language compiler SigSolid to realize the potential of SigVM. Experimental results show that SigVM enables contracts in our benchmark applications to be reimplemented in a fully autonomous way, eliminating the dependency on unreliable mechanisms like off-chain relay servers. SigVM can significantly simplify the execution flow of our benchmark applications, and can avoid security risks such as front-run attacks.
We propose three constructions of classically verifiable non-interactive zero-knowledge proofs and arguments (CV-NIZK) for QMA in various preprocessing models. - We construct a CV-NIZK for QMA in the quantum secret parameter model where a trusted setup sends a quantum proving key to the prover and a classical verification key to the verifier. It is information theoretically sound and zero-knowledge. - Assuming the quantum hardness of the learning with errors problem, we construct a CV-NIZK for QMA in a model where a trusted party generates a CRS and the verifier sends an instance-independent quantum message to the prover as preprocessing. This model is the same as one considered in the recent work by Coladangelo, Vidick, and Zhang (CRYPTO '20). Our construction has the so-called dual-mode property, which means that there are two computationally indistinguishable modes of generating CRS, and we have information theoretical soundness in one mode and information theoretical zero-knowledge property in the other. This answers an open problem left by Coladangelo et al, which is to achieve either of soundness or zero-knowledge information theoretically. To the best of our knowledge, ours is the first dual-mode NIZK for QMA in any kind of model. - We construct a CV-NIZK for QMA with quantum preprocessing in the quantum random oracle model. This quantum preprocessing is the one where the verifier sends a random Pauli-basis states to the prover. Our construction uses the Fiat-Shamir transformation. The quantum preprocessing can be replaced with the setup that distributes Bell pairs among the prover and the verifier, and therefore we solve the open problem by Broadbent and Grilo (FOCS '20) about the possibility of NIZK for QMA in the shared Bell pair model via the Fiat-Shamir transformation.
Michael Neuder, Daniel J. Moroz, Rithvik Rao, David C. Parkes
We outline two dishonest strategies that can be cheaply executed on the Ethereum 2.0 beacon chain, even by validators holding less than one-third of the total stake: malicious chain reorganizations ("reorgs") and finality delays. In a malicious reorg, an attacker withholds their blocks and attestations before releasing them at an opportune time in order to force a chain reorganization, which they can take advantage of by double-spending or front-running transactions. To execute a finality delay an attacker uses delayed block releases and withholding of attestations to increase the mean and variance of the time it takes blocks to become finalized. This impacts the efficiency and predictability of the system. We provide a probabilistic and cost analysis for each of these attacks, considering a validator with 30% of the total stake.