The Center for Education and Research in Information Assurance and Security (CERIAS)

The Center for Education and Research in
Information Assurance and Security (CERIAS)
Center for Education and Research in Information Assurance and Security

Meng Xu - University of Waterloo

Students: Spring 2025, unless noted otherwise, sessions will be virtual on Zoom.

Fast and Reliable Formal Verification of Smart Contracts with the Move Prover

Nov 30, 2022

Download: Video Icon MP4 Video Size: 212.8MB  
Watch on Youtube Watch on YouTube

Abstract



The Move Prover (MVP) is a formal verifier for smart contracts written In the Move programming language. MVP has an expressive specification language, and is fast and reliable enough that it can be run routinely by developers and in integration testing. Besides the simplicity of smart contracts and the Move language, three implementation approaches are responsible for the practicality of MVP: (1) an alias-free memory model, (2)fine-grained invariant checking, and (3) monomorphization. The entirety of the Move code for the Diem blockchain has been extensively specified and can be completely verified by MVP in a few minutes. Changes in the Diem framework must be successfully verified before being integrated into the open source repository on GitHub.

About the Speaker

Meng Xu
Dr. Meng Xu is an Assistant Professor in the Cheriton School of Computer Science at the University of Waterloo, Canada. His research is in the area of system and software security, with a focus on delivering high-quality solutions to practical security programs, especially in finding and patching vulnerabilities in critical computer systems. This usually includes research and development of automated program analysis/ testing / verification tools that facilitate the security reasoning of critical programs.


Ways to Watch

YouTube

Watch Now!

Over 500 videos of our weekly seminar and symposia keynotes are available on our YouTube Channel. Also check out Spaf's YouTube Channel. Subscribe today!