-
Specification is Law: Safe Creation and Upgrade of Ethereum Smart Contracts
Authors:
Pedro Antonino,
Juliandson Ferreira,
Augusto Sampaio,
A. W. Roscoe
Abstract:
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 compromis…
▽ More
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.
△ Less
Submitted 16 May, 2022;
originally announced May 2022.
-
Delay Encryption by Cubing
Authors:
Ivo Maffei,
A. W. Roscoe
Abstract:
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 an…
▽ More
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.
△ Less
Submitted 11 May, 2022;
originally announced May 2022.
-
Trusted And Confidential Program Analysis
Authors:
Han Liu,
Pedro Antonino,
Zhiqiang Yang,
Chao Liu,
A. W. Roscoe
Abstract:
We develop the concept of Trusted and Confidential Program Analysis (TCPA) which enables program certification to be used where previously there was insufficient trust. Imagine a scenario where a producer may not be trusted to certify its own software (perhaps by a foreign regulator), and the producer is unwilling to release its sources and detailed design to any external body. We present a protoc…
▽ More
We develop the concept of Trusted and Confidential Program Analysis (TCPA) which enables program certification to be used where previously there was insufficient trust. Imagine a scenario where a producer may not be trusted to certify its own software (perhaps by a foreign regulator), and the producer is unwilling to release its sources and detailed design to any external body. We present a protocol that can, using trusted computing based on encrypted sources, create certification via which all can trust the delivered object code without revealing the unencrypted sources to any party. Furthermore, we describe a realization of TCPA with trusted execution environments (TEE) that enables general and efficient computation. We have implemented the TCPA protocol in a system called TCWasm for web assembly architectures. In our evaluation with 33 benchmark cases, TCWasm managed to finish the analysis with relatively slight overheads.
△ Less
Submitted 1 December, 2021;
originally announced December 2021.
-
Guardian: symbolic validation of orderliness in SGX enclaves
Authors:
Pedro Antonino,
Wojciech Aleksander Wołoszyn,
A. W. Roscoe
Abstract:
Modern processors can offer hardware primitives that allow a process to run in isolation. These primitives implement a trusted execution 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 \emph{enclaves}. These guarant…
▽ More
Modern processors can offer hardware primitives that allow a process to run in isolation. These primitives implement a trusted execution 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 \emph{enclaves}. These guarantees, however, can be easily thwarted if the enclave has not been properly designed. Its interface with the untrusted software stack is arguably the largest attack surface that adversaries can exploit; unintended interactions with untrusted code can expose the enclave to memory corruption attacks, for instance. In this paper, we propose a notion of an \emph{orderly} enclave which splits its behaviour into several execution phases each of which imposes a set of restrictions on accesses to untrusted memory, phase transitions and registers sanitisation. A violation to these restrictions indicates an undesired behaviour which could be harnessed to perpetrate attacks against the enclave. We also introduce \Analyser{}: a tool that uses symbolic execution to carry out the validation of an enclave against our notion of an orderly enclave; in this process, it also looks for some typical memory-corruption vulnerabilities. We discuss how our approach can prevent and flag enclave vulnerabilities that have been identified in the literature. Moreover, we have evaluated how our approach fares in the analysis of some practical enclaves. \Analyser{} was able to identify real vulnerabilities on these enclaves which have been acknowledged and fixed by their maintainers.
△ Less
Submitted 12 May, 2021;
originally announced May 2021.
-
Formalising and verifying smart contracts with Solidifier: a bounded model checker for Solidity
Authors:
Pedro Antonino,
A. W. Roscoe
Abstract:
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 progr…
▽ More
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.
△ Less
Submitted 7 February, 2020;
originally announced February 2020.
-
Translating between models of concurrency
Authors:
David Mestel,
A. W. Roscoe
Abstract:
Hoare's Communicating Sequential Processes (CSP) admits a rich universe of semantic models closely related to the van Glabbeek spectrum. In this paper we study finite observational models, of which at least six have been identified for CSP, namely traces, stable failures, revivals, acceptances, refusal testing and finite linear observations. We show how to use the recently-introduced \emph{priorit…
▽ More
Hoare's Communicating Sequential Processes (CSP) admits a rich universe of semantic models closely related to the van Glabbeek spectrum. In this paper we study finite observational models, of which at least six have been identified for CSP, namely traces, stable failures, revivals, acceptances, refusal testing and finite linear observations. We show how to use the recently-introduced \emph{priority} operator to transform refinement questions in these models into trace refinement (language inclusion) tests. Furthermore, we are able to generalise this to any (rational) finite observational model. As well as being of theoretical interest, this is of practical significance since the state-of-the-art refinement checking tool FDR4 currently only supports two such models. In particular we study how it is possible to check refinement in a discrete version of the Timed Failures model that supports Timed CSP.
△ Less
Submitted 22 April, 2019;
originally announced April 2019.
-
A Proof of Entropy Minimization for Outputs in Deletion Channels via Hidden Word Statistics
Authors:
Arash Atashpendar,
David Mestel,
A. W. Roscoe,
Peter Y. A. Ryan
Abstract:
From the output produced by a memoryless deletion channel from a uniformly random input of known length $n$, one obtains a posterior distribution on the channel input. The difference between the Shannon entropy of this distribution and that of the uniform prior measures the amount of information about the channel input which is conveyed by the output of length $m$, and it is natural to ask for whi…
▽ More
From the output produced by a memoryless deletion channel from a uniformly random input of known length $n$, one obtains a posterior distribution on the channel input. The difference between the Shannon entropy of this distribution and that of the uniform prior measures the amount of information about the channel input which is conveyed by the output of length $m$, and it is natural to ask for which outputs this is extremized. This question was posed in a previous work, where it was conjectured on the basis of experimental data that the entropy of the posterior is minimized and maximized by the constant strings $\texttt{000}\ldots$ and $\texttt{111}\ldots$ and the alternating strings $\texttt{0101}\ldots$ and $\texttt{1010}\ldots$ respectively. In the present work we confirm the minimization conjecture in the asymptotic limit using results from hidden word statistics. We show how the analytic-combinatorial methods of Flajolet, Szpankowski and Vallée for dealing with the hidden pattern matching problem can be applied to resolve the case of fixed output length and $n\rightarrow\infty$, by obtaining estimates for the entropy in terms of the moments of the posterior distribution and establishing its minimization via a measure of autocorrelation.
△ Less
Submitted 30 July, 2018;
originally announced July 2018.
-
From Clustering Supersequences to Entropy Minimizing Subsequences for Single and Double Deletions
Authors:
Arash Atashpendar,
Marc Beunardeau,
Aisling Connolly,
Rémi Géraud,
David Mestel,
A. W. Roscoe,
Peter Y. A. Ryan
Abstract:
A binary string transmitted via a memoryless i.i.d. deletion channel is received as a subsequence of the original input. From this, one obtains a posterior distribution on the channel input, corresponding to a set of candidate supersequences weighted by the number of times the received subsequence can be embedded in them. In a previous work it is conjectured on the basis of experimental data that…
▽ More
A binary string transmitted via a memoryless i.i.d. deletion channel is received as a subsequence of the original input. From this, one obtains a posterior distribution on the channel input, corresponding to a set of candidate supersequences weighted by the number of times the received subsequence can be embedded in them. In a previous work it is conjectured on the basis of experimental data that the entropy of the posterior is minimized and maximized by the constant and the alternating strings, respectively. In this work, in addition to revisiting the entropy minimization conjecture, we also address several related combinatorial problems. We present an algorithm for counting the number of subsequence embeddings using a run-length encoding of strings. We then describe methods for clustering the space of supersequences such that the cardinality of the resulting sets depends only on the length of the received subsequence and its Hamming weight, but not its exact form. Then, we consider supersequences that contain a single embedding of a fixed subsequence, referred to as singletons, and provide a closed form expression for enumerating them using the same run-length encoding. We prove an analogous result for the minimization and maximization of the number of singletons, by the alternating and the uniform strings, respectively. Next, we prove the original minimal entropy conjecture for the special cases of single and double deletions using similar clustering techniques and the same run-length encoding, which allow us to characterize the distribution of the number of subsequence embeddings in the space of compatible supersequences to demonstrate the effect of an entropy decreasing operation.
△ Less
Submitted 4 March, 2019; v1 submitted 2 February, 2018;
originally announced February 2018.
-
Card games as pointer structures: case studies in mobile CSP modelling
Authors:
A. W. Roscoe
Abstract:
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 tha…
▽ More
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.
△ Less
Submitted 25 November, 2016;
originally announced November 2016.
-
A Static Analysis Framework for Livelock Freedom in CSP
Authors:
Joel Ouaknine,
Hristina Palikareva,
A. W. Roscoe,
James Worrell
Abstract:
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 o…
▽ More
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.
△ Less
Submitted 27 September, 2013; v1 submitted 27 April, 2013;
originally announced April 2013.
-
On model checking data-independent systems with arrays without reset
Authors:
R. S. Lazic,
T. C. Newcomb,
A. W. Roscoe
Abstract:
A system is data-independent with respect to a data type X iff the operations it can perform on values of type X are restricted to just equality testing. The system may also store, input and output values of type X. We study model checking of systems which are data-independent with respect to two distinct type variables X and Y, and may in addition use arrays with indices from X and values from…
▽ More
A system is data-independent with respect to a data type X iff the operations it can perform on values of type X are restricted to just equality testing. The system may also store, input and output values of type X. We study model checking of systems which are data-independent with respect to two distinct type variables X and Y, and may in addition use arrays with indices from X and values from Y . Our main interest is the following parameterised model-checking problem: whether a given program satisfies a given temporal-logic formula for all non-empty nite instances of X and Y . Initially, we consider instead the abstraction where X and Y are infinite and where partial functions with finite domains are used to model arrays. Using a translation to data-independent systems without arrays, we show that the u-calculus model-checking problem is decidable for these systems. From this result, we can deduce properties of all systems with finite instances of X and Y . We show that there is a procedure for the above parameterised model-checking problem of the universal fragment of the u-calculus, such that it always terminates but may give false negatives. We also deduce that the parameterised model-checking problem of the universal disjunction-free fragment of the u-calculus is decidable. Practical motivations for model checking data-independent systems with arrays include verification of memory and cache systems, where X is the type of memory addresses, and Y the type of storable values. As an example we verify a fault-tolerant memory interface over a set of unreliable memories.
△ Less
Submitted 26 May, 2004;
originally announced May 2004.
