Seminar - Towards foundational smart contract verification
School of Engineering and Computer Science Seminar
Speaker: Daniel Britten, University of Waikato
Time:
Friday 6th August 2021 at 12:00 PM -
12:50 PM
Location:
Cotton Building CO431
Abstract
Smart Contracts are programs which are executed on a blockchain, they often have high financial stakes and are immutable once deployed - as a result correctness is critical. In this talk I will describe aspects of an approach for foundational smart contract correctness using the DeepSEA language. DeepSEA has a verified compiler within Coq which enables proofs to be done about a high-level representation of the smart contract yet with the guarantee that the generated bytecode deployed to the blockchain is a refinement of the high-level representation.
DeepSEA is developed by CertiK. I have been involved with extending and improving DeepSEA as a part of my PhD research. As elegantly put in a Whiley paper David Pearce recently drew my attention to: "The gold standard for software verification is machine-checked formal proof of correctness, followed by verified refinement down to the executable machine code or bytecode" - this is exactly to goal of DeepSEA, for Ethereum smart contracts.