SE Seminar: Proving Ethereum Smart Contracts correct using Vale, F* and Z3

21 Feb 2023 2:00 PM - 3:00 PM
Presenter/Speaker: Associate Professor Mark Utting, University of Queensland
Location: G.1.15

We explore the use of Microsoft’s Vale framework to guarantee low level correctness of Ethereum Virtual Machine (EVM) bytecode, while affording smart contract developers higher-level language and reasoning features. We encode EVM-R (a subset of EVM semantics and instruction set) into F*, and raise the EVM-R into Vale design-by-contract components in an intermediate language supporting conditional logic. The specifications of Vale procedures constructed from these verified EVM bytecodes carry integrity to the bytecode level, which cannot be guaranteed by current EVM compilers. Furthermore, raising the instruction set to Vale allows opportunity for refinement of the instructions, which we did ensuring safety properties of overflow protection, invalid memory access protection, and functional correctness. We demonstrate our contributions through two case study smart contracts, a simple casino, and a subcurrency coin.