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.
Madhumitha Harishankar, Jinhang Zuo, Sriram V. Iyer, Patrick Tague · 5 authors
Relying on dedicated contracts with specific network operators for Internet access significantly limits connectivity options for devices. As new usecases for internet access emerge, e.g., with the Internet of Things in smart-cities, managing such individual contracts for each deployed device with varying data needs is prohibitively cumbersome and highly expensive. In this work, we enable contract-less connectivity between end-devices and access points/networks that have no a-priori trust relationship. Our core insight is that exchange of services and payments can be trustlessly enforced by distributed ledger technologies; the credentials that blockchains use for account management can also be used for TLS-based authentication in networks. However, the blockchain's ability to enforce transaction rules is limited by the extent to which the underlying exchange of services is digitally trackable, which is susceptible to manipulation in this case. Requiring blockchain-integrated trusted hardware at the access points for bandwidth metering significantly hinders adoption; even software modifications required at the access points to process blockchain-based auth and payments incur practical deployment and scalability challenges. In designing Datanet, we address these challenges and enable seamless and incentivized connectivity between unknown end-devices and APs, using existing standards that allow for interoperability with current and future networks, and without significant overhead for client devices.
Yankai Xie, Chi Zhang, Lingbo Wei, Qingtao Wang · 5 authors
Hardware trusted execution environment (TEE) provided by Intel SGX enclave has been introduced in existing payment channel schemes as a root-of-trust to enforce faithful protocol execution so that participants do not need to monitor Bitcoin blockchain anymore. However, the security of these schemes relies totally on enclaves. Since private keys of all channel funds are kept by both payment channel participants’ enclaves, a malicious participant can steal funds from the counterparty by defeating her own enclave. To solve the above problem, we present a novel TEE-based payment channel scheme that transfers the responsibility of running enclaves from participants to a third party committee, while relieving both participants from monitoring the blockchain at the same time. Furthermore, since committee members can try to steal funds by defeating their own enclaves, we exploit the additive homomorphic property of signature keys in Elliptic Curve Cryptography to design a novel secret sharing scheme to tolerate a subset of committee members to be malicious. By using the above secret sharing scheme, private keys of the channel funds are never constructed in any committee member’s enclave, so that a malicious committee member cannot steal funds by defeating his own enclave. Finally, experiment shows our scheme can ensure payment channel funds security without efficient compromises compared with existing TEE-based payment channel schemes.
Security and Verification in Computing
Blockchain Technology Applications and Security
Physical Unclonable Functions (PUFs) and Hardware Security
This paper proposes a new approach and tool for blockchain software developers and architects to use for determining which computations of a smart contract can be effectively done off-chain without loss of trust and how they can be moved off-chain automatically. Our approach uses Finite State Machines (FSMs) and Hierarchical State Machines (HSMs) modeling in order to create smart contract patterns using graphs and then use pattern properties to identify which parts of the smart contracts should be considered for moving off-chain. Once software execution transits into the pattern's entry state, off-chain execution continues until the execution transits into the pattern's exit state, when execution continues on-chain. This paper further describes a tool for (1) FSM input and visualization, its analysis, and automatic transformation into a smart contract, and (2) an interface to support the developers' decision to optimally off-chain computations and to (3) define the communications between on-chain and off-chain computations.
Damiano Di Francesco Maesa, Frank Tietze, Julius Theye
Our proposal aims to help solving a trust problem between licensors and licensees that occurs during the active life of license agreements. We particularly focus on licensing of proprietary intellectual property (IP) that is embedded in Internet of Things (IoT) devices and services (e.g. patented technologies). To achieve this we propose to encode the logic of license agreements into smart licenses (SL). We define a SL as a `digital twin' of a licensing contract, i.e. one or more smart contracts that represent the full or relevant parts of a licensing agreement in machine readable and executable code. As SL are self enforcing, the royalty computation and execution of payments can be fully automated in a tamper free and trustworthy way. This of course, requires to employ a Distributed Ledger Technology (DLT). Such an Automated Licensing Payment System (ALPS) can thus automate an established business process and solve a longstanding trust issue in licensing markets. It renders traditional costly audits obsolete, lowers entry barriers for those who want to participate in licensing markets, and enables novel business models too complex with traditional approaches.
Public Blockchains (BC) in support of Smart Contracts (SC), e.g., Ethereum, enable everyone to coordinate in a decentralized model to manage scarce and valuable resources,e.g., cryptocurrencies. Such BCs allow for the building of SCs that own resources and manage a set of permissions describing who is allowed to interact with these resources and what actions they can apply to them. However, Programming Languages (PL) and run-time systems used in current BCs lack a secure, flexible, and straightforward way to implement permissions within their SCs, leading to erroneous implementations that allow unauthorized access. The best-known incident related to a permission problem was the "Parity Hack", which led to the "loss" of tokens, valued at approximately 31 M USD.A better and secure SC access control concept provides an improved path to managing permissions. Thus, this paper presents a novel concept for handling permissions compatible with functional SC languages leveraging opaque and substructural data types to provide capability-based permission management. The opaque data types enforce that only designated functions can create permission carrying capabilities. Substructural data types prevent an unpermitted duplication of capabilities.
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.
David Heath, Yibin Yang, David Devecsery, Vladimir Kolesnikov
We build a complete and efficient ZK toolchain that handles proof statements encoded as arbitrary ANSI C programs.Zero-Knowledge (ZK) proofs are foundational in cryptography. Recent ZK research has focused intensely on non-interactive proofs of small statements, useful in blockchain scenarios. We instead target large statements that are useful, e.g., in proving properties of programs.Recent work (Heath and Kolesnikov, CCS 2020 [HK20a]) designed an efficient proof-of-concept ZK machine (ZKM). Their machine executes arbitrary programs over a minimal instruction set, authenticating in ZK the program execution. In this work, we significantly extend this research thrust, both in terms of efficiency and generality. Our contributions include:• A rich and performance-oriented architecture for representing arbitrary ZK proofs as programs.• A complete compiler toolchain providing full support for ANSI C95 programs. We ran off-the-shelf buggy versions of the Linux programs sed and gzip, proving in ZK that each program has a bug. To our knowledge, this is the first ZK system capable of executing standard Linux programs.• Improved ZK oblivious RAM (ORAM). [HK20a] introduced an efficient ZK-specific ORAM BubbleRAM that consumes O(log2n) communication per access. We extend BubbleRAM with multi-level caching, decreasing communication to O(log n) per access. This introduces the possibility of a cache miss, which we handle cheaply. Our experiments show that cache misses are rare; in isolation, i.e., ignoring other processor costs, BubbleCache improves communication over BubbleRAM by more than 8×. Using BubbleCache improves our processor’s total communication (including costs of cache misses) by ≈ 25-30%.• Numerous low-level optimizations, resulting in a CPU that is both more expressive and ≈ 5.5× faster than [HK20a]’s.• Attention to user experience. Our engineer-facing ZK instrumentation and extensions are minimal and easy to use.Put together, our system is efficient and general, and can run many standard Linux programs. The resultant machine runs at up to 11KHz on a 1Gbps LAN and supports MBs of RAM.
Efficient zero-knowledge (ZK) proofs for arbitrary boolean or arithmetic circuits have recently attracted much attention. Existing solutions suffer from either significant prover overhead (i.e., high memory usage) or relatively high communication complexity (at least κ bits per gate, for computational security parameter κ). In this paper, we propose a new protocol for constant-round interactive ZK proofs that simultaneously allows for an efficient prover with asymptotically optimal memory usage and significantly lower communication compared to protocols with similar memory efficiency. Specifically:•The prover in our ZK protocol has linear running time and, perhaps more importantly, memory usage linear in the memory needed to evaluate the circuit non-cryptographically. This allows our proof system to scale easily to very large circuits.•for statistical security parameter ρ = 40, our ZK protocol communicates roughly 9 bits/gate for boolean circuits and 2–4 field elements/gate for arithmetic circuits over large fields.Using 5 threads, 400 MB of memory, and a 200 Mbps network to evaluate a circuit with hundreds of billions of gates, our implementation (ρ = 40, κ = 128) runs at a rate of 0.45 μs/gate in the boolean case, and 1.6 μs/gate for an arithmetic circuit over a 61-bit field.We also present an improved subfield Vector Oblivious Linear Evaluation (sVOLE) protocol with malicious security that is of independent interest.
Jon Stephens, Kostas Ferles, Benjamin Mariano, Shuvendu K. Lahiri · 5 authors
Smart contracts are programs that run on the blockchain and digitally enforce the execution of contracts between parties. Because bugs in smart contracts can have serious monetary consequences, ensuring the correctness of such software is of utmost importance. In this paper, we present a novel technique, and its implementation in a tool called SMARTPULSE, for automatically verifying temporal properties in smart contracts. SMARTPULSE is the first smart contract verification tool that is capable of checking liveness properties, which ensure that "something good" will eventually happen (e.g., "I will eventually receive my refund"). We experimentally evaluate SMARTPULSE on a broad class of smart contracts and properties and show that (a) SMARTPULSE allows automatically verifying important liveness properties, (b) it is competitive with or better than state-of-the-art tools for safety verification, and (c) it can automatically generate attacks for vulnerable contracts.
Christopher M. VanYe, Beatrice Li, Andrew Koch, Mai N. Luu · 12 authors
This paper addresses security and risk management of hardware and embedded systems across several applications. There are three companies involved in the research. First is an energy technology company that aims to leverage electric- vehicle batteries through vehicle to grid (V2G) services in order to provide energy storage for electric grids. Second is a defense contracting company that provides acquisition support for the DOD's conventional prompt global strike program (CPGS). These systems need protections in their production and supply chains, as well as throughout their system life cycles. Third is a company that deals with trust and security in advanced logistics systems generally. The rise of interconnected devices has led to growth in systems security issues such as privacy, authentication, and secure storage of data. A risk analysis via scenario-based preferences is aided by a literature review and industry experts. The analysis is divided into various sections of Criteria, Initiatives, C-I Assessment, Emergent Conditions (EC), Criteria-Scenario (C-S) relevance and EC Grouping. System success criteria, research initiatives, and risks to the system are compiled. In the C-I Assessment, a rating is assigned to signify the degree to which criteria are addressed by initiatives, including research and development, government programs, industry resources, security countermeasures, education and training, etc. To understand risks of emergent conditions, a list of Potential Scenarios is developed across innovations, environments, missions, populations and workforce behaviors, obsolescence, adversaries, etc. The C-S Relevance rates how the scenarios affect the relevance of the success criteria, including cost, schedule, security, return on investment, and cascading effects. The Emergent Condition Grouping (ECG) collates the emergent conditions with the scenarios. The generated results focus on ranking Initiatives based on their ability to negate the effects of Emergent Conditions, as well as producing a disruption score to compare a Potential Scenario's impacts to the ranking of Initiatives. The results presented in this paper are applicable to the testing and evaluation of security and risk for a variety of embedded smart devices and should be of interest to developers, owners, and operators of critical infrastructure systems.
Physical Unclonable Functions (PUFs) and Hardware Security
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.
Blockchain is widely used nowadays and it is expected to be more exploited in the near future. Blockchain tends to be more used due to its security layer beyond any active component. Therefore, companies are relying on cutting expenses through converging to the blockchain network and to stop relying on traditional security components due to their high costs and security concerns. The Blockchain technology provides several advantages therefore more applications will be leveraging Distributed Ledger Technologies (DLTs) in the upcoming future. The current work is focused around tackling the use of Blockchain for Cyber Threat Intelligence (CTI) sharing providing a new means to disseminate securely threats data between Security Operations Center (SOC) teams.
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).
Since there are no security concerns such as Sybil attacks, selfish mining, etc., the higher the system throughput, the better for the permissioned blockchain. And with the emergence of consensus algorithms, the throughput rates of permissioned blockchain can be up to thousands of transactions per second. The existing serial execution method for smart contracts becomes a new bottleneck for the system. Due to the lack of mutual trust between nodes, for a batch of smart contracts contained in a block, the traditional two-phase smart contract concurrency approach can only achieve concurrency within a single node, but not the parallel execution of contracts between nodes. In this paper, we propose a new two-phase framework based on trusted hardware Intel SGX, which can avoid the re-execution of all smart contracts on all nodes and improve parallelism between nodes. And consistency between nodes is achieved directly with state replication, rather than by re-executing transactions. We design a pre-execution mechanism for smart contracts in untrusted memory to batch fetch all the state data that a smart contract needs to access to reduce frequent enclave transitions during smart contract execution. Besides, we propose a method that generates a compact read-write set and a data structure named Merkle Forest which can generate the compact Merkle multiproofs for the initial data in untrusted memory in parallel and can quickly verify the correctness of the data passed in the enclave. Finally, we integrate all the techniques proposed in this paper into an open-source system BFT-SMaRt to evaluate our approach in a distributed setting. Experimental results show the efficiency of the proposed methods.
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.