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.
Publisher
Association for Computing Machinery
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.
