Speaker:
Meng Xu
University of Waterloo

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: 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.

The weekly security seminar has been held every semester since spring of 1992. We invite personnel at Purdue and visitors from outside to present on topics of particular interest to them in the areas of computer and network security, computer crime investigation, information warfare, information ethics, public policy for computing and security, the computing "underground," and other related topics. More info