Blockchain platforms are coming into use for processing critical transactions among participants who have not established mutual trust. Many blockchains are programmable, supporting smart contracts , which maintain persistent state and support transactions that transform the state. Unfortunately, bugs in many smart contracts have been exploited by hackers. Obsidian is a novel programming language with a type system that enables static detection of bugs that are common in smart contracts today. Obsidian is based on a core calculus, Silica, for which we proved type soundness. Obsidian uses typestate to detect improper state manipulation and uses linear types to detect abuse of assets. We integrated a permissions system that encodes a notion of ownership to allow for safe, flexible aliasing. We describe two case studies that evaluate Obsidian’s applicability to the domains of parametric insurance and supply chain management, finding that Obsidian’s type system facilitates reasoning about high-level states and ownership of resources. We compared our Obsidian implementation to a Solidity implementation, observing that the Solidity implementation requires much boilerplate checking and tracking of state, whereas Obsidian does this work statically.
Neville Grech, Michael Kong, Anton Jurisevic, Lexi Brent · 6 authors
Ethereum is a distributed blockchain platform, serving as an ecosystem for smart contracts: full-fledged intercommunicating programs that capture the transaction logic of an account. A gas limit caps the execution of an Ethereum smart contract: instructions, when executed, consume gas, and the execution proceeds as long as gas is available. Gas-focused vulnerabilities permit an attacker to force key contract functionality to run out of gas---effectively performing a permanent denial-of-service attack on the contract. Such vulnerabilities are among the hardest for programmers to protect against, as out-of-gas behavior may be uncommon in nonattack scenarios and reasoning about these vulnerabilities is nontrivial. In this paper, we identify gas-focused vulnerabilities and present MadMax: a static program analysis technique that automatically detects gas-focused vulnerabilities with very high confidence. MadMax combines a smart contract decompiler and semantic queries in Datalog. Our approach captures high-level program modeling concepts (such as "dynamic data structure storage" and "safely resumable loops") and delivers high precision and scalability. MadMax analyzes the entirety of smart contracts in the Ethereum blockchain in just 10 hours and flags vulnerabilities in contracts with a monetary value in billions of dollars. Manual inspection of a sample of flagged contracts shows that 81% of the sampled warnings do indeed lead to vulnerabilities.
The CAP theorem says that no blockchain can be live under dynamic participation and safe under temporary network partitions. To resolve this availability-finality dilemma, we formulate a new class of flexible consensus protocols, ebb-and-flow protocols, which support a full dynamically available ledger in conjunction with a finalized prefix ledger. The finalized ledger falls behind the full ledger when the network partitions but catches up when the network heals. Gasper, the current candidate protocol for Ethereum 2.0's beacon chain, combines the finality gadget Casper FFG with the LMD GHOST fork choice rule and aims to achieve this property. However, we discovered an attack in the standard synchronous network model, highlighting a general difficulty with existing finality-gadget-based designs. We present a construction of provably secure ebb-and-flow protocols with optimal resilience. Nodes run an off-the-shelf dynamically available protocol, take snapshots of the growing available ledger, and input them into a separate off-the-shelf BFT protocol to finalize a prefix. We explore connections with flexible BFT and improve upon the state-of-the-art for that problem.
Jiachi Chen, Xin Xia, David Lo, John Grundy · 6 authors
Smart contracts are Turing-complete programs running on the blockchain. They are immutable and cannot be modified, even when bugs are detected. Therefore, ensuring smart contracts are bug-free and well-designed before deploying them to the blockchain is extremely important. A contract defect is an error, flaw or fault in a smart contract that causes it to produce an incorrect or unexpected result, or to behave in unintended ways. Detecting and removing contract defects can avoid potential bugs and make programs more robust. Our previous work defined 20 contract defects for smart contracts and divided them into five impact levels. According to our classification, contract defects with seriousness level between 1-3 can lead to unwanted behaviors, e.g., a contract being controlled by attackers. In this paper, we proposeDefectChecker, a symbolic execution-based approach and tool to detect eight contract defects that can cause unwanted behaviors of smart contracts on the Ethereum blockchain platform.DefectCheckercan detect contract defects from smart contracts’ bytecode. We verify the performance ofDefectCheckerby applying it to an open-source dataset. Our evaluation results show thatDefectCheckerobtains a high F-score (88.8 percent in the whole dataset) and only requires 0.15s to analyze one smart contract on average. We also appliedDefectCheckerto 165,621 distinct smart contracts on the Ethereum platform. We found that 25,815 of these smart contracts contain at least one of the contract defects that belongs to impact level 1-3, including some real-world attacks.
We facilitate trusted cross-blockchain state proofs by implementing a chain-relay that validates block headers from proof-of-work blockchains. While current approaches require proof sizes linear to the amount of blocks the state was built on, trusted intermediaries, or economic assumptions, we propose the utilization of off-chain computations through zkSNARKs to provide a cryptographically secure and highly scalable sidechain mechanism. Multiple block headers are included in batches and verified off-chain, while preserving light client support. Only the validity of the off-chain computation is verified on-chain, creating a sidechain mechanism that requires constant verification costs and releases the target ledger from processing and storing every single block header of the source blockchain. Efficient Merkle proofs enable including intermediary blocks for any batch that was submitted. We provide a prototypical implementation that facilitates the verification of 504 Bitcoin headers in a single proof on Ethereum using the ZoKrates framework. Hereby, the verification costs are reduced by a factor of 187 compared to current approaches such as BTC Relay.
Among all ongoing attacks on mobile, those targeting blockchain-wallet applications raise pressing concerns due to the risks of potential monetary loss. These attacks mainly focus on the theft and forwarding of keys in executable files. The challenge is that these malicious code behaviors are not detectable with the usual detection methods. We propose in this article the implementation of an unpacking system to the intelligent block-chain applications: AutoD, based on the JNI layer deception-call in Android ART. This solution can successfully restore the decrypted Dex file during the execution of the reinforced blockchain applications. The core idea is to first transfer the Dex from memory to the sdcard completely according to the DexFile structure. Then through deception-calling on every method of every class, AutoD successfully repairs the function-extracting protection component in Dex. Experimental results show that AutoD offers full repair on the function-ex-tracting protection component, where most of the malicious code usually hides.
This thesis addresses computer security problems in: Access Control, Ethereum Smart Contracts, Cloud VM Scheduling, and Logic Locking. These problems are solved using polynomially timed reductions to 2 complexity classes: PSPACE-Complete and NP-Complete. This thesis is divided into 2 parts, problems reduced to: Model Checking (PSPACE-Complete) and Integer Linear Programming (ILP) (NP-Complete). The PSPACE-Complete problems are: Safety Analysis of Administrative Temporal Role Based Access Control (ATRBAC) Policies, and Safety Analysis of Ethereum Smart Contracts. The NP-Complete problems are: Minimizing Information Leakage in Virtual Machine (VM) Cloud Environments using VM Migrations, and Attacking Logic Locked Circuits using a Reduction to Integer Linear Programming (ILP). \n \nIn Chapter 3, I create the Cree Administrative Temporal Role Based Access Control (ATRBAC)-Safety solver. Which is a reduction from ATRBAC-Safety to Model Checking. I create 4 general performance techniques which can be utilized in any ATRBAC-Safety solver. \n \n 1. Polynomial Time Solving, which is able to solve specific archetypes of ATRBAC-Safety policies using a polynomial timed algorithm. \n 2. Static Pruning, which includes 2 methods for reducing the size of the policy without effecting the result of the safety query. \n 3. Abstraction Refinement, which can increase the speed for reachable safety queries by only solving a subset of the original policy. \n 4. Bound Estimation, which creates a bound on the number of steps from the initial state, where a satisfying state must exist. This is directly used by the model checker's bounded model checking mode, but can be utilized by any solver with a bound limiting parameter. \n \nIn Chapter 4, I analyze ATRBAC-Safety policies to identify some of the ``sources of complexity'' which make solving ATRBAC-Safety policies difficult. I provide analysis of the sources of complexity that exists in the previously published datasets [128,90,54]. I perform analysis of Cree's performance techniques on the previous datasets. I create 2 new datasets, which are shown to be hard instances of ATRBAC-Safety. I analyze the new datasets to show how they achieve this hardness and how they differ from each other and the previous datasets. \n \nIn Chapter 5, I create a novel reduction from a Reduced-Solidity Smart Contract, subset of available Solidity features, to Model Checking. This reduction reduces Reduced-Solidity Smart Contract into a Finite State Machine and then reduces to an instance of a Model Checking problem. This provides the ability to test smart contracts published on the Ethereum blockchain and test if there exists bugs or malicious code. I perform empirical analysis on select Smart contracts. \n \nIn Chapter 6, I create 2 methods for generating instances of ATRBAC policies into Solidity Smart Contracts. The first method is the Generic ATRBAC Smart Contract. This method requires no modification before deployment. After deployed the owner is able to create, and maintain, the policy using special access functions. The special action functions are automated with code that converts an ATRBAC policy into a series of transactions the owner can run. The second method is the Baked ATRBAC Smart Contract. This method takes an ATRBAC policy and reduces it to a Smart Contract instance with no special access functions. The smart contract can then be deployed by anyone, and that person will have no special access. I perform an empirical analysis on the setup costs, transaction costs, and security each provides. \n \nIn Chapter 7, I create a new reduction from Minimizing Information Leakage via Virtual Machine (VM) Migrations to Integer Linear Programming (ILP). I compare a polynomial algorithm by Moon et. al. [71], my ILP reduction, and a reduction to CNF-SAT that is not included in this thesis. The polynomial method is faster, but the problem is NP-Complete thus that solution must have sacrificed something to obtain the polynomial time speed (unless P = NP). I show instances in which the polynomial time algorithm does not produce the minimum total information leakage, but the ILP and CNF-SAT reductions are able to. In addition to this, I show that Total Information Leakage also has a security vulnerability for non-zero information leakage using the <R,C> model. I propose an alternative method to Total Information Leakage, called Max Client-to-Client Information Leakage, which removes the vulnerability at the cost of increased total information leakage. \n \nIn Chapter 8, I create a reduction from the Key Recovery Attack on Logic Locked Circuits to Integer Linear Programming (ILP). This is a recreation of the ``SAT Attack'' using ILP. I provide an empirical analysis of the ILP attack and compare it to the SAT-Attack. I show that ``ILP Attack'' is a viable attack, thus future claims of ``SAT-Attack Resistant Logic Locking Techniques'' need to also show resistance to all potential NP-Complete attacks.
Christina Muller, Marcus Brandenburger, Christian Cachin, Pascal Felber · 6 authors
Blockchain technology promises to revolutionize manufacturing industries. For example, several supply-chain use-cases may benefit from transparent asset tracking and automated processes using smart contracts. Several real-world deployments exist where the transparency aspect of a blockchain is both an advantage and a disadvantage at the same time. The exposure of assets and business interaction represent critical risks. However, there are typically no confidentiality guarantees to protect the smart contract logic as well as the processed data. Trusted execution environments (TEE) are an emerging technology available in both edge or mobile-grade processors (e.g., Arm TrustZone) and server-grade processors (e.g., Intel SGX). TEEs shield both code and data from malicious attackers. This practical experience report presents TZ4Fabric, an extension of Hyperledger Fabric to leverage Arm TrustZone for the secure execution of smart contracts. Our design minimizes the trusted computing base executed by avoiding the execution of a whole Hyperledger Fabric node inside the TEE, which continues to run in untrusted environment. Instead, we restrict it to the execution of only the smart contract. The TZ4Fabric prototype exploits the open-source OP-TEE framework, as it supports deployments on cheap low-end devices (e.g., Raspberry Pis). Our experimental results highlight the performance trade-off due to the additional security guarantees provided by Arm TrustZone. TZ4Fabric will be released as open-source.
From the lessons that can be learned so far in this book, the author justifies why a new strategy is required to refocus our perception and utilization of computerized capabilities in the future. Chapter 8 focuses on the advancement of the cyber security discipline by determining trust-less control-sets – a fourth dimension if you will, comprising blockchain technology. Blockchain has been implemented in fungible forms, such as public bitcoin and Ethereum, and in a non-fungible manner like private keyless signature infrastructure. It is the latter that is of particular interest, where proven implementations have the potential to demonstrably act as a verifiable trust anchor, embellishing cyber security controls in a number of critical areas to ensure (1) preservation of data integrity, (2) digital finger printing of IoT assets to prove the source of data is trustworthy, (3) validation of identity and access management mechanisms, and (4) software provenance in the supply chain for not only traditional code-bases but also AI algorithms.
Vaivaswatha Nagaraj, Jacob Johannsen, Anton Trunov, George Pîrlea · 6 authors
Scilla is a higher-order polymorphic typed intermediate level language for implementing smart contracts. In this talk, we describe a Scilla compiler targeting LLVM, with a focus on mapping Scilla types, values, and its functional language constructs to LLVM-IR. The compiled LLVM-IR, when executed with LLVM's JIT framework, achieves a speedup of about 10x over the reference interpreter on a typical Scilla contract. This reduced latency is crucial in the setting of blockchains, where smart contracts are executed as parts of transactions, to achieve peak transactions processed per second. Experiments on the Ackermann function achieved a speedup of more than 45x. This talk abstract is aimed at both programming language researchers looking to implement an LLVM based compiler for their functional language, as well as at LLVM practitioners.
Gerardo Canfora, Andrea Di Sorbo, Sonia Laudanna, Anna Vacca · 5 authors
Nowadays, blockchain technologies are increasingly adopted for different purposes and in different application domains. Accordingly, more and more applications are developed for running on a distributed ledger technology (i.e., \textit{dApps}). The business logic of a dApp (or part of it) is usually implemented within one (or more) smart contract(s) developed through Solidity, an object-oriented programming language for writing smart contracts on different blockchain platforms, including the popular Ethereum. In Ethereum, once compiled, the smart contracts run on the machines of miners who can earn Ethers (a cryptographic currency like Bitcoin) by contributing their computing resources and the \textit{gas} (in Ether) corresponds to the execution fee compensating such computing resources. However, the deployment and execution costs of a smart contract strictly depend on the choices done by developers while implementing it. Unappropriated design choices -- e.g., in the data structures and the specific instructions used -- could lead to higher gas consumption than necessary. In this paper, we systematically identify a set of 20 Solidity code smells that could affect the deployment and transaction costs of a smart contract, i.e., \textit{cost smells}. On top of these smells, we propose GasMet, a suite of metrics for statically evaluating the code quality of a smart contract, from the gas consumption perspective. In an experiment involving 2,186 real-world smart contracts, we demonstrate that the proposed metrics (i) have direct associations with deployment costs, and (ii) they could be used to properly identify the level of gas consumption of a smart contract without the need for deploying it.
Palina Tolmach, Yi Li, Shang‐Wei Lin, Yang Liu · 5 authors
A smart contract is a computer program which allows users to automate their actions on the blockchain platform. Given the significance of smart contracts in supporting important activities across industry sectors including supply chain, finance, legal and medical services, there is a strong demand for verification and validation techniques. Yet, the vast majority of smart contracts lack any kind of formal specification, which is essential for establishing their correctness. In this survey, we investigate formal models and specifications of smart contracts presented in the literature and present a systematic overview in order to understand the common trends. We also discuss the current approaches used in verifying such property specifications and identify gaps with the hope to recognize promising directions for future work.
A smart contract is a software program that runs on top of a blockchain. It contains a collection of public functions that can be invoked within the transactions launched over the contract by parties interacting with it. Being computer programs, well-studied formal verification techniques can be applied to them. Indeed, smart contracts are a very interesting application domain for validation, verification and optimization techniques since (1) they are relatively small in size, hence the application of these techniques scales better than when applied to larger industrial code, (2) they are valuable (in the corresponding blockchain cryptocurrency), hence software bugs or inefficiencies can cause economical losses and there is much interest in formally proving their safety and security, and (3) they require proving new specific properties to ensure their reliability and efficiency.
Aug 1, 2020·2020 7th IEEE International Conference on Cyber Security and Cloud Computing (CSCloud)/2020 6th IEEE International Conference on Edge Computing and Scalable Cloud (EdgeCom)
Despite the increased accuracy of intrusion detection systems (IDS) in identifying cyberattacks in computer networks and devices connected to the internet, distributed or coordinated attacks can still go undetected or not detected on time. The single vantage point limits the ability of these IDSs to detect such attacks. Due to this reason, there is a need for attack characteristics’ exchange among different IDS nodes. Researchers proposed a cooperative intrusion detection system to share these attack characteristics effectively. This approach was useful; however, the security of the shared data cannot be guaranteed. More specifically, maintaining the integrity and consistency of shared data becomes a significant concern. In this paper, we propose a blockchain-based solution that ensures the integrity and consistency of attack characteristics shared in a cooperative intrusion detection system. The proposed architecture achieves this by detecting and preventing fake features injection and compromised IDS nodes. It also facilitates scalable attack features exchange among IDS nodes, ensures heterogeneous IDS nodes participation, and it is robust to public IDS nodes joining and leaving the network. We evaluate the security analysis and latency. The result shows that the proposed approach detects and prevents compromised IDS nodes, malicious features injection, manipulation, or deletion, and it is also scalable with low latency.
The promise of disparate features envisioned by the 3GPP for 5G, such as offering enhanced Mobile Broadband connectivity while providing massive Machine Type Communications likely with very low data rates and maintaining Ultra Reliable Low Latency Communications requirements, create a very challenging environment for protecting the 5G networks themselves and associated assets. To overcome such complexity, future 5G networks must employ a very high degree of network and service management automation, which is a security challenge by itself as well as an opportunity for smarter and more efficient security functions. In this paper, we present the smart, trustworthy and liable 5G security platform being designed and developed in the INSPIRE-5Gplus1 project. This platform takes advantage of new techniques such as Machine Learning (ML), Artificial Intelligence (AI), Distributed Ledger Technologies (DLT), network softwarization and Trusted Execution Environment (TEE) for closed-loop and end-to-end security management following a zero-touch model in 5G and Beyond 5G networks. To this end, we specifically elaborate on two key aspects of our platform, namely security management with Security Service Level Agreements (SSLAs) and liability management, in addition to the description of the overall architecture.
Smart contracting protocols promise to regulate the transfer of cryptocurrency amongst participants in a trustless manner. A safe smart contract implementation should ensure that each participant can always append a contract transaction to the blockchain in order move the contract towards secure completion. To this goal, we propose Bitcoin Trace-Net, a contract verification framework which generates an executable symbolic model from the underlying contract implementation. A Trace-Net model consists of a Petri Net formalism enriched with a Dolev-Yao-like actor knowledge model. The explicit symbolic actor knowledge model supports the verification of contracts featuring cryptographic sub-protocols, which may not be observable on the blockchain. Trace-Net is sufficiently expressive to accurately model blockchain semantics such as the delay between a transaction broadcast and its subsequent confirmation, as well as adversarial blockchain reorganizations of finite depths, both of which can break smart contract safety. As an implementation level framework, Trace-Net can be instantiated at run-time to monitor and verify smart contract protocol executions.
The need for data trading promotes the emergence of data market. However, in conventional data markets, both data buyers and data sellers have to use a centralized trading platform which might be dishonest. A dishonest centralized trading platform may steal and resell the data seller's data, or may refuse to send data after receiving payment from the data buyer. It seriously affects the fair data transaction and harm the interests of both parties to the transaction. To address this issue, we propose a novel blockchain-based data trading framework with Trusted Execution Environment (TEE) to provide a trusted decentralized platform for fair data trading. In our design, a blockchain network is proposed to realize the payments from data buyers to data sellers, and a trusted exchange is built by using a TEE for the first time to achieve fair data transmission. With these help, data buyers and data sellers can conduct transactions directly. We implement our proposed framework on Ethereum and Intel SGX, security analysis and experimental results have demonstrated that the framework proposed can effectively guarantee the fair completion of data tradings.
Ashish Rajendra Sai, Conor Holmes, Jim Buckley, Andrew Le Gear
Blockchain systems have gained substantial traction recently, partly due to the potential of decentralized immutable mediation of economic activities. Ethereum is a prominent example that has the provision for executing stateful computing scripts known as Smart Contracts. These smart contracts resemble traditional programs, but with immutability being the core differentiating factor. Given their immutability and potential high monetary value, it becomes imperative to develop high-quality smart contracts. Software metrics have traditionally been an essential tool in determining programming quality. Given the similarity between smart contracts (written in Solidity for Ethereum) and object-oriented (OO) programming, OO metrics would appear applicable. In this paper, we empirically evaluate inheritance-based metrics as applied to smart contracts. We adopt this focus because, traditionally, inheritance has been linked to a more complex codebase which we posit is not the case with Solidity based smart contracts. In this work, we evaluate the hypothesis that, due to the differences in the context of smart contracts and OO programs, it may not be appropriate to use the same interpretation of inheritance based metrics for assessment.
Gustavo Grieco, Will Song, Artur Cygan, Josselin Feist · 5 authors
Ethereum smart contracts---autonomous programs that run on a blockchain---often control transactions of financial and intellectual property. Because of the critical role they play, smart contracts need complete, comprehensive, and effective test generation. This paper introduces an open-source smart contract fuzzer called Echidna that makes it easy to automatically generate tests to detect violations in assertions and custom properties. Echidna is easy to install and does not require a complex configuration or deployment of contracts to a local blockchain. It offers responsive feedback, captures many property violations, and its default settings are calibrated based on experimental data. To date, Echidna has been used in more than 10 large paid security audits, and feedback from those audits has driven the features and user experience of Echidna, both in terms of practical usability (e.g., smart contract frameworks like Truffle and Embark) and test generation strategies. Echidna aims to be good at finding real bugs in smart contracts, with minimal user effort and maximal speed.
Access control plays a crucial role in constructing trust in a system. Particularly, it is imperative to enforce a fine-grained access control mechanism to make the access control framework flexible due to the high complexity of untrustworthy environments such as the Internet of Things (IoT) environments. However, traditional access control techniques can be hardly trusted on account of their centralized enforcements and improper distributed computing mechanisms while facing diverse and intricate threats. Although existing solutions based on public blockchain technology have addressed some issues, new challenges derived from public blockchain technology become noticeable such as low consensus efficiency and delicate incentive mechanism. In this paper, we propose Bloccess, a fine-grained access control framework using permissioned blockchain techniques, which enhances the trust in untrustworthy environments by enforcing a trustworthy access control mechanism. Bloccess provides a unified and user-centric solution for access control in distributed untrustworthy environments and optimizes the decentralized access control management, which significantly ensures the security properties of protected environments in terms of the threat model structured in this paper. We also prove the feasibility and effectiveness of Bloccess by security analysis and the comparison with some related frameworks.
João F. Ferreira, Pedro E. D. Cruz, Thomas Durieux, Abreu, Rui
Over the last few years, there has been substantial research on automated analysis, testing, and debugging of Ethereum smart contracts. However, it is not trivial to compare and reproduce that research. To address this, we present SmartBugs, an extensible and easy-to-use execution framework that simplifies the execution of analysis tools on smart contracts written in Solidity, the primary language used in Ethereum. SmartBugs is currently distributed with support for 10 tools and two datasets of Solidity contracts. The first dataset can be used to evaluate the precision of analysis tools, as it contains 143 annotated vulnerable contracts with 208 tagged vulnerabilities. The second dataset contains 47,518 unique contracts collected through Etherscan. We discuss how SmartBugs supported the largest experimental setup to date both in the number of tools and in execution time. Moreover, we show how it enables easy integration and comparison of analysis tools by presenting a new extension to the tool SmartCheck that improves substantially the detection of vulnerabilities related to the DASP10 categories Bad Randomness, Time Manipulation, and Access Control (identified vulnerabilities increased from 11% to 24%).
Non-fungible tokens are an up and coming application domain for smart contracts. Ethereum is the first blockchain-based decentralized computing platform that has standardized this type of tokens into a well-defined interface, namely ERC721. We propose a framework that provides developers with a smart contract suite that offers complete implementations of the ERC721 standard and common extensions and features frequently encountered in ERC721-based applications. We introduce a specification language that enables customization and configuration of the smart contract suite by including and excluding the supported features and extensions. We evaluate the smart contract suite for its extensibility and reusability and compare the metrics with four reference implementations tackling a similar problem. In addition to this, we evaluate and analyze the effort and efficiency of the specification language in comparison to manual configuration of the smart contract suite. Our contribution lies in examining quality metrics for code extensibility and reusability and determining the more insightful metrics for assessing these quality attributes in the context of Solidity smart contracts. Additionally, from the lines of code metric, We conclude that our specification language offers a simple and efficient alternative to manual smart contract suite customization.