Source author record

A. W. Roscoe

A. W. Roscoe appears in the imported research catalog. Authorship, coauthor and topic links are available while profile ownership is still unclaimed.

ResearcherUnclaimed source record

Logic in Computer Science Software Engineering Cryptography and Security Programming Languages

Catalog footprint

What is connected

5works

4topics

4close collaborators

Actions

Connect this record

Open graph Browse works

Inspect adjacent papers, topics, institutions and collaborators without losing the researcher page.

Building this map preview

BZPEER is loading the nearby papers, people, topics and institutions for this page.

preprint2022arXiv

Delay Encryption by Cubing

Delay Encryption (often called Timed-Release Encryption) is a scheme in which a message is sent into the future by ensuring its confidentiality only for a given amount of time. We propose a new scheme based on a novel time-lock puzzle. This puzzle relies on the assumption that repeated squaring is an inherently sequential process. We perform an extensive and practical analysis of many classical and quantum attacks on our scheme and conclude that it is secure given some precautions.

preprint2022arXiv

Specification is Law: Safe Creation and Upgrade of Ethereum Smart Contracts

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 \emph{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 two widely used Ethereum standards: the ERC20 Token Standard and ERC1155 Multi Token Standard, with promising results.

preprint2020arXiv

Formalising and verifying smart contracts with Solidifier: a bounded model checker for Solidity

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. It translates Solid into Boogie, an intermediate verification language, that is later verified using Corral, a bounded model checker for Boogie. Unlike much of the work in this area, we do not try to find specific behavioural/code patterns that might lead to vulnerabilities. Instead, we provide a tool to find errors/bad states, i.e. program states that do not conform with the intent of the developer. Such a bad state, be it a vulnerability or not, might be reached through the execution of specific known code patterns or through behaviours that have not been anticipated.

preprint2016arXiv

Card games as pointer structures: case studies in mobile CSP modelling

The author has long enjoyed using the CSP refinement checker FDR to solve puzzles, as witnessed by examples in \cite{tpc,ucs}. Recent experiments have shown that a number of games of patience (card games for one) are now well within bounds. We discuss the modelling approaches used to tackle these and avoid symmetric states. For two such games we reveal much higher percentages of winnable games than was previously believed. The techniques developed for some of these card games -which employ various dynamic patterns of cards - suggest techniques for modelling pointer structures in CSP and FDR analogous to those used with the pi-calculus. Most of these use CSP's ability to express mobile systems.

preprint2013arXiv

A Static Analysis Framework for Livelock Freedom in CSP

In a process algebra with hiding and recursion it is possible to create processes which compute internally without ever communicating with their environment. Such processes are said to diverge or livelock. In this paper we show how it is possible to conservatively classify processes as livelock-free through a static analysis of their syntax. In particular, we present a collection of rules, based on the inductive structure of terms, which guarantee livelock-freedom of the denoted process. This gives rise to an algorithm which conservatively flags processes that can potentially livelock. We illustrate our approach by applying both BDD-based and SAT-based implementations of our algorithm to a range of benchmarks, and show that our technique in general substantially outperforms the model checker FDR whilst exhibiting a low rate of inconclusive results.