Blockhouse :Technology with trust built in

High security • Pro‑regulation • Environmentally friendly

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.​

READ

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.

READ

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.

READ

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.

READ

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.

READ

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.

READ

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.

READ

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.

READ

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.

READ

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.

READ

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.

READ

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.

READ

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.

READ

safepay on ethereum: a framework for detecting unfair payments in smart contracts

awarded best demo paper of the year 2020

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.

READ

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.

READ

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.

READ

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.​

READ

TBTL either owns or has licenses to much of the IP described in these papers

Social Share Buttons and Icons powered by Ultimatelysocial

AWARDED BEST DEMO PAPER OF THE YEAR 2020

The 40th IEEE International Conference on Distributed Computing Systems (ICDCS) was successfully held from November 29th to December 1st, 2020. The paper SAFEPAY on Ethereum: A Framework for Detecting Unfair Payments in Smart Contracts written by Oxford-Hainan Blockchain Research Institute’s team won the Best Demo Award.