Smart contracts Verification

High-assurance smart contracts

The goal of this project is to use formal verification to improve assurance of smart contracts. By providing mathematical rigorous proofs that smart contracts do what we think they should do, we better leverage of such technology and enable its use for safety- and security-critical purposes.

We have developed a framework to reason formally about Ethereum Virtual Machine bytecode execution in Isabelle/HOL. We have used that framework to verify Ethereum smart contracts. Now we are extending that framework to be able to verify realistic food supply-chain smart contracts.

This project is one of many Trustworthy Systems projects and is done in collaboration with the Blockchain research group in Data61's Software and Computational Systems.

Publications

Sidney Amani, Myriam Begel, Maksym Bortin and Mark Staples Towards verifying Ethereum smart contract bytecode in Isabelle/HOL International Conference on Certified Programs and Proofs, pp. 66-77, Los Angeles, January, 2018

Contact

Mark Staples, mark.staples<at>data61.csiro.au