RESEARCH PAPERS
Digital civilisation: manifesto for a trustworthy, well regulated world
A.W. Roscoe
Digital Civilisation Conference
Digital technology is advancing at a fantastic, some would say alarming, rate. It is taking over so much of how we interact with the world and each other. However it more reflects commercial opportunities and disconnected attempts to streamline government services than a proper digital civilisation. It offers the chance for a smoother and easier life while threatening a loss of personal privacy. We believe that society should develop ways of making all this technology more cohesive, more ethical and more respectful of the individual. We think that society should come together and organise the rules by which it expects technology to play, and the technological tools to allow a cohesive digital civilisation to grow. These two things are the core of our digital civilisation initiative.
The greening of blockchain mining
A.W. Roscoe, Bangdao Chen
University College Oxford Blockchain Research Centre
The Blockhouse Technology Limited
We analyse the proof of work mining model and show how to simulate many of its properties in a form of proof of stake called Work your Stake. In doing so we create innovations on timing, branch prevention and achieving an unbiasable random oracle that will be useful in other Blockchain models and decentralised systems. At the time of writing (mid 2019) the best known public blockchains are maintained by proof of work, a protocol which is simultaneously magical and disastrous. We will see why it is magical later. The best-known objection to it is that proof of work wastes energy. Mining a block of the bitcoin blockchain currently means that the network has to compute a truly astronomical number of hashes: about 2.2*1022.
ADDITIONAL papers
Embedding Reverse Links in a Blockchain
A.W. Roscoe, Pedro Antonino, Jonathan Lawrence
University College Oxford Blockchain Research Centre, The Blockhouse Technology Ltd
Blockchains provide extremely simple certainty looking backward in time because of the way each block contains a hash of its predecessor. This is not possible in the same way looking forward in time for various reasons, not the least of which is that when block 𝑁 is created, block 𝑁 + 1, and thus its hash, are unknown. Therefore blockchains rely on more complex mechanisms to establish what the successor of any given block is, and to ensure that alternatives - known as forks - cannot be introduced either close to the time of its creation or long after. These typically rely on chains of dependency and PKIs. In this paper we show how the concept of hooks can create something closely analogous to the usual hash links, only in the other direction. These represent a powerful mechanism to counteract attempts to insert forks from relatively old blocks, and are entirely internal to the blockchain. In understanding hooks we do some detailed combinatorial analysis of the game that good and bad agents play in blockchains, introducing criteria for relatively small collections of agents to make decisions, up to stochastic certainty.
THE CONSENSUS MACHINE: FORMALISING CONSENSUS IN THE PRESENCE OF MALIGN AGENTS (PRELIMINARY)
A.W. Roscoe, Pedro Antonino, Jonathan Lawrence
University College Oxford Blockchain Research Centre, The Blockhouse Technology Ltd
We show how a group of independent agents with carefully specified notions of progress and synchronisation can proceed in a model where consensus does not require unanimity and represents an emergent group behaviour. These agents will typically cooperate to implement a decentralised system such as a blockchain. Thus a model state machine can be compiled into replicated asynchronous agents that implement it in such a way as to overcome Byzantine faults up to a certain assumed level. Our abstraction achieves precise reliability and allows us to create schemes in which multiple consensus machines interact that can be modelled in process algebras like CSP and verified by model checking. This paper concentrates on the CSP analysis of a protocol showing how one distributed consensus machine can take over control from another without creating ambiguity over the outcome.
HOW TO CREATE A PUBLIC BLOCKCHAIN ETHICALLY
A.W. Roscoe
University College Oxford Blockchain Research Centre
Blockchains have a lot to offer to society and international trust. If one cannot set up a coalition that will be permanently trusted by all, then a widely used public blockchain where
parties hold and generate assets has much going for it. It is necessary to strongly align:
a) The interests of the participants who hold assets in keeping the integrity intact; b) The interest of a diverse and, where possible, public spirited community in building a
chain with total integrity.
TAKING THE WORK OUT OF BLOCKCHAIN SECURITY
A.W. Roscoe, Wang Lei
Chieftin Lab
University College Oxford Blockchain Research Centre
The most convincing argument for proof of work in the mining of public blockchains is, at least in our view, that it makes the creation of a fake branch too difficult or impossible thanks to the follow the longest chain principle. In this paper we suggest a modification to the structure and protocol for blockchains that provides an alternate possibility for this. Specifically, we show how blockchains can develop links in the opposite direction to the standard hashes of the hash chain thanks to building in hooks that can later be used to attach further up the chain. These, together with limited use of timing, can eliminate any realistic possibility of a branch being plausible.
Temporal signature in the blockchain
A.W. Roscoe
Chieftin Lab
University College Oxford Blockchain Research Centre
Every blockchain requires a form of cryptographic hash to maintain its basic integrity, linking blocks as well as contributing to cryptographic signature. A secure and long lasting blockchain provides asecure and linear notion of timestamping. In this paper we explain how the latter can be used in constructing novel hash-based signatures and investigate whether such signatures can be used to maintain the structure of the blockchain.
Key agreements via protocols
A.W. Roscoe, Wang Lei
University College Oxford Blockchain Research Centre
The objective of this paper is to introduce and justify a mining model with as much as possible in common with PoW but which does not require anything like so much energy usage. The core idea is to retain the hash competition but make it vastly easier by dint of controlling how many entries can be made. Each has to be paid for. Broadly speaking we want to force miners to spend money on mining tokens of some sort rather than electricity.
Fair exchange in the blockchain (draft)
A.W. Roscoe, Bangdao Chen, Wang Lei.
Chieftin Lab
Fair exchange is an important primitive in transactions where the parties do not completely trust one another. It is well known to be impossible to implement this with 100% assurance without a trusted third party. The blockchain is a sort of trusted third party built out of many untrusted parties, and a very popular target for systems involving peer-to-peer (i.e. without passing via central authorities) transactions. In this paper we show a number of different ways in which fair exchange can be implemented.
Delay and escrow in the blockchain (draft)
A.W. Roscoe
Chieftin Lab
In this paper we show how to implement exact-time delay encryption in a trust environment like the blockchain, where we can be confident that some sort of majority of participants are trustworthy but not any individual one. In other words we give a protocol for generating delay(x; t), a value which gives no significant information until time t, whereupon it can be decrypted to x by anyone. We highlight some applications of this construct and show how it can be extended to a more general form of escrow.
Further thoughts on Work Your Stake (draft)
A.W. Roscoe, Bangdao Chen, Wang Lei
This paper analyses the practicality, economics and options of our WyS mining model. We are not, of course, economists.
We examine the options available to anyone designing a blockchain using WyS and the options there seemingly are to influencing its economy. The model was somewhat based on proof of work but contains options not available there.
Seraph: Enabling Cross-Platform Security Analysis For EVM and WASM Smart Contracts
Zhiqiang Yang, Han Liu, Yue Li, Huixuan Zheng, Lei Wang, Bangdao Chen
University College Oxford Blockchain Research Centre
Shanghai Jiao Tong University
As blockchain becomes increasingly popular across various industries in recent years, many companies started designing and developing their own smart contract platforms to enable better services on blockchain. While smart contracts are notoriously known to be vulnerable to external attacks, such platform diversity further amplified the security challenge. To mitigate this problem, we designed the very first cross-platform security analyzer called Seraph for smart contracts.
PROTECT YOUR SMART CONTRACT AGAINST UNFAIR PAYMENT
Yue Li, Han Liu, Zhiqiang Yang, Bin Wang, Qian Ren, Lei Wang, Bangdao Chen
University College Oxford Blockchain Research Centre
Shanghai Jiao Tong University
While smart contracts have enabled a wide range of applications in many public blockchains, e.g., Ethereum, their security issues have been raising an increasing number of threats on the stability of blockchain ecosystem. In practice, many external attacks on smart contracts result from broken payments with digital assets, e.g., cryptocurrencies. While an increasing number of research works have been focusing on such problems, many of them adopted pattern-based heuristics (e.g., reentrancy) to find payment-related attacks thus can incur a considerably large portion of both false positives and negatives.
safepay on ethereum: a framework for detecting unfair payments in smart contracts
Yue Li, Han Liu, Zhiqiang Yang, Bin Wang, Qian Ren, Lei Wang, Bangdao Chen
University College Oxford Blockchain Research Centre
Shanghai Jiao Tong University
Smart contracts on the Ethereum blockchain are notoriously known as vulnerable to external attacks. Many of their issues led to a considerably large financial loss as they
resulted from broken payments by digital assets, e.g., cryptocurrency. Existing research focused on specific patterns to find such problems, yet may lead to false alarms or miss important issues. To mitigate these limitations, we designed the SAFEPAY analysis framework to find unfair payments in Ethereum smart contracts. Compared to existing analyzers, SAFEPAY can detect potential blockchain transactions with feasible exploits thus effectively avoid false reports.
Solidifier: bounded model checking Solidity using lazy contract deployment and precise memory modelling
Pedro Antonino, A. W. Roscoe
The Blockhouse Technology Limited
University College Oxford Blockchain Research Centre
The exploitation of smart-contract vulnerabilities can have catastrophic consequences such as the loss of millions of pounds worth of crypto assets. Formal verification can be a useful tool in identifying vulnerabilities and proving that they have been fixed. In this paper, we present a formalisation of Solidity and the Ethereum blockchain using the Solid language and its blockchain; a Solid program is obtained by explicating/desugaring a Solidity program. We make some abstractions that over-approximate the way in which Solidity/Ethereum behave. Based on this formalisation, we create Solidifier: a bounded model checker for Solidity.
Guardian: Symbolic Validation of Orderliness in SGX Enclaves
Pedro Antonino, Wojciech Aleksander Wołoszyn, A. W. Roscoe
The Blockhouse Technology Limited
University College Oxford Blockchain Research Centre
Modern processors can offer hardware primitives that allow a pro- cess to run in isolation. These primitives implement a trusted execu- tion environment (TEE) in which a program can run such that the integrity and confidentiality of its execution are guaranteed. Intel’s Software Guard eXtensions (SGX) is an example of such primitives and its isolated processes are called enclaves. These guarantees, however, can be easily thwarted if the enclave has not been prop- erly designed. Its interface with the untrusted software stack is a perhaps the largest attack surface that adversaries can exploit; un- intended interactions with untrusted code can expose the enclave to memory corruption attacks, for instance.
SPECIFICATION IS LAW: SAFE CREATION AND UPGRADE OF ETHEREUM SMART CONTRACTS
Pedro Antonino, Juliandson Ferreira, Augusto Sampaio, and A. W. Roscoe
The Blockhouse Technology Limited, Oxford, UK
Centro de InformÅLatica, Universidade Federal de Pernambuco, Recife, Brazil
Department of Computer Science, Oxford University, Oxford, UK
University College Oxford Blockchain Research Centre, Oxford, UK
Smart contracts are the building blocks of the “code is law” paradigm: the smart contract’s code indisputably describes how its assets are to be managed - once it is created, its code is typically immutable. Faulty smart contracts present the most significant evidence against the practicality of this paradigm; they are well-documented and resulted in assets worth vast sums of money being compromised. To address this issue, the Ethereum community proposed (i) tools and processes to audit/ analyse smart contracts, and (ii) design patterns implementing a mechanism to make contract code mutable. Individually, (i) and (ii) only partially address the challenges raised by the “code is law” paradigm. In this paper, we combine elements from (i) and (ii) to create a systematic framework that moves away from “code is law” and gives rise to a new “specification is law” paradigm. It allows contracts to be created and upgraded but only if they meet a corresponding formal specification. The framework is centered around a trusted deployer: an off-chain service that formally verifies and enforces this notion of conformance. We have prototyped this framework, and investigated its applicability to contracts implementing three widely used Ethereum standards: the ERC20 Token Standard, ERC3156 Flash Loans and ERC1155 Multi Token Standard, with promising results.
An Unbiassable Random Oracle for Blockchains
A.W. Roscoe, Pedro Antonino and Jonathan Lawrence
We introduce a new way of constructing a random oracle that generates a random number at chosen events — such as the generation of a new block — in a blockchain. We make fairly standard assumptions about the distribution of good and bad behaviour of contributing agents and do not require any dependably trustworthy player, internal or external. We give two variants on this oracle. These cannot be meaningfully biassed by any feasible coalition of bad agents, whether by their action or inaction.
Flexible remote attestation of pre-SNP SEV VMs using SGX enclaves
Pedro Antonino, The Blockhouse Technology Limited, Oxford, UK
Ante Derek, Faculty of Electrical Engineering and Computing, University of Zagreb, Zagreb, Croatia
Wojciech Aleksander Wołoszyn, The Blockhouse Technology Limited, Oxford, UK / Mathematical Institute, University of Oxford, Oxford, UK / St Hilda’s College, Oxford, UK
We propose a protocol that explores a synergy between two TEE implementations: it brings SGX-like remote attestation to SEV VMs. We use the notion of a trusted guest owner, implemented as an SGX enclave, to deploy, attest, and provision an SEV VM. This machine can, in turn, rely on the trusted owner to generate SGX-like attestation proofs on its behalf. Our protocol combines the application portability of SEV with the flexible remote attestation of SGX.We formalise our protocol and prove that it achieves the intended guarantees using the Tamarin prover. Moreover, we develop an implementation for our trusted guest owner together with example SEV machines, and put those together to demonstrate how our protocol can be used in practice; we use this implementation to evaluate our protocol in the context of creating accountable machine-learning models. We also discuss how our protocol can be extended to provide a simple remote attestation mechanism for a heterogeneous infrastructure of trusted components.
Demo: CLOAK: A Framework For Development of Confidential Blockchain Smart Contracts
Qian Ren, Oxford-Hainan Blockchain Research Institute
Han Liu, Oxford-Hainan Blockchain Research Institute
Yue Li, Oxford-Hainan Blockchain Research Institute
Hong Lei, Oxford-Hainan Blockchain Research Institute / School of Computer Science and Cyberspace Security, Hainan University
In recent years, as blockchain adoption has been expanding across a wide range of domains, e.g., digital asset, supply chain finance, etc., the confidentiality of smart contracts is now a fundamental demand for practical applications. However, while new privacy protection techniques keep coming out, how existing ones can best fit development settings is little studied. Suffering from limited architectural support in terms of programming interfaces, state-of-the-art solutions can hardly reach general developers. In this paper, we proposed the CLOAK framework for developing confidential smart contracts. The key capability of CLOAK is allowing developers to implement and deploy practical solutions to multi-party transaction (MPT) problems, i.e., transact with secret inputs and states owned by different parties by simply specifying it. To this end, CLOAK introduced a domain-specific annotation language for declaring privacy specifications and further automatically generating confidential smart contracts to be deployed with trusted execution environment (TEE) on blockchain. In our evaluation on both simple and real-world applications, developers managed to deploy business services on blockchain in a concise manner by only developing CLOAK smart contracts whose size is less than 30% of the deployed ones.
Cloak: Transitioning States on Legacy Blockchains Using Secure and Publicly Verifiable Off-Chain Multi-Party Computation
Qian Ren, SSC Holding Company Ltd / Oxford-Hainan Blockchain Research Institute
Yingjun Wu, SSC Holding Company Ltd / Oxford-Hainan Blockchain Research Institute
Han Liu, Oxford-Hainan Blockchain Research Institute / Tsinghua University
Yue Li, Oxford-Hainan Blockchain Research Institute
Anne Victor, SSC Holding Company Ltd / Oxford-Hainan Blockchain Research Institute
Hong Lei, Hainan University / Oxford-Hainan Blockchain Research Institute
Lei Wang, Shanghai Jiao Tong University
Bangdao Chen, SSC Holding Company Ltd / Oxford-Hainan Blockchain Research Institute
In recent years, the confidentiality of smart contracts has become a fundamental requirement for practical applications. While many efforts have been made to develop architectural capabilities for enforcing confidential smart contracts, a few works arise to extend confidential smart contracts to Multi-Party Computation (MPC), i.e., multiple parties jointly evaluate a transaction off-chain and commit the outputs on-chain without revealing their secret inputs/outputs to each other. However, existing solutions lack public verifiability and require 𝑂(𝑛) transactions to enable negotiation or resist adversaries, thus suffering from inefficiency and compromised security. In this paper, we propose Cloak, a framework for enabling Multi- Party Transaction (MPT) on existing blockchains. An MPT refers to transitioning blockchain states by an publicly verifiable off-chain MPC. We identify and handle the challenges of securing MPT by harmonizing TEE and blockchain. Consequently, Cloak secures the off-chain nondeterministic negotiation process (a party joins an MPT without knowing identities or the total number of parties until the MPT proposal settles), achieves public verifiability (the public can validate that the MPT correctly handles the secret inputs/ outputs from multiple parties and reads/writes states on-chain), and resists Byzantine adversaries. According to our proof, Cloak achieves better security with only 2 transactions, superior to previous works that achieve compromised security at 𝑂(𝑛) transactions cost. By evaluating examples and real-world MPTs, the gas cost of Cloak reduces by 32.4% on average.
