Beyond an emerging popular web applications runtime supported in almost all commodity browsers, WebAssembly (WASM) is further regarded to be the next-generation execution environment for blockchain-based applications. Indeed, many popular blockchain platforms such as EOSIO and NEAR have adopted WASM-based execution engines. Most recently, WASM has been favored by Ethereum, the largest smart contract platform, to replace the state-of-the-art EVM. However, whether and how well current WASM outperforms EVM on blockchain clients is still unknown. This article conducts the first measurement study to understand the performance on WASM VMs and EVM for executing smart contracts for blockchain-based applications. To our surprise, the current WASM VM does not provide expected satisfactory performance. The overhead introduced by WASM is really non-trivial. Our results shed the light on challenges when deploying WASM in practice, and provide insightful implications for improvement space.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.