Meng Xu - University of Waterloo
Fast and Reliable Formal Verification of Smart Contracts with the Move Prover
Nov 30, 2022
The Move Prover (MVP) is a formal verifier forsmart contracts written In the Move programming language. MVP has an expressivespecification language, and is fast and reliable enough that it can be runroutinely by developers and in integration testing. Besides the simplicity ofsmart contracts and the Move language, three implementation approaches areresponsible for the practicality of MVP: (1) an alias-free memory model, (2)fine-grained invariant checking, and (3) monomorphization. The entirety of theMove code for the Diem blockchain has been extensively specified and can becompletely verified by MVP in a few minutes. Changes in the Diem framework mustbe successfully verified before being integrated into the open sourcerepository on GitHub.
About the Speaker
Dr.Meng Xu is an Assistant Professor in the Cheriton School of Computer Science atthe University of Waterloo, Canada. His research is in the area of system andsoftware security, with a focus on delivering high-quality solutions topractical security programs, especially in finding and patching vulnerabilitiesin critical computer systems. This usually includes research and development ofautomated program analysis/ testing / verification tools that facilitate thesecurity reasoning of critical programs.