Loading...
Thumbnail Image
Publication

Modelling a blockchain for smart contract verification using DeepSEA

Abstract
To create trustworthy programs, the 'gold standard' is specifications at a high-enough level to clearly correspond to the informal specifications, and also a refinement proof linking these high-level specifications down to, in our case, executable bytecode. The DeepSEA system demonstrates how this can be done, in the context of smart contracts on the Ethereum blockchain. A key component of this is the model of the blockchain on which the smart contracts reside. When doing proofs in DeepSEA, it is critical to have such a model, which allows for the writing of specifications at a high-level clearly corresponding to informal specifications. A candidate model for doing so and its usefulness for carrying out proofs is discussed in this paper.
Type
Conference Contribution
Type of thesis
Series
Citation
Date
2022
Publisher
Association for Computing Machinery
Degree
Supervisors
Rights
This is an author’s accepted version of a conference paper published in FTSCS 2022: Proceedings of the 8th ACM SIGPLAN International Workshop on Formal Techniques for Safety-Critical Systems. © 2022 Copyright held by the authors. Publication rights licensed to ACM.