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

Add to Calendar Add to your calendar

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.

Go backGo back to the seminar list