We provide enhanced security against insider attacks in services that manage extremely sensitive data. One example is a #MeToo use case where sexual harassment complaints are reported but only revealed when another complaint is filed against the same perpetrator. Such a service places tremendous trust on service operators which our work aims to relieve. To this end we introduce a new autonomous data management concept which transfers responsibility for the sensitive data from administrators to secure and verifiable hardware. The main idea is to manage all data access via a cluster of autonomous computation agents running inside Intel SGX enclaves. These EConfidante agents share a secret data key which is unknown to any external entity, including the data service administrators, thus eliminating many opportunities for data exposure. In this paper we describe a detailed design of the EConfidante system, its flow and how it is managed and implemented. Our #MeToo design also uses an immutable distributed ledger which is built using components from a Blockchain framework. We implemented a proof of concept of our system for the #MeToo use case and analyze its security properties and implementation details.
Jialiang Chang, Bo Gao, Hao Xiao, Jun Sun · 6 authors
Ethereum smart contracts are an innovation built on top of the blockchain technology, which provides a platform for automatically executing contracts in an anonymous, distributed, and trusted way. The problem is magnified by the fact that smart contracts, unlike ordinary programs, cannot be patched easily once deployed. It is important for smart contracts to be checked against potential vulnerabilities. In this work, we propose an alternative approach to automatically identify critical program paths (with multiple function calls including inter-contract function calls) in a smart contract, rank the paths according to their criticalness, discard them if they are infeasible or otherwise present them with user friendly warnings for user inspection. We identify paths which involve monetary transaction as critical paths, and prioritize those which potentially violate important properties. For scalability, symbolic execution techniques are only applied to top ranked critical paths. Our approach has been implemented in a tool called sCompile, which has been applied to 36,099 smart contracts. The experiment results show that sCompile is efficient, i.e., 5 seconds on average for one smart contract. Furthermore, we show that many known vulnerabilities can be captured if user inspects as few as 10 program paths generated by sCompile. Lastly, sCompile discovered 224 unknown vulnerabilities with a false positive rate of 15.4% before user inspection.
Raziel combines secure multi-party computation and proof-carrying code to provide privacy, correctness and verifiability guarantees for smart contracts on blockchains. Effectively solving DAO and Gyges attacks, this paper describes an implementation and presents examples to demonstrate its practical viability (e.g., private and verifiable crowdfundings and investment funds). Additionally, we show how to use Zero-Knowledge Proofs of Proofs (i.e., Proof-Carrying Code certificates) to prove the validity of smart contracts to third parties before their execution without revealing anything else. Finally, we show how miners could get rewarded for generating pre-processing data for secure multi-party computation.
Florentin Guth, Valentin Wüstholz, Maria Christakis, Péter Müller
Smart contracts are programs that manage digital assets according to a certain protocol, expressing for instance the rules of an auction. Understanding the possible behaviors of a smart contract is difficult, which complicates development, auditing, and the post-mortem analysis of attacks. This paper presents the first specification mining technique for smart contracts. Our technique extracts the possible behaviors of smart contracts from contract executions recorded on a blockchain and expresses them as finite automata. A novel dependency analysis allows us to separate independent interactions with a contract. Our technique tunes the abstractions for the automata construction automatically based on configurable metrics, for instance, to maximize readability or precision. We implemented our technique for the Ethereum blockchain and evaluated its usability on several real-world contracts.
Mic Bowman, Andrea Miele, Michael Steiner, Bruno Vavala
We present Private Data Objects (PDOs), a technology that enables mutually untrusted parties to run smart contracts over private data. PDOs result from the integration of a distributed ledger and Intel Secure Guard Extensions (SGX). In particular, contracts run off-ledger in secure enclaves using Intel SGX, which preserves data confidentiality, execution integrity and enforces data access policies (as opposed to raw data access). A distributed ledger verifies and records transactions produced by PDOs, in order to provide a single authoritative instance of such objects. This allows contracting parties to retrieve and check data related to contract and enclave instances, as well as to serialize and commit contract state updates. The design and the development of PDOs is an ongoing research effort, and open source code is available and hosted by Hyperledger Labs [5, 7].
The Blockchain is an emerging paradigm that could solve security and trust issues for Internet of Things (IoT) platforms. We recently introduced in an IETF draft (“Blockchain Transaction Protocol for Constraint Nodes”) the BIoT paradigm, whose main idea is to insert sensor data in blockchain transactions. Because objects are not logically connected to blockchain platforms, controller entities forward all information needed for transaction forgery. Never less in order to generate cryptographic signatures, object needs some trusted computing resources. In previous papers we proposed the Four-Quater Architecture integrating general purpose unit (GPU), radio SoC, sensors/actuators and secure elements including TLS/DTLS stacks. These secure microcontrollers also manage crypto libraries required for blockchain operation. The BIoT concept has four main benefits: publication/duplication of sensors data in public and distributed ledgers, time stamping by the blockchain infrastructure, data authentication, and non repudiation.
Jul 1, 2018·2018 IEEE International Conference on Internet of Things (iThings) and IEEE Green Computing and Communications (GreenCom) and IEEE Cyber, Physical and Social Computing (CPSCom) and IEEE Smart Data (SmartData)
Scalability and privacy are two challenges for today's blockchain systems. Processing transactions at every node in the system limits the system's ability to scale. Furthermore, the requirement to publish all corporate or individual information for processing at every node, essentially making the data public, is - despite of all other advantages - often considered a major obstacle to blockchain adoption. In this paper, we make two main contributions to address these two problems: (i) To increase efficiency, we propose a processing model which employs non-interactive proofs to off-chain computations, thereby reducing on-chain computational efforts to the verification of correctness of execution rather than the execution itself. Due to the verifiable computation scheme's zero-knowledge property, private information used in the off-chain computation does not have to become public to verify correctness. (ii) We introduce ZoKrates, a toolbox to specify, integrate and deploy such off-chain computations. It consists of a domain-specific language, a compiler, and generators for proofs and verification Smart Contracts. ZoKrates hides significant complexity inherent to zero-knowledge proofs, provides a more familiar and higher level of programming abstractions to developers and enables circuit integration, hence fostering adoption.
Gbadebo Ayoade, Vishal Karande, Latifur Khan, Kevin W. Hamlen
Due to the centralization of authority in the management of data generated by IoT devices, there is a lack of transparency in how user data is being shared among third party entities. With the popularity of adoption of blockchain technology, which provide decentralized management of assets such as currency as seen in Bitcoin, we propose a decentralized system of data management for IoT devices where all data access permission is en-forced using smart contracts and the audit trail of data access is stored in the blockchain. With smart contracts applications, multiple parties can specify rules to govern their interactions which is independently enforced in the blockchain without the need for a centralized system. We provide a framework that store the hash of the data in the blockchain and store the raw data in a secure storage platform using trusted execution environment (TEE). In particular, we consider Intel SGX as a part of TEE that ensure data security and privacy for sensitive part of the application (code and data).
Jul 1, 2018·2018 IEEE International Conference on Internet of Things (iThings) and IEEE Green Computing and Communications (GreenCom) and IEEE Cyber, Physical and Social Computing (CPSCom) and IEEE Smart Data (SmartData)
DAO attack showed that formal verification of smart contracts is an important issue that should be addressed to prevent irreversible consequences due to design faults activation in Blockchain applications. This paper proposes a modeling method of an Ethereum application based on smart contracts, with the aim of applying a formal method, namely Model-Checking, to verify that the application implementation complies with its specification, formalized by a set of temporal logic propositions. NuSMV tool has been chosen to support this first approach. The proposed model template is shaped by three layers capturing respectively the behavior of Ethereum blockchain, the smart contracts themselves and the execution framework. The approach is illustrated by a case study coming from energy market field.
Mallikarjun Reddy Dorsala, V. N. Sastry, Chapram Sudhakar
Outsourcing a computation has been a major research area in cryptography. A delegatorDoutsources a computation to a workerW, who expects to get paid in return for delivering correct outputs. The delegator has to verify the output returned, to guard against malicious or malfunctioning worker. The worker may not trust the delegator to pay for computations performed by him. Blockchain systems like Bitcoin and Ethereum offer public verifiability of transactions generated in their networks. These transactions are of the form of a set of opcodes in Bitcoins or initiate execution of a contract in Ethereum, thus offering execution of small programs publicly. A fair protocol for verifiable computation between two parties$D$and$W$must provide the following guarantee: (1) Fast verification: The work performed to verify the correctness of output of a function is less than the work performed to compute function. (2) Pay to learn output: W obtains pay from D iff D received the correct output of the computation from W. In this work, we design two ideal functionalities$\mathcal{F}_{CRR}^{\ast}$for single worker case and$\mathcal{F}_{CCRR}^{\ast}$for multiple workers case. Existing methods do not allow Mutual revocation of deposit transaction which reduces the cost of script execution. Our ideal functionalities offer mutual revocation of the deposit transaction made byD. We show the realization of our ideal functionality$\mathcal{F}_{CRR}^{\ast}$in Bitcoin, and we also discuss fair protocols for verifiable computations of GCD of two large numbers and optimization problems. As our final work, we show a fair protocol for proof-based verifiable computing schemes.
A developing field of interest for the distributed systems and applied cryptography communities is that of smart contracts: self-executing financial instruments that synchronize their state, often through a blockchain. One such smart contract system that has seen widespread practical adoption is Ethereum, which has grown to a market capacity of 100 billion USD and clears an excess of 500,000 daily transactions. Unfortunately, the rise of these technologies has been marred by a series of costly bugs and exploits. Increasingly, the Ethereum community has turned to formal methods and rigorous program analysis tools. This trend holds great promise due to the relative simplicity of smart contracts and bounded-time deterministic execution inherent to the Ethereum Virtual Machine (EVM). Here we present KEVM, an executable formal specification of the EVM's bytecode stack-based language built with the K Framework, designed to serve as a solid foundation for further formal analyses. We empirically evaluate the correctness and performance of KEVM using the official Ethereum test suite. To demonstrate the usability, several extensions of the semantics are presented. and two different-language implementations of the ERC20 Standard Token are verified against the ERC20 specification. These results are encouraging for the executable semantics approach to language prototyping and specification.
Chuka Oham, Raja Jurdak, Salil S. Kanhere, Ali Dorri · 5 authors
In this paper, we propose a partitioned BlockChain based Framework for Auto-insurance Claims and Adjudication (B-FICA) for CAVs that tracks both sensor data and entity interactions with two-sided verification. B-FICA uses permissioned BC with two partitions to share information on a need to know basis. It also uses multi-signed transactions for proof of execution of instructions, for reliability and auditability and also uses a dynamic lightweight consensus and validation protocol to prevent evidence alteration. Qualitative evaluation shows that B-FICA is resilient to several security attacks from potential liable entities. Finally, simulations show that compared to the state of the art, B-FI CA reduces processing time and its delay overhead is negligible for practical scenarios and at marginal security cost.
Petar Tsankov, Andrei Dan, Dana Drachsler Cohen, Arthur Gervais · 6 authors
Permissionless blockchains allow the execution of arbitrary programs (called smart contracts), enabling mutually untrusted entities to interact without relying on trusted third parties. Despite their potential, repeated security concerns have shaken the trust in handling billions of USD by smart contracts. To address this problem, we present Securify, a security analyzer for Ethereum smart contracts that is scalable, fully automated, and able to prove contract behaviors as safe/unsafe with respect to a given property. Securify's analysis consists of two steps. First, it symbolically analyzes the contract's dependency graph to extract precise semantic information from the code. Then, it checks compliance and violation patterns that capture sufficient conditions for proving if a property holds or not. To enable extensibility, all patterns are specified in a designated domain-specific language. Securify is publicly released, it has analyzed >18K contracts submitted by its users, and is regularly used to conduct security audits by experts. We present an extensive evaluation of Securify over real-world Ethereum smart contracts and demonstrate that it can effectively prove the correctness of smart contracts and discover critical violations.
Proof of Work systems are used in cryptocurrencies to obtain consensus in distributed peer-to-peer systems that share no trust. Miners of cryptocurrency compete by engaging in the Proof of Work to solve a cryptographic challenge. The first to successfully provide a solution to the challenge wins by minting new currency. The process of mining also simultaneously prevents double-spending through the creation of an append-only distributed database known as the blockchain. The most widely adopted Proof of Work is the Hashcash scheme and the most widely deployed miners are ASIC-based. Despite the popularity of Hashcash, two issues are commonly identified its use. Firstly, the high energy consumption of the scheme is perceived as wasteful because the solutions found provide no useful output, and secondly, the computational complexity class of the scheme is not formally known. Based on these deficiencies, we propose a novel Proof of Work system which achieves the following goals:
Sergei Tikhomirov, Ekaterina Voskresenskaya, Ivan Ivanitskiy, Ramil Takhaviev · 6 authors
Ethereum is a major blockchain-based platform for smart contracts - Turing complete programs that are executed in a decentralized network and usually manipulate digital units of value. Solidity is the most mature high-level smart contract language. Ethereum is a hostile execution environment, where anonymous attackers exploit bugs for immediate financial gain. Developers have a very limited ability to patch deployed contracts. Hackers steal up to tens of millions of dollars from flawed contracts, a well-known example being "The DAO", broken in June 2016. Advice on secure Ethereum programming practices is spread out across blogs, papers, and tutorials. Many sources are outdated due to a rapid pace of development in this field. Automated vulnerability detection tools, which help detect potentially problematic language constructs, are still underdeveloped in this area.
Blockchain-based decentralized cryptocurrency platforms are currently one of the hottest topics in technology. Although most of the interest is generated by cryptocurrency related activities, it is becoming apparent that a much wider spectrum of applications can leverage the blockchain technology. The primary concepts enabling such general use of the blockchain are the so-called smart contracts, which are special programs that run on the blockchain. One of the most popular blockchain platforms that supports smart contracts is Ethereum. As smart contracts typically handle money, ensuring their low number of faults and vulnerabilities are essential. To aid smart contract developers and help to mature the technology, we need analysis tools and studies for smart contracts. As an initiative for this, we propose the adoption of some well-known OO metrics for Solidity smart contracts. Furthermore, we analyze more than 40 thousand Solidity source files with our prototype tool. The results suggest that smart contract programs are short, neither overly complex nor coupled too much, do not rely heavily on inheritance, and either quite well-commented or not commented at all. Moreover, smart contracts could benefit from an external library and dependency management mechanism, as more than 85% of the defined libraries in Solidity files code the same functionalities.
Termination of smart contracts is crucial for any blockchain system's security and consistency, especially for those supporting Turing-complete smart contract languages. Resource-constrained blockchain systems, like Ethereum and Hyperledger Fabric, could prevent smart contracts from terminating properly when the pre-allocated resources are not sufficient. The Zen system utilizes the dependent type system of the programming language F* to prove the termination of smart contracts for all inputs during compilation time. Since the smart contract execution usually depends on the current blockchain state and user inputs, this approach is not always successful. In this work, we propose a lazy approach by statically proving conditional termination and non-termination of a smart contract to determine input conditions under which the contract terminates or not. Prior to the execution of the smart contract, the proof-carrying blockchain system will check that its current state and the contract's input satisfy the termination conditions in order to determine if the contract is qualified (i.e., eventually terminating) to run on the chain.
Yandamuri, Sravya, Abraham, Ittai, Nayak, Kartik, Reiter, Michael K.
A smart contract on a blockchain cannot keep a secret because its data is replicated on all nodes in a network. To remedy this problem, it has been suggested to combine blockchains with trusted execution environments (TEEs), such as Intel SGX, for executing applications that demand privacy. Untrusted blockchain nodes cannot get access to the data and computations inside the TEE. This paper first explores some pitfalls that arise from the combination of TEEs with blockchains. Since TEEs are, in principle, stateless they are susceptible to rollback attacks, which should be prevented to maintain privacy for the application. However, in blockchains with non-final consensus protocols, such as the proof-of-work in Ethereum and others, the contract execution must handle rollbacks by design. This implies that TEEs for securing blockchain execution cannot be directly used for such blockchains; this approach works only when the consensus decisions are final. Second, this work introduces an architecture and a prototype for smart-contract execution within Intel SGX technology for Hyperledger Fabric, a prominent platform for enterprise blockchain applications. Our system resolves difficulties posed by the execute-order-validate architecture of Fabric and prevents rollback attacks on TEE-based execution as far as possible. For increasing security, our design encapsulates each application on the blockchain within its own enclave that shields it from the host system. An evaluation shows that the overhead moving execution into SGX is within 10%-20% for a sealed-bid auction application.
Mustafa Al-Bassam, Alberto Sonnino, Michał Król, Ioannis Psaras
We present Airtnt, a novel scheme that enables users with CPUs that support Trusted Execution Environments (TEEs) and remote attestation to rent out computing time on secure enclaves to untrusted users. Airtnt makes use of the attestation capabilities of TEEs and smart contracts on distributed ledgers to guarantee the fair exchange of the payment and the result of an execution. Airtnt makes use of off-chain payment channels to allow requesters to pay executing nodes for intermediate "snapshots" of the state of an execution. Effectively, this step-by-step "compute-payment" cycle realises untrusted pay-as-you-go micropayments for computation. Neither the requester nor the executing node can walk away and incur monetary loss to the other party. This also allows requesters to continue executions on other executing nodes if the original executing node becomes unavailable or goes offline.
Parinya Ekparinya, Vincent Gramoli, Guillaume Jourjon
Recently, several works conjectured the vulnerabilities of mainstream blockchains under several network attacks. All these attacks translate into showing that the assumptions of these blockchains can be violated in theory or under simulation at best. Unfortunately, previous results typically omit both the nature of the network under which the blockchain code runs and whether blockchains are private, consortium or public. In this paper, we study the public Ethereum blockchain as well as a consortium and private blockchains and quantify the feasibility of man-in-the-middle and double spending attacks against them. To this end, we list important properties of the Ethereum public blockchain topology, we deploy VMs with constrained CPU quantum to mimic the top-10 mining pools of Ethereum and we develop full-fledged attacks, that first partition the network through BGP hijacking or ARP spoofing before issuing a Balance Attack to steal coins. Our results demonstrate that attacking Ethereum is remarkably devastating in a consortium or private context as the adversary can multiply her digital assets by 200, 000x in 10 hours through BGP hijacking whereas it would be almost impossible in a public context.
Fergus Dall, Gabrielle De Micheli, Thomas Eisenbarth, Daniel Genkin · 7 authors
Intel Software Guard Extensions (SGX) allows users to perform secure computation on platforms that run untrusted software. To validate that the computation is correctly initialized and that it executes on trusted hardware, SGX supports attestation providers that can vouch for the user’s computation. Communication with these attestation providers is based on the Extended Privacy ID (EPID) protocol, which not only validates the computation but is also designed to maintain the user’s privacy. In particular, EPID is designed to ensure that the attestation provider is unable to identify the host on which the computation executes. In this work we investigate the security of the Intel implementation of the EPID protocol. We identify an implementation weakness that leaks information via a cache side channel. We show that a malicious attestation provider can use the leaked information to break the unlinkability guarantees of EPID. We analyze the leaked information using a lattice-based approach for solving the hidden number problem, which we adapt to the zero-knowledge proof in the EPID scheme, extending prior attacks on signature schemes.
Ahmed E. Kosba, Charalampos Papamanthou, Elaine Shi
Many cloud and cryptocurrency applications rely on verifying the integrity of outsourced computations, in which a verifier can efficiently verify the correctness of a computation made by an untrusted prover. State-of-the-art protocols for verifiable computation require that the computation task be expressed as arithmetic circuits, and the number of multiplication gates in the circuit is the primary metric that determines performance. At the present, a programmer could rely on two approaches for expressing the computation task, either by composing the circuits directly through low-level development tools; or by expressing the computation in a high-level program and rely on compilers to perform the program-to-circuit transformation. The former approach is difficult to use but on the other hand allows an expert programmer to perform custom optimizations that minimize the resulting circuit. In comparison, the latter approach is much more friendly to non-specialist users, but existing compilers often emit suboptimal circuits. We present xJsnark, a programming framework for verifiable computation that aims to achieve the best of both worlds: offering programmability to non-specialist users, and meanwhile automating the task of circuit size minimization through a combination of techniques. Specifically, we present new circuit-friendly algorithms for frequent operations that achieve constant to asymptotic savings over existing ones; various globally aware optimizations for short- and long- integer arithmetic; as well as circuit minimization techniques that allow us to reduce redundant computation over multiple expressions. We illustrate the savings in different applications, and show the framework's applicability in developing large application circuits, such as ZeroCash, while minimizing the circuit size as in low-level implementations.
Proof-of-Stake systems randomly choose, on each round, one of the\nparticipants as a consensus leader that extends the chain with the next block\nsuch that the selection probability is proportional to the owned stake.\nHowever, distributed random number generation is notoriously difficult. Systems\nthat derive randomness from the previous blocks are completely insecure;\nsolutions that provide secure random selection are inefficient due to their\nhigh communication complexity; and approaches that balance security and\nperformance exhibit selection bias. When block creation is rewarded with new\nstake, even a minor bias can have a severe cumulative effect.\n In this paper, we propose Robust Round Robin, a new consensus scheme that\naddresses this selection problem. We create reliable long-term identities by\nbootstrapping from an existing infrastructure, such as Intel's SGX processors,\nor by mining them starting from an initial fair distribution. For leader\nselection we use a deterministic approach. On each round, we select a set of\nthe previously created identities as consensus leader candidates in round robin\nmanner. Because simple round-robin alone is vulnerable to attacks and offers\npoor liveness, we complement such deterministic selection policy with a\nlightweight endorsement mechanism that is an interactive protocol between the\nleader candidates and a small subset of other system participants. Our solution\nhas low good efficiency as it requires no expensive distributed randomness\ngeneration and it provides block creation fairness which is crucial in\ndeployments that reward it with new stake.\n